%%% 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.
%
%
%%%