Proof step 1 from proof ls-fin-add (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  n→i(m) < n→i(n) + i, 0 ≤ i, ¬ m < n + i→n(i) ⊦

Rule argument

Additional information

Proof step 2 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  0 < n→i(n) + i, n→i(m) < n→i(n) + i, n + i→n(i) ≤ m, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: pos-int: ⊦ n→i(m) < j → 0 < j; ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 3 from proof ls-fin-add (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; nat freely generated by 0, +1;; ⊦ m ≤ 0 ↔ m = 0; (s) ⊦ m + n = 0 ↔ m = 0 ∧ n = 0; (ws) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

Proof step 4 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  0 < n→i(n) + i, n→i(m0) + 1 < n→i(n) + i, n + i→n(i) ≤ m0 + 1, 0 ≤ i, ∀ n0, i0. ¬ 0 < n→i(n0) + i0 ∨ ¬ n→i(m0) < n→i(n0) + i0 ∨ ¬ n0 + i→n(i0) ≤ m0 ∨ ¬ 0 ≤ i0 ⊦

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 +1 = m + 1; (s)

Proof step 5 from proof ls-fin-add (previous step) (back to tree)

User applied rule all left

And obtained the following new goals

• Proof step 6:

  n→i(m0) + 1 < n→i(n) + i, 0 < n→i(n) + i, 0 ≤ i, n + i→n(i) ≤ m0 + 1, ¬ 0 < n→i(n) + i ∨ ¬ n→i(m0) < n→i(n) + i ∨ ¬ n + i→n(i) ≤ m0 ∨ ¬ 0 ≤ i ⊦

Rule argument

Additional information

Used terms: n, i

Proof step 6 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  n + i→n(i) = m0 + 1, n→i(m0) < n→i(n) + i, n→i(m0) + 1 < n→i(n) + i, 0 < n→i(n) + i, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: num-n2i-ls-02: 0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n; ls-int-ls-nat: ⊦ i ≥ 0 → ((* i) + n→i(n) < n→i(m) ↔ i→n(i) + n < m); c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ ¬ n < n; (s) ⊦ m < n + 1 ↔ ¬ n < m; (s) ⊦ m < n → (n ≤ m + 1 ↔ n = m + 1); (s) ⊦ m + 1 ≠ 0; (s) lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat ⊦ m ≤ n ↔ ¬ n < m; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ ¬ m + n < m; (s) ⊦ 0 < m ↔ m ≠ 0; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le: ⊦ i ≤ j ∧ 0 < i → 0 < j; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s)

Proof step 7 from proof ls-fin-add (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  n + i→n(i) = m0 + 1, m0 = n + i→n(i) -1, 0 < n→i(n) + i, n→i(m0) + 1 < n→i(n) + i, n→i(m0) < n→i(n) + i, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: num-i2n-le-02: 0 ≤ i ⊦ (* m) ≤ i→n(i) ↔ n→i(m) ≤ i; nat2int-04: ⊦ n→i(m) < n→i(n) ↔ m < n; ls-int-ls-nat: ⊦ i ≥ 0 → ((* i) + n→i(n) < n→i(m) ↔ i→n(i) + n < m); num-n2i-ls-02: 0 ≤ i ⊦ (* i) < n→i(n) ↔ i→n(i) < n; ⊦ n -1 = n - 1; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 1 ≤ i ↔ 0 < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ n + 0 = n; (s) ⊦ 0 + i = i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 0 < m ↔ m ≠ 0; (s) eqle-one: ⊦ m = n + 1 ∧ n < n0 → m ≤ n0; (forward) from specification nat f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic lf-02: ⊦ m < n ∧ m = n0 → n0 < n; (forward) from specification nat-basic lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic ⊦ m < n → n ≠ 0; (s) ⊦ m < n → (n ≤ m ↔ false); (s) n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used formulas: m0 = n + i→n(i) -1

Proof step 8 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  0 < n→i(n) + i, n→i(i→n(i) - 1) < i, n→i(i→n(i) - 1) + 1 < i, 0 < i, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: num-i2n-le-02: 0 ≤ i ⊦ (* m) ≤ i→n(i) ↔ n→i(m) ≤ i; nat2int-08: ⊦ ¬ n→i(n) < 0; n2i-add: ⊦ n→i(m + n) = n→i(m) + n→i(n); pos-int: ⊦ n→i(m) < j → 0 < j; 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) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ n -1 = n - 1; (s) n ≤ m ⊦ (m - n) + n0 = n1 ↔ m + n0 = n + n1; (s) ⊦ i + j < j ↔ i < 0; (s) ⊦ 0 + i = i; (s) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 1 ≤ i ↔ 0 < i; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ m + n = m + n0 ↔ n = n0; (s)

Proof step 9 from proof ls-fin-add (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 10:

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

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; lf-02: ⊦ i < j ∧ j = i0 → i < i0; (forward) from specification int-basic1 n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: i→n(i), m

Proof step 10 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  i→n(i) = m + 1, i ≠ 0, 0 < n→i(n) + i, n→i(m) < i, n→i(m) + 1 < i, 0 < i ⊦

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; ⊦ i ≠ j → (i ≤ j ↔ i < j); (s)

Proof step 11 from proof ls-fin-add (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 12:

  i→n(i0 -1) = m + 1, i0 -1 ≠ 0, 0 < i0 -1, n→i(m) + 1 < i0 -1, n→i(m) < i0 -1, 0 < n→i(n) + i0 -1, ∀ m, n. ¬(i→n(i0) = m + 1 ∧ i0 ≠ 0 ∧ 0 < n→i(n) + i0 ∧ n→i(m) < i0 ∧ n→i(m) + 1 < i0 ∧ 0 < i0) ⊦

Rule argument

Additional information

Used simplifier rules: rax-04: ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; pos-int: ⊦ n→i(m) < j → 0 < j; i2i-pos: ⊦ 0 < i → n→i(i→n(i)) = i; int generated by 0, +1, -1;; ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ i + (* j) < i0 + (* j0) ↔ i < i0 + (j0 - j); (s) ⊦ 0 + i = i; (s) ⊦ i +1 = i + 1; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 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 forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ ¬ i < i; (s)

Proof step 12 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  i→n(i0) - 1 = m + 1, i0 ≠ 1, 0 < i0, 0 < n→i(n) + i0, 1 < i0, 2 + n→i(m) < i0, 1 < n→i(n) + i0, ∀ m0, n0. i→n(i0) ≠ m0 + 1 ∨ i0 = 0 ∨ ¬ 0 < n→i(n0) + i0 ∨ ¬ n→i(m0) < i0 ∨ ¬ n→i(m0) + 1 < i0 ⊦

Rule argument

Additional information

Used simplifier rules: sub: j ≤ i, 0 ≤ j ⊦ i→n(i - j) = i→n(i) - i→n(j); forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + j < i0 ∧ j0 < j → i + j0 < i0; (s) ⊦ i < j - i0 ↔ i + i0 < j; (s) ⊦ i -1 = i - 1; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 1 ≤ i ↔ 0 < i; (s)

Proof step 13 from proof ls-fin-add (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 14:

  i→n(i0) = m1 + 1, m1 = m + 1, i0 ≠ 1, i→n(i0) ≠ 0, 1 < n→i(n) + i0, 2 + n→i(m) < i0, 1 < i0, 0 < n→i(n) + i0, 0 < i0, ∀ m0, n0. i→n(i0) ≠ m0 + 1 ∨ i0 = 0 ∨ ¬ 0 < n→i(n0) + i0 ∨ ¬ n→i(m0) < i0 ∨ ¬ n→i(m0) + 1 < i0 ⊦

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; n ≠ 0 ⊦ m = n - 1 ↔ n = m + 1; (elim) Used terms: i→n(i0), m1

Proof step 14 from proof ls-fin-add (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 15:

  i→n(i0) = 2 + m, i0 ≠ 0, i0 ≠ 1, 1 < n→i(n) + i0, 2 + n→i(m) < i0, 1 < i0, 0 < n→i(n) + i0, 0 < i0, ∀ n0. ¬ 0 < n→i(n0) + i0 ⊦

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; nat2int-03: ⊦ n→i(n + 1) = n→i(n) + 1; add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + j < i0 ∧ ¬ j < j0 → i + j0 < i0; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ i + j < i0 ∧ j0 < j → i + j0 < i0; (s) n < n0 ⊦ m + (* n) = m0 + (* n0) ↔ m = m0 + (n0 - n); (s)

Proof step 15 from proof ls-fin-add (previous step) (back to tree)

Heuristic quantifier closing applied rule all left

And closed the goal!

Rule argument

Additional information

Used terms: n