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.
Complete mathematical induction. (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*.