Proof step 1 from proof allslotsfull-inc (conclusion) (back to tree)

n1 < # ar, n0 < # ar ⊦ n = (n1 + 1) % # ar ∧ ar[n1] ≠ e ∧ ar[n1] ≠ ⊥ → (allslotsfull(ar, n0, n1, e, false) ↔ allslotsfull(ar, n0, n, e, true))

System applied rule normalize

And obtained the following new goals

Proof step 2:
n = (n1 + 1) % # ar, ¬(allslotsfull(ar, n0, n1, e, false) ↔ allslotsfull(ar, n0, n, e, true)), ar[n1] ≠ ⊥, ar[n1] ≠ e, n0 < # ar, n1 < # ar ⊦

Rule argument

Additional information

Proof step 2 from proof allslotsfull-inc (previous step) (back to tree)

n = (n1 + 1) % # ar, ¬(allslotsfull(ar, n0, n1, e, false) ↔ allslotsfull(ar, n0, n, e, true)), ar[n1] ≠ ⊥, ar[n1] ≠ e, n0 < # ar, n1 < # ar ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 3:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n0 < # ar, n1 < # ar ⊦ (∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥) ↔ (∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥)

Rule argument

Additional information

Used simplifier rules: allslotsfull-def: ⊦ allslotsfull(ar, n0, n, e, b) ↔ (∀ m. between(n0, m, n, b) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥); between-def: ⊦ between(n0, m, n, b) ↔ n0 = n ∧ b ∨ (n < n0 ⊃ m < n ∨ n0 ≤ m;n0 ≤ m ∧ m < n); ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 3 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n0 < # ar, n1 < # ar ⊦ (∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥) ↔ (∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥)

User applied rule case distinction

And obtained the following new goals

Proof step 4:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥
Proof step 24:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

pos: right 1

Additional information

Proof step 4 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 5:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar) ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Proof step 5 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar) ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule all left

And obtained the following new goals

Proof step 6:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar) ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

pos: left 6 terms: m abort: F discard: F computed: T

Additional information

Used terms: m

Proof step 6 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar) ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 7:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar) ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Proof step 7 from proof allslotsfull-inc (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

Proof step 8:
n0 = (n1 + 1) % # ar, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥
Proof step 16:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar), ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

pos: left 7

Additional information

Proof step 8 from proof allslotsfull-inc (previous step) (back to tree)

n0 = (n1 + 1) % # ar, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 9:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n1 < # ar, ∀ m. (n1 < (n1 + 1) % # ar ⊃ m < n1 ∨ (n1 + 1) % # ar ≤ m;(n1 + 1) % # ar ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < (n1 + 1) % # ar ⊃ m < n1 ∨ (n1 + 1) % # ar ≤ m;(n1 + 1) % # ar ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m % n < n; (s) ⊦ m < n → n ≠ 0; (s)

Proof step 9 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n1 < # ar, ∀ m. (n1 < (n1 + 1) % # ar ⊃ m < n1 ∨ (n1 + 1) % # ar ≤ m;(n1 + 1) % # ar ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < (n1 + 1) % # ar ⊃ m < n1 ∨ (n1 + 1) % # ar ≤ m;(n1 + 1) % # ar ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 10:
n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n
Proof step 11:
# ar ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, m < # ar, (n1 + 1) / # ar * # ar ≤ n1 + 1, ∀ m. (n1 < n1 + 1 - (n1 + 1) / # ar * # ar ⊃ m < n1 ∨ n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ;n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ∧ m < n1 ) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n1 + 1 - (n1 + 1) / # ar * # ar ⊃ m < n1 ∨ n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ;n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ∧ m < n1 ), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

spec: nat-div, name:rax, seq:n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n, subst:[m, n] → [n1 + 1, # ar], <all paths>

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) n ≠ 0 ⊦ m / n * n ≤ m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult Used terms: n1 + 1, # ar

Proof step 10 from proof allslotsfull-inc (previous step) (back to tree)

n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n

A spec-lemma

Proof step 11 from proof allslotsfull-inc (previous step) (back to tree)

