Literature.
[1] Ján Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
[3] Ján Komara. Recursive Functions. Online.
Measure induction. (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*.