ϵ">]>
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] Structural case analysis on lists. Syntax:
Example(s):
where and are new variables (eigen-variables).
The predicate is defined in the module Standard.
[CL] Structural induction on lists. Syntax:
where the induction formula is formed from the current sequent.
Example(s):
The predicate is defined in the module Standard.
List concatenation. The list concatenation function , written as x++y, is defined in the module and the following properties are built in into the CL theorem prover:
We write as an abbreviation for .