ϵ">]>
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.
Exercise. Show that the principle of -induction is admissible in Peano arithmetic.
Remark. Prove the claim for the special case in the following theory.
[CL] Hint. Reduce the induction on to course of values induction with measure . Recall that the pair size function , written as |x|, is defined in the module Standard.