Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
...
Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)
Module in logic: Peano arithmetic
Included module
Remark
[CL] CL-TeX.
Application display Tex_f1_f / 1:
Application display Tex_f1_g / 1:
Application display Tex_f1_r / 1:
Application display Tex_f2_r1 / 2:
Remark
Generalized root I.
Theory in logic: ☆Peano arithmetic
Function displayed by Tex_f1_f as
Axiom
Axiom
Remark
Exercise. Prove
Theorem
End of theory
Remark
Generalized root II.
Theory in logic: ☆Peano arithmetic
Function displayed by Tex_f1_f as
Function displayed by Tex_f1_g as
Axiom
Axiom
Function / 2 displayed by Tex_f2_r1 as
Function displayed by Tex_f1_r as
Remark
Exercise. Prove
Theorem
End of theory
Remark
Generalized root III.
Theory in logic: ☆Peano arithmetic
Function displayed by Tex_f1_f as
Function displayed by Tex_f1_g as
Axiom
Axiom
Function / 2 displayed by Tex_f2_r1 as
Function displayed by Tex_f1_r as
Remark
Exercise. Prove
Remark. Note that the auxiliary function is defined by regular recursion with measure . The condition in the second clause guarantees that the definition is regular: