ϵ">]>
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] Dyadic case analysis. Syntax:
Example(s):
where is a new variable (eigen-variable).
The predicate is defined in the module Standard.
Dyadic induction. Show that the principle of dyadic induction is admissible in Peano arithmetic.
Remark. Prove the claim for the special case in the following theory.
Hint. Reduce dyadic induction to complete induction.