Proof step 1 from proof nat2int-04 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(n→i(m) < n→i(n) ↔ m < n) ⊦

Rule argument

Additional information

Proof step 2 from proof nat2int-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(n→i(m) < n→i(n) ↔ m < n) ⊦

Rule argument

Additional information

Proof step 3 from proof nat2int-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 4:

  ⊦ m < n ↔ ¬ n ≤ m

• Proof step 5:

  ¬(n→i(m) < n→i(n) ↔ ¬ n ≤ m) ⊦

Rule argument

Additional information

Used terms: n, m

Proof step 4 from proof nat2int-04 (previous step) (back to tree)

A spec-lemma

Proof step 5 from proof nat2int-04 (previous step) (back to tree)

Heuristic structural induction applied rule structural induction

And obtained the following new goals

• Proof step 6:

  ¬(n→i(m0 +1) < n→i(n) ↔ ¬ n ≤ m0 +1), ∀ n. n→i(m0) < n→i(n) ↔ ¬ n ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: nat2int-10: ⊦ n→i(n) ≤ 0 ↔ n = 0; nat freely generated by 0, +1;; ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 6 from proof nat2int-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬(n→i(m0) + 1 < n→i(n) ↔ ¬ n ≤ m0 + 1), ∀ n. n→i(m0) < n→i(n) ↔ ¬ n ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: nat2int-03: ⊦ n→i(n + 1) = n→i(n) + 1; ⊦ 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

Proof step 7 from proof nat2int-04 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  ¬(n→i(m0) + 1 < n→i(n) ↔ ¬ n ≤ m0 + 1), n ≠ 0, ∀ n. n→i(m0) < n→i(n) ↔ ¬ n ≤ m0 ⊦

Rule argument

Additional information

Used simplifier rules: nat2int-06: ⊦ ¬ n→i(n) + 1 < 0; add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 0 ≤ m; (s) Used formulas: n = 0

Proof step 8 from proof nat2int-04 (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 9:

  n→i(m0) < n→i(n -1) ↔ ¬ n -1 ≤ m0, ¬(n→i(m0) + 1 < n→i(n) ↔ ¬ n ≤ m0 + 1), n ≠ 0 ⊦

Rule argument

Additional information

Used terms: n -1

Proof step 9 from proof nat2int-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  n→i(m0) < n→i(n -1) ↔ ¬ n -1 ≤ m0, ¬(n→i(m0) + 1 < n→i(n) ↔ ¬ n ≤ m0 + 1), n ≠ 0 ⊦

Rule argument

Additional information

Proof step 10 from proof nat2int-04 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 11:

  n→i(m0) < n→i(m) ↔ ¬ m ≤ m0, n = m +1, ¬(n→i(m0) + 1 < n→i(n) ↔ ¬ n ≤ m0 + 1), n ≠ 0 ⊦

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m = n -1 ↔ n = m +1; (elim) Used terms: n, m

Proof step 11 from proof nat2int-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: nat2int-03: ⊦ n→i(n + 1) = n→i(n) + 1; c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s) ⊦ m +1 = m + 1; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + j < i + i0 ↔ j < i0; (s)