Clausal Language (ver. 5.81.21, by P.J. Voda, J. Komara, J. Kluka)

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. Course of Values Recursion.

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.

\forall x (\forall y (y < x \to φ [y]) \to φ [x])

\forall z (z < n \to φ [z])

φ [x]

[CL] Complete mathematical induction. Syntax:

indm <variable> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

$indm x$
$\frac{φ [x] *}{\forall y (y < x \to φ [y]) \to φ [x] *}$
$indm x; a$
$\frac{φ [x] *}{\forall y (y < x \to \forall a φ [y]) \to φ [x] *}$

Integer division.

x \div 0 = 0

x \div y = 0 \leftarrow y \neq 0 \land x < y

x \div y = (x ∸ y) \div y + 1 \leftarrow y \neq 0 \land x ≧ y

Exercise. Prove

y \neq 0 \to \exists r (x = x \div y \cdot y + r \land r < y)

y \neq 0 \to \exists r (x = x \div y \cdot y + r \land r < y)

Greatest common divisor. Euclid algorithm based on the property

x \neq 0 \land z ∣ x \to z ∣ y \leftrightarrow z ∣ y mod x

[CL] Remark. This property in the form of the following theorem

x \neq 0 \land z ∣ x \to z ∣ y mod x \leftrightarrow z ∣ y

Euclid_divides_mod

is proved in the module Maux*.

\gcd (0, y) = y

\gcd (x, y) = \gcd (y mod x, x) \leftarrow x \neq 0

Exercise. (1 point) Prove

x \neq 0 \lor y \neq 0 \to \gcd (x, y) ∣ x \land \gcd (x, y) ∣ y

(x \neq 0 \lor y \neq 0) \land z ∣ x \land z ∣ y \to z ≦ \gcd (x, y)

[CL] Hint. In the proof you will need the following theorem

x \neq 0 \to y mod x < x

Mod_bounded

from the module Maux*.

x \neq 0 \lor y \neq 0 \to \gcd (x, y) ∣ x \land \gcd (x, y) ∣ y

(x \neq 0 \lor y \neq 0) \land z ∣ x \land z ∣ y \to z ≦ \gcd (x, y)

Query:

Results:

Heap used: 302012 free: 133913688

Time used: 0:0:0:37