ϵ">]>
Measure induction. (bonus 1 point) Show that the principle of measure induction (course of values induction with measure) is admissible in Peano arithmetic.
Remark. Prove the claim for the special case in the following theory.
[CL] Measure 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_minus |
is proved in the module Maux*.