Proof step 1 from proof labsp (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i→n(i) < i→n(j) ↔ abs(i) < abs(j)), 0 ≤ j, 0 ≤ i ⊦

Rule argument

Additional information

Proof step 2 from proof labsp (previous step) (back to tree)

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

  ¬(i→n(i0 +1) < i→n(j) ↔ abs(i0 +1) < abs(j)), 0 ≤ i0 +1, 0 ≤ j, ∀ j. ¬(¬(i→n(i0) < i→n(j) ↔ abs(i0) < abs(j)) ∧ 0 ≤ j ∧ 0 ≤ i0) ⊦

• Proof step 8:

  ¬(i→n(i0 -1) < i→n(j) ↔ abs(i0 -1) < abs(j)), 0 ≤ i0 -1, 0 ≤ j, ∀ j. ¬(¬(i→n(i0) < i→n(j) ↔ abs(i0) < abs(j)) ∧ 0 ≤ j ∧ 0 ≤ i0) ⊦

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; int generated by 0, +1, -1;; ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ i ≤ j → ¬ j < i; (s)

Proof step 3 from proof labsp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  ¬(i→n(i0 + 1) < i→n(j) ↔ abs(i0 + 1) < j), ~1 ≤ i0, 0 ≤ j, ∀ j0. (i→n(i0) < i→n(j0) ↔ i0 < j0) ∨ ¬ 0 ≤ j0 ∨ ¬ 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ 0 ≤ i → abs(i) = i; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ i +1 = i + 1; (s)

Proof step 4 from proof labsp (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  ¬(i→n(i0 + 1 - 1) + 1 < i→n(j) ↔ abs(i0 + 1) < j), 0 < i0 + 1, 0 ≤ j, ~1 ≤ i0, ∀ j0. (i→n(i0) < i→n(j0) ↔ i0 < j0) ∨ ¬ 0 ≤ j0 ∨ ¬ 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; ⊦ i < 0 → abs(i + 1) = abs(i) - 1; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i - j = ~(i + j); (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs i < 0 ⊦ (* i) + j = j - ~ i; (s) ⊦ 0 < m ↔ m ≠ 0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i - j < i0 ↔ i < j + i0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ 0 ≤ i → (i < 1 ↔ i = 0); (s) Used terms: i0 + 1

Proof step 5 from proof labsp (previous step) (back to tree)

Lemma Int2nat-pos

Proof step 6 from proof labsp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ¬(i→n(i0) + 1 < i→n(j) ↔ i0 + 1 < j), 0 ≤ i0, 0 ≤ j, ∀ j0. (i→n(i0) < i→n(j0) ↔ i0 < j0) ∨ ¬ 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ 0 < j → abs(j) = j; (s) ⊦ i + 0 = i; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s)

Proof step 7 from proof labsp (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

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

Proof step 8 from proof labsp (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  ¬(¬ i→n(j) < i→n(i0) ↔ i0 ≤ j), 0 < i0, 0 ≤ j, ∀ j0. (i→n(i0) < i→n(j0) ↔ i0 < j0) ∨ ¬ 0 ≤ j0 ∨ ¬ 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: sub: j ≤ i, 0 ≤ j ⊦ i→n(i - j) = i→n(i) - i→n(j); abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ 0 < j → abs(j) = j; (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 + 1 ↔ i ≤ j; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ 0 < i → abs(i - 1) = abs(i) - 1; (s) ⊦ 1 ≤ i ↔ 0 < i; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i -1 = i - 1; (s) c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic ⊦ m < n + 1 ↔ ¬ n < m; (s) n0 ≤ n ⊦ n - n0 < m ↔ n < m + n0; (s) ⊦ m < 1 ↔ m = 0; (s) ⊦ m ≤ n ↔ ¬ n < m; (ss) ⊦ i ≤ j → ¬ j < i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 9 from proof labsp (previous step) (back to tree)

User applied rule all left

And closed the goal!

Rule argument

Additional information

Used simplifier rules: rax-04: ⊦ 0 ≤ i → i→n(i + 1) = i→n(i) + 1; ⊦ m < n + 1 ↔ ¬ n < m; (s) a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic c: ⊦ m + n = n + m; from specification nat-basic ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: j + 1