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.
Chapter. Numeric Programs.
Section. Primitive Recursion.
[CL] Mathematical induction. Syntax:
where the induction formula is formed from the current sequent.
Example(s):
indN;x
indN;x;a
Note that the predicate N is defined in the module Standard as:
Exponentiation.
Exercise. Prove
[CL] Remark. Note that we then have
##
Exercise. (1 point for one solved problem) Prove