# ar ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, m < # ar, (n1 + 1) / # ar * # ar ≤ n1 + 1, ∀ m. (n1 < n1 + 1 - (n1 + 1) / # ar * # ar ⊃ m < n1 ∨ n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ;n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ∧ m < n1 ) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n1 + 1 - (n1 + 1) / # ar * # ar ⊃ m < n1 ∨ n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ;n1 + 1 - (n1 + 1) / # ar * # ar ≤ m ∧ m < n1 ), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 12:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n1 < # ar, ∀ m0. ((n1 + 1) / # ar * # ar = 0 ⊃ m0 < n1 ∨ n1 < m0 + (n1 + 1) / # ar * # ar ;n1 < m0 + (n1 + 1) / # ar * # ar ∧ m0 < n1 ) ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ((n1 + 1) / # ar * # ar = 0 ⊃ m < n1 ∨ n1 < m + (n1 + 1) / # ar * # ar;n1 < m + (n1 + 1) / # ar * # ar ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + 1 ≤ n ↔ m < n; (s) n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s) mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult n ≠ 0 ⊦ m / n * n ≤ m; (s) ⊦ m < n → n ≠ 0; (s) ⊦ 0 ≤ m; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m + n < m + n0 ↔ n < n0; (s) n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s)

Proof step 12 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n1 < # ar, ∀ m0. ((n1 + 1) / # ar * # ar = 0 ⊃ m0 < n1 ∨ n1 < m0 + (n1 + 1) / # ar * # ar ;n1 < m0 + (n1 + 1) / # ar * # ar ∧ m0 < n1 ) ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ((n1 + 1) / # ar * # ar = 0 ⊃ m < n1 ∨ n1 < m + (n1 + 1) / # ar * # ar;n1 < m + (n1 + 1) / # ar * # ar ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule case distinction

And obtained the following new goals

Proof step 13:
(n1 + 1) / # ar * # ar ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, m < # ar, ∀ m0. ((n1 + 1) / # ar * # ar = 0 ⊃ m0 < n1 ∨ n1 < m0 + (n1 + 1) / # ar * # ar ;n1 < m0 + (n1 + 1) / # ar * # ar ∧ m0 < n1 ) ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥, n1 < m + (n1 + 1) / # ar * # ar ∧ m < n1

Rule argument

pos: right 1

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m ≤ m; (s)

Proof step 13 from proof allslotsfull-inc (previous step) (back to tree)

(n1 + 1) / # ar * # ar ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, m < # ar, ∀ m0. ((n1 + 1) / # ar * # ar = 0 ⊃ m0 < n1 ∨ n1 < m0 + (n1 + 1) / # ar * # ar ;n1 < m0 + (n1 + 1) / # ar * # ar ∧ m0 < n1 ) ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥, n1 < m + (n1 + 1) / # ar * # ar ∧ m < n1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 14:
(n1 + 1) / # ar ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < m + (n1 + 1) / # ar * # ar, m < # ar, n1 < # ar, n1 ≤ m, ∀ m0. n1 < m0 + (n1 + 1) / # ar * # ar ∧ m0 < n1 ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n ↔ ¬ n ≤ m; (ss) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult ⊦ m * n + n0 < n ↔ m = 0 ∧ n0 < n; (ws) ⊦ m ≠ 0 → (m * n = 0 ↔ n = 0); (s) ⊦ m0 * m = 0 ↔ m0 = 0 ∨ m = 0; (ws)

Proof step 14 from proof allslotsfull-inc (previous step) (back to tree)

(n1 + 1) / # ar ≠ 0, ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < m + (n1 + 1) / # ar * # ar, m < # ar, n1 < # ar, n1 ≤ m, ∀ m0. n1 < m0 + (n1 + 1) / # ar * # ar ∧ m0 < n1 ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 15:
n ≠ 0 ⊦ n ≤ m → m / n = (m - n) / n + 1

Rule argument

spec: nat-div, name:rec, seq:n ≠ 0 ⊦ n ≤ m → m / n = (m - n) / n + 1, subst:[m, n] → [n1 + 1, # ar], <all paths>

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) ⊦ m * (n + 1) = m * n + m; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ ¬ n < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m + n - n + n1 = m - n1; (s) ⊦ m - m = 0; (s) ⊦ m + 1 ≠ 0; (s) n ≠ 0 ⊦ 0 / n = 0; (s) ⊦ 0 * n = 0; (s) ⊦ ¬ m + n < m; (s) ⊦ m < n → ¬ n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ n ∧ n0 ≠ 0 → ¬ n * n0 < m; (s) ⊦ m + m = 2 * m; (s) ⊦ m0 ≠ 0 → m ≤ m * m0; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ m ≤ m; (s) ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic succ-03: ⊦ m < n ∧ m + 1 ≠ n → m + 1 < n; (forward) from specification nat-basic ⊦ m < n → m / n = 0; (s) Used terms: n1 + 1, # ar

Proof step 15 from proof allslotsfull-inc (previous step) (back to tree)

n ≠ 0 ⊦ n ≤ m → m / n = (m - n) / n + 1

