Proof step 1 from proof sub-01 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i→n(i - j) ≠ i→n(i) - i→n(j), j ≤ 0, i ≤ j ⊦

Rule argument

Additional information

Proof step 2 from proof sub-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i→n(i - j) ≠ i→n(i) - i→n(j), i ≤ j, j ≤ 0, i ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs

Proof step 3 from proof sub-01 (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  i = i0 + j, i→n(i0) ≠ i→n(i) - i→n(j), i ≤ 0, j ≤ 0, i ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i0 = i - j ↔ i = i0 + j; (elim) Used terms: i, j, i0

Proof step 4 from proof sub-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i→n(i0) ≠ i→n(i0 + j) - i→n(j), j ≤ 0, i0 + j ≤ 0, i0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: 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 ↔ j ≤ 0; (s)

Proof step 5 from proof sub-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  0 ≤ i, 0 ≤ j ⊦ i→n(i) + i→n(j) = i→n(i + j)

• Proof step 7:

  i→n(i0) ≠ i→n(i0 + j) - i→n(j), i0 ≤ 0, i0 + j ≤ 0, j ≤ 0 ⊦ 0 ≤ i0 ∧ 0 ≤ j

Rule argument

Additional information

Used simplifier rules: ⊦ m + n - m = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic Used terms: j, i0

Proof step 6 from proof sub-01 (previous step) (back to tree)

Lemma add

Proof step 7 from proof sub-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  i0 ≠ 0, i→n(i0) ≠ i→n(i0 + j) - i→n(j), i0 < 0, i0 + j ≤ 0, j ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ m - m = 0; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i + 0 = i; (s) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s)

Proof step 8 from proof sub-01 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 9:

  0 ≤ i, 0 ≤ j ⊦ i→n(i) + i→n(j) = i→n(i + j)

Rule argument

Additional information

Used simplifier rules: abs-neg: ⊦ i→n(~ i) = i→n(i); ⊦ ~ i + ~ j = ~(i + j); (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 = n; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) ⊦ i + 0 = i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: ~ i0, ~ j

Proof step 9 from proof sub-01 (previous step) (back to tree)

Lemma add