ϵ">]>
Literature.
[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.
[CL] Discrimination on the constructors of numeric terms. Example(s):
[CL] Formatting the output. Use the format to display numbers as numeric terms. Try out the following simple queries
98041654 = t:Term
3,(2,(0,1),1,2),0,3 = t:Term
[CL] Structural case analysis on numeric terms. Syntax:
Example(s):
where , , and are new variables (eigen-variables).
Structural induction on numeric terms. Show that the principle of structural induction over numeric terms is admissible in Peano arithmetic.
Remark. Prove the claim for the special case in the following theory.
[CL] Hint. Reduce structural induction on to course of values induction with measure . Recall that the pair size function , written as |x|, is defined in the module Standard.
[CL] Structural induction on numeric terms. Syntax:
where the induction formula is formed from the current sequent.
Example(s):
where , , and are new variables (eigen-variables).
where , , and are new variables (eigen-variables).
[CL] Structural induction on numeric terms (2nd form). Syntax:
where the induction formula is formed from the current sequent.
Example(s):
where , , and are new variables (eigen-variables).
where , , and are new variables (eigen-variables).
Rearranging terms into additive normal form. Define the function such that
Verify your implementations!