A spec-lemma

Proof step 16 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar), ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule case distinction

And obtained the following new goals

Proof step 17:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, (n1 + 1) % # ar < n0, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, m < (n1 + 1) % # ar ∨ n0 ≤ m ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥
Proof step 21:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, m < (n1 + 1) % # ar, n0 ≤ m, ¬ (n1 + 1) % # ar < n0, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

pos: left 6

Additional information

Proof step 17 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, (n1 + 1) % # ar < n0, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, m < (n1 + 1) % # ar ∨ n0 ≤ m ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 18:
ar[n1] ≠ ⊥, ar[n1] ≠ e, m < # ar, n0 < # ar, n1 < # ar, (n1 + 1) % # ar < n0, (n1 + 1) % # ar + 1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, m < (n1 + 1) % # ar ∨ n0 ≤ m ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m % n < n; (s) ⊦ m < n → n ≠ 0; (s) ⊦ m +1 = m + 1; (s) trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 18 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ ⊥, ar[n1] ≠ e, m < # ar, n0 < # ar, n1 < # ar, (n1 + 1) % # ar < n0, (n1 + 1) % # ar + 1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, m < (n1 + 1) % # ar ∨ n0 ≤ m ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule case distinction

And obtained the following new goals

Proof step 19:
ar[n1] ≠ ⊥, ar[n1] ≠ e, (n1 + 1) % # ar + 1 < # ar, (n1 + 1) % # ar < n0, n1 < # ar, n0 < # ar, m < # ar, m < (n1 + 1) % # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

pos: left 9

Additional information

