ϵ">]>
Complete mathematical induction. (bonus 1 point) Show that the principle of complete mathematical induction (course of values induction) is admissible in Peano arithmetic.
Remark. Prove the claim for the special case in the following theory.
[CL] Complete mathematical induction. Syntax:
where the induction formula is formed from the current sequent.
Example(s):
Greatest common divisor. Euclid algorithm based on the property
[CL] Remark. This property in the form of the following theorem
Euclid_divides_mod |
is proved in the module Maux*.