%%% Assignment 9
%%% Out: Mon 26 Nov
%%% Due: Mon 3 Dec
%
% This assignment is to be submitted on paper.
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% 1. Consider the statement:
%
% "for every natural number n, the product n * (n + 1) is even".
%
% Give an informal inductive proof of the corresponding formula:
% Specify clearly what lemmas you are using.
%
% !x:nat ?y:nat . y + y = x * (s x)
%
%
% 2. Give a proof term corresponding to your informal proof from part 1.
% Also give an equational specification of the term.
%
%
% 3. Now bracket irrelevant parts of the proof term,
% according to the following bracketing of the proposition:
%
% !x:nat ?y:nat . [y + y = x * (s x)]
%
%
% 4. Convert the bracketed formula in part 3 into a type, and simplify it.
% Also simplify the bracketed proof term, to arrive at a recursive function
% of the corresponding type.
%
%
% 5. Consider the function in part 4, extracted from the proof in part 2.
% What does it compute? Give an equational specification for it.
%
%
%%%