Used simplifier rules: let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat n ≠ 0 ⊦ m < n → ((m + 1) % n < m ↔ n = m + 1 ∧ m ≠ 0); (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ ¬ n < n; (s) ⊦ 0 < m ↔ m ≠ 0; (s) n ≠ 0 ⊦ n % n = 0; (s) ⊦ 1 < m ↔ ¬(m = 0 ∨ m = 1); (s) ⊦ m + 1 ≠ 0; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ m < n → ¬ n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat ⊦ n ≠ 0 → (m + n = 1 ↔ n = 1 ∧ m = 0); (ws) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ n ≤ n0 ∧ n1 ≤ m → n + n1 ≤ n0 + m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ m; (s)

Proof step 19 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ ⊥, ar[n1] ≠ e, (n1 + 1) % # ar + 1 < # ar, (n1 + 1) % # ar < n0, n1 < # ar, n0 < # ar, m < # ar, m < (n1 + 1) % # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 20:
ar[n1] ≠ ⊥, ar[n1] ≠ e, m + 1 < n0, m < (n1 + 1) % # ar, m < # ar, n0 < # ar, n1 < # ar, (n1 + 1) % # ar < n0, (n1 + 1) % # ar + 1 < # ar, m < n0, 2 + m < # ar, m + 1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ n1 < n0 ∧ m < n1, ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: ⊦ m +1 = m + 1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic ⊦ m < n → (n ≤ m ↔ false); (s) ⊦ m < n → n ≠ 0; (s) f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic

Proof step 20 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ ⊥, ar[n1] ≠ e, m + 1 < n0, m < (n1 + 1) % # ar, m < # ar, n0 < # ar, n1 < # ar, (n1 + 1) % # ar < n0, (n1 + 1) % # ar + 1 < # ar, m < n0, 2 + m < # ar, m + 1 < # ar, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ n1 < n0 ∧ m < n1, ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule case distinction

And closed the goal!

Rule argument

pos: right 1

Additional information

Used simplifier rules: fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat ⊦ m < n → m % n = m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ ¬ n < n; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic ⊦ m +1 = m + 1; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ m ≤ m; (s) ⊦ m ≤ n → (n < m ↔ false); (s) n ≠ 0 ⊦ m < n → ((m + 1) % n < m ↔ n = m + 1 ∧ m ≠ 0); (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) n ≠ 0 ⊦ n % n = 0; (s)

Proof step 21 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, m < (n1 + 1) % # ar, n0 ≤ m, ¬ (n1 + 1) % # ar < n0, ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 22:
ar[n1] ≠ ⊥, ar[n1] ≠ e, n1 < (n1 + 1) % # ar, n0 < (n1 + 1) % # ar, m < # ar, n0 < # ar, n1 < # ar, m < (n1 + 1) % # ar, n0 ≤ n1, n1 ≤ m, n0 ≤ m, ∀ m0. n0 ≤ m0 ∧ m0 < n1 ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Used simplifier rules: ⊦ m < n → m ≤ n; (s) ⊦ m < n → n ≠ 0; (s) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ n → (n < m ↔ false); (s) ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 22 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ ⊥, ar[n1] ≠ e, n1 < (n1 + 1) % # ar, n0 < (n1 + 1) % # ar, m < # ar, n0 < # ar, n1 < # ar, m < (n1 + 1) % # ar, n0 ≤ n1, n1 ≤ m, n0 ≤ m, ∀ m0. n0 ≤ m0 ∧ m0 < n1 ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 23:
n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n

Rule argument

spec: nat-div, name:rax, seq:n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n, subst:[m, n] → [n1 + 1, # ar], <all paths>

Additional information

Used simplifier rules: ⊦ m < n → n ≠ 0; (s) n ≠ 0 ⊦ m / n * n ≤ m; (s) mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult mult-c: ⊦ m * n = n * m; from specification nat-mult ⊦ m + n < m + n0 ↔ n < n0; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ 0 ≤ m; (s) n0 ≤ n ⊦ m < n - n0 ↔ m + n0 < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n ↔ ¬ n ≤ m; (ss) fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat ⊦ m ≤ n → (n ≤ m ↔ m = n); (s) ⊦ n + 0 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic ⊦ m ≤ m; (s) Used terms: n1 + 1, # ar

Proof step 23 from proof allslotsfull-inc (previous step) (back to tree)

n ≠ 0, m / n * n ≤ m ⊦ m % n = m - m / n * n

A spec-lemma

Proof step 24 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ∀ m. (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 25:
ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Proof step 25 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, m < # ar, n0 < # ar, n1 < # ar, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule all left

And obtained the following new goals

Proof step 26:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

pos: left 7 terms: m abort: F discard: F computed: T

Additional information

Used terms: m

Proof step 26 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n1 < # ar, n0 < # ar, m < # ar, (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ∀ m. (n0 = (n1 + 1) % # ar ∨ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar)) ∧ m < # ar → ar[m] ≠ e ∧ ar[m] ≠ ⊥ ⊦ ar[m] ≠ e ∧ ar[m] ≠ ⊥

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 27:
ar[n1] ≠ e, ar[n1] ≠ ⊥, n0 ≠ (n1 + 1) % # ar, m < # ar, n0 < # ar, n1 < # ar, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ∀ m0. ((n1 + 1) % # ar < n0 ⊃ m0 < (n1 + 1) % # ar ∨ n0 ≤ m0;n0 ≤ m0 ∧ m0 < (n1 + 1) % # ar) ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar), ar[m] ≠ e ∧ ar[m] ≠ ⊥

Rule argument

Additional information

Proof step 27 from proof allslotsfull-inc (previous step) (back to tree)

ar[n1] ≠ e, ar[n1] ≠ ⊥, n0 ≠ (n1 + 1) % # ar, m < # ar, n0 < # ar, n1 < # ar, (n1 < n0 ⊃ m < n1 ∨ n0 ≤ m;n0 ≤ m ∧ m < n1), ∀ m0. ((n1 + 1) % # ar < n0 ⊃ m0 < (n1 + 1) % # ar ∨ n0 ≤ m0;n0 ≤ m0 ∧ m0 < (n1 + 1) % # ar) ∧ m0 < # ar → ar[m0] ≠ e ∧ ar[m0] ≠ ⊥ ⊦ ((n1 + 1) % # ar < n0 ⊃ m < (n1 + 1) % # ar ∨ n0 ≤ m;n0 ≤ m ∧ m < (n1 + 1) % # ar), ar[m] ≠ e ∧ ar[m] ≠ ⊥

User applied rule case distinction

And closed the goal!

Rule argument

pos: left 7

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss) ⊦ m ≠ n → (m < n ↔ ¬ n < m); (ss) ⊦ m < n → ¬ n < m; (s) fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat n ≠ 0 ⊦ m % n < n; (s) n ≠ 0 ⊦ m < n → ((m + 1) % n < m ↔ n = m + 1 ∧ m ≠ 0); (s) ⊦ m +1 = m + 1; (s) ⊦ m = m0 + n0 ∧ n < n0 → m0 + n < m; (s) ⊦ m < n → m ≤ n; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat lf: ⊦ m < n ∧ n < n0 → m +1 < n0; (forward) from specification nat-basic trans-nat: ⊦ n < n0 ∧ n0 < n1 → n < n1; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m + 1 ≠ 0; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic n ≠ 0 ⊦ n % n = 0; (s) ⊦ m < n → m % n = m; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ m < n → (n ≤ m ↔ false); (s)