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