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

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

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])

φ [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 \dot{-} 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. 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:

Heap used: 300252 free: 133916004

Time used: 0:0:0:31