Proof step 2 from proof div-div-rec (previous step) (back to tree)

((j - (2 ^ i - 1)) / 2 ^ i - 1) / 2 ≠ (j - (2 ^ (i + 1) - 1)) / 2 ^ (i + 1), j < 0, 0 < i ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 3:
((j + 1 - 2 ^ i) / 2 ^ i - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j < i, j < 0, 0 < i, j + 1 < i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i +1 = i + 1; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs trans: ⊦ i < j ∧ j < j0 → i < j0; (forward) from specification int-basic1 lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 ⊦ i - (j - j0) = i + j0 - j; (s)

Proof step 3 from proof div-div-rec (previous step) (back to tree)

((j + 1 - 2 ^ i) / 2 ^ i - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j < i, j < 0, 0 < i, j + 1 < i ⊦

User applied rule apply elim lemma

And obtained the following new goals

Proof step 4:
((j + 1 - 2 ^ i) / 2 ^ i - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j + 1 < i, 0 < i, j < 0, j < i ⊦ 0 < 2 ^ i ∧ j + 1 - 2 ^ i < 0
Proof step 7:
j + 1 - 2 ^ i = i0 * 2 ^ i + j0, (i0 - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j + 1 < i, 0 < i, j < 0, j < i, abs(j0) < 2 ^ i, 0 < 2 ^ i, j + 1 - 2 ^ i < 0, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

spec: int-div, name:div-elim-negpos, seq:⊦ 0 < j ∧ i < 0 → ( i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0), subst:[i, j, i0, j0] → [j + 1 - 2 ^ i, 2 ^ i, i0, j0]

Additional information

Used simplifier rules: ⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0); (elim) Used terms: j + 1 - 2 ^ i, 2 ^ i, i0, j0

Proof step 4 from proof div-div-rec (previous step) (back to tree)

((j + 1 - 2 ^ i) / 2 ^ i - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j + 1 < i, 0 < i, j < 0, j < i ⊦ 0 < 2 ^ i ∧ j + 1 - 2 ^ i < 0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 5:
((j + 1 - 2 ^ i) / 2 ^ i - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j + 1 < i, 0 < i, j < 0, j < i, 0 ≤ i, 2 ^ i ≤ j + 1 ⊦

Rule argument

Additional information

Used simplifier rules: pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i; ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → ¬ j < i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) 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 < i0 ↔ i < j + i0; (s)

Proof step 5 from proof div-div-rec (previous step) (back to tree)

((j + 1 - 2 ^ i) / 2 ^ i - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j + 1 < i, 0 < i, j < 0, j < i, 0 ≤ i, 2 ^ i ≤ j + 1 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 6:
⊦ i < 0 ∧ 0 < j → ¬ j ≤ i

Rule argument

spec: int-abs, name:zero-gels-02, seq: ⊦ i < 0 ∧ 0 < j → ¬ j ≤ i, subst:[i, j] → [j + 1, 2 ^ i], <all paths>

Additional information

Used simplifier rules: pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i; zero: ⊦ 0 < j → (i ^ j = 0 ↔ i = 0); two-lez-01: ⊦ 2 ^ i ≤ 0 ↔ i < 0; ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); (s) j ≠ 0 ⊦ ~ i / j = ~(i / j); (s) i ≠ 0 ⊦ i / i = 1; (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 ⊦ i < j → ¬ j < i; (s) Used terms: j + 1, 2 ^ i

Proof step 6 from proof div-div-rec (previous step) (back to tree)

⊦ i < 0 ∧ 0 < j → ¬ j ≤ i

A spec-lemma

Proof step 7 from proof div-div-rec (previous step) (back to tree)

j + 1 - 2 ^ i = i0 * 2 ^ i + j0, (i0 - 1) / 2 ≠ (j + 1 - 2 ^ (i + 1)) / 2 ^ (i + 1), j + 1 < i, 0 < i, j < 0, j < i, abs(j0) < 2 ^ i, 0 < 2 ^ i, j + 1 - 2 ^ i < 0, j0 ≤ 0, i0 ≤ 0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 8:
j + 1 = 2 ^ i * (i0 + 1) + j0, (i0 - 1) / 2 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), j0 < i, i0 < i, j + 1 < 2 ^ i, j + 1 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, 0 ≤ i, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i; succ: ⊦ 0 ≤ i → j ^ (i + 1) = j ^ i * j; ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs ⊦ i < 0 ∧ 0 ≤ j → i < 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 + 0 = i; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * j + i = i * (j + 1); (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 8 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (i0 + 1) + j0, (i0 - 1) / 2 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), j0 < i, i0 < i, j + 1 < 2 ^ i, j + 1 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, 0 ≤ i, j0 ≤ 0, i0 ≤ 0 ⊦

User applied rule subst equation

And obtained the following new goals

Proof step 9:
j + 1 = 2 ^ i * (i0 + 1) + j0, (i0 - 1) / 2 ≠ (2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), abs(j0) < 2 ^ i, j < 0, 0 < i, 2 ^ i * (i0 + 1) + j0 < i, 2 ^ i * (i0 + 1) + j0 < 2 ^ i, i0 < i, j0 < i, i0 ≤ 0, j0 ≤ 0, 0 ≤ i ⊦

Rule argument

pos: left 1, flags:

Additional information

Proof step 9 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (i0 + 1) + j0, (i0 - 1) / 2 ≠ (2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), abs(j0) < 2 ^ i, j < 0, 0 < i, 2 ^ i * (i0 + 1) + j0 < i, 2 ^ i * (i0 + 1) + j0 < 2 ^ i, i0 < i, j0 < i, i0 ≤ 0, j0 ≤ 0, 0 ≤ i ⊦

User applied rule cut formula

And obtained the following new goals

Proof step 10:
j + 1 = 2 ^ i * (i0 + 1) + j0, 2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2 = 2 ^ i * (i0 - 1) + j0, (i0 - 1) / 2 ≠ (2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j0 < i, i0 < i, 2 ^ i * (i0 + 1) + j0 < 2 ^ i, 2 ^ i * (i0 + 1) + j0 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, 0 ≤ i, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

fma: 2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2 = 2 ^ i * (i0 - 1) + j0

Additional information

Used simplifier rules: ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + j = i + i0 ↔ 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 Used formulas: 2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2 = 2 ^ i * (i0 - 1) + j0

Proof step 10 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (i0 + 1) + j0, 2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2 = 2 ^ i * (i0 - 1) + j0, (i0 - 1) / 2 ≠ (2 ^ i * (i0 + 1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j0 < i, i0 < i, 2 ^ i * (i0 + 1) + j0 < 2 ^ i, 2 ^ i * (i0 + 1) + j0 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, 0 ≤ i, j0 ≤ 0, i0 ≤ 0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 11:
j + 1 = 2 ^ i * (i0 + 1) + j0, (i0 - 1) / 2 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), 2 ^ i * i0 + j0 < 0, j + 1 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, i0 < i, 0 ≤ i, j0 ≤ 0, i0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (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 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * (j + 1) + j1 < i ↔ i * j + j1 < 0; (s) ⊦ i + j = i + i0 ↔ j = i0; (s) ⊦ (* i) + i0 - (* j) = (i - j) + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 11 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (i0 + 1) + j0, (i0 - 1) / 2 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), 2 ^ i * i0 + j0 < 0, j + 1 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, i0 < i, 0 ≤ i, j0 ≤ 0, i0 ≤ 0 ⊦

User applied rule apply elim lemma

And obtained the following new goals

Proof step 12:
j + 1 = 2 ^ i * (i0 + 1) + j0, i0 - 1 = i1 * 2 + j1, i1 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), i0 < i, j0 < i, abs(j0) < 2 ^ i, j < 0, 0 < i, j + 1 < i, 2 ^ i * i0 + j0 < 0, abs(j1) < 2, 0 < 2, i0 - 1 < 0, i0 ≤ 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-div, name:div-elim-negpos, seq:⊦ 0 < j ∧ i < 0 → ( i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0), subst:[i, j, i0, j0] → [i0 - 1, 2, i1, j1]

Additional information

Used simplifier rules: ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ 0 < j ∧ i < 0 → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ j0 ≤ 0 ∧ abs(j0) < j ∧ i0 ≤ 0); (elim) Used terms: i0 - 1, 2, i1, j1

Proof step 12 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (i0 + 1) + j0, i0 - 1 = i1 * 2 + j1, i1 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), i0 < i, j0 < i, abs(j0) < 2 ^ i, j < 0, 0 < i, j + 1 < i, 2 ^ i * i0 + j0 < 0, abs(j1) < 2, 0 < 2, i0 - 1 < 0, i0 ≤ 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 13:
j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, i1 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j + 1 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (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 ≤ ~1 ↔ i < 0; (s) ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * j + i = i * (j + 1); (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i - j = i0 ↔ i = i0 + j; (s)

Proof step 13 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, i1 ≠ (j + 1 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j + 1 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule subst equation

And obtained the following new goals

Proof step 14:
j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, j < 0, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

pos: left 1, flags:

Additional information

Proof step 14 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, j < 0, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule cut formula

And obtained the following new goals

Proof step 15:
j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, (2 * (i1 + 1) + j1) * 2 ^ i + j0 - 2 ^ i * 2 = 2 ^ i * (2 * i1 + j1) + j0, i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

fma: (2 * (i1 + 1) + j1) * 2 ^ i + j0 - 2 ^ i * 2 = 2 ^ i * (2 * i1 + j1) + j0

Additional information

Used simplifier rules: ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ i * j + i = i * (j + 1); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + j = i + i0 ↔ 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 Used formulas: (2 * (i1 + 1) + j1) * 2 ^ i + j0 - 2 ^ i * 2 = 2 ^ i * (2 * i1 + j1) + j0

Proof step 15 from proof div-div-rec (previous step) (back to tree)

j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, (2 * (i1 + 1) + j1) * 2 ^ i + j0 - 2 ^ i * 2 = 2 ^ i * (2 * i1 + j1) + j0, i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule subst equation

And obtained the following new goals

Proof step 16:
j + 1 = 2 ^ i * (2 * (i1 + 1) + j1) + j0, i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, j < 0, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

pos: left 2, flags: discard

Additional information

Proof step 16 from proof div-div-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 17:
⊦ i + (* j) = i0 + (* j0) ↔ i = i0 + (j0 - j)
Proof step 18:
j = 2 ^ i * (2 * (i1 + 1) + j1) + (j0 - 1), i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-abs, name:numadd, seq: ⊦ i + (* j) = i0 + (* j0) ↔ i = i0 + (j0 - j), subst:[j0, i0, j, i] → [j0, 2 ^ i * (2 * (i1 + 1) + j1), 1, j], <all paths>

Additional information

Used terms: j0, 2 ^ i * (2 * (i1 + 1) + j1), 1, j

Proof step 17 from proof div-div-rec (previous step) (back to tree)

⊦ i + (* j) = i0 + (* j0) ↔ i = i0 + (j0 - j)

A spec-lemma

Proof step 18 from proof div-div-rec (previous step) (back to tree)

j = 2 ^ i * (2 * (i1 + 1) + j1) + (j0 - 1), i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, j < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule subst equation

And obtained the following new goals

Proof step 19:
i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 2 ^ i * (2 * (i1 + 1) + j1) + (j0 - 1) < 0, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

pos: left 1, flags: discard

Additional information

Proof step 19 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * (i1 + 1) + j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 2 ^ i * (2 * (i1 + 1) + j1) + (j0 - 1) < 0, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 20:
⊦ i * (j + j0) = i * j + i * j0
Proof step 21:
i1 ≠ ((2 ^ i * 2 * (i1 + 1) + 2 ^ i * j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, (2 ^ i * 2 * (i1 + 1) + 2 ^ i * j1) + j0 < i, 0 < i, (2 ^ i * 2 * (i1 + 1) + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-mult, name:dist-rsplit, seq: ⊦ i * (j + j0) = i * j + i * j0, subst:[j0, j, i] → [j1, 2 * (i1 + 1), 2 ^ i], <all paths>

Additional information

Used terms: j1, 2 * (i1 + 1), 2 ^ i

Proof step 20 from proof div-div-rec (previous step) (back to tree)

⊦ i * (j + j0) = i * j + i * j0

A spec-lemma

Proof step 21 from proof div-div-rec (previous step) (back to tree)

i1 ≠ ((2 ^ i * 2 * (i1 + 1) + 2 ^ i * j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, (2 ^ i * 2 * (i1 + 1) + 2 ^ i * j1) + j0 < i, 0 < i, (2 ^ i * 2 * (i1 + 1) + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 22:
⊦ (i + i0) * j = i * j + i0 * j
Proof step 23:
i1 ≠ ((2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, (2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-mult, name:dist-lsplit, seq: ⊦ (i + i0) * j = i * j + i0 * j, subst:[j, i0, i] → [2, 1, i1], <all paths>

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 2, 1, i1

Proof step 22 from proof div-div-rec (previous step) (back to tree)

⊦ (i + i0) * j = i * j + i0 * j

A spec-lemma

Proof step 23 from proof div-div-rec (previous step) (back to tree)

i1 ≠ ((2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + j0 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, (2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + j0 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 24:
⊦ i + j = j + i
Proof step 25:
i1 ≠ (j0 + 2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1 < i, 0 < i, (2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-basic2, name:add-c, seq: ⊦ i + j = j + i, subst:[j, i] → [j0, 2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1], <all paths>

Additional information

Used terms: j0, 2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1

Proof step 24 from proof div-div-rec (previous step) (back to tree)

⊦ i + j = j + i

A spec-lemma

Proof step 25 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (j0 + 2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1 < i, 0 < i, (2 ^ i * (i1 * 2 + 1 * 2) + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 26:
⊦ i * (j + j0) = i * j + i * j0
Proof step 27:
i1 ≠ (j0 + (2 ^ i * i1 * 2 + 2 ^ i * 1 * 2) + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, ((2 ^ i * i1 * 2 + 2 ^ i * 1 * 2) + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + (2 ^ i * i1 * 2 + 2 ^ i * 1 * 2) + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-mult, name:dist-rsplit, seq: ⊦ i * (j + j0) = i * j + i * j0, subst:[j0, j, i] → [1 * 2, i1 * 2, 2 ^ i], <all paths>

Additional information

Used terms: 1 * 2, i1 * 2, 2 ^ i

Proof step 26 from proof div-div-rec (previous step) (back to tree)

⊦ i * (j + j0) = i * j + i * j0

A spec-lemma

Proof step 27 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (j0 + (2 ^ i * i1 * 2 + 2 ^ i * 1 * 2) + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, ((2 ^ i * i1 * 2 + 2 ^ i * 1 * 2) + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + (2 ^ i * i1 * 2 + 2 ^ i * 1 * 2) + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 28:
⊦ i = 1 → i * j = j
Proof step 29:
1 = 1, i1 ≠ (j0 + (2 ^ i * i1 * 2 + 2 ^ i * 2) + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + (2 ^ i * i1 * 2 + 2 ^ i * 2) + 2 ^ i * j1 < i, 0 < i, ((2 ^ i * i1 * 2 + 2 ^ i * 2) + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-mult, name:one-01, seq: ⊦ i = 1 → i * j = j, subst:[j, i] → [2, 1], <all paths>

Additional information

Used terms: 2, 1

Proof step 28 from proof div-div-rec (previous step) (back to tree)

⊦ i = 1 → i * j = j

A spec-lemma

Proof step 29 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + (2 ^ i * i1 * 2 + 2 ^ i * 2) + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + (2 ^ i * i1 * 2 + 2 ^ i * 2) + 2 ^ i * j1 < i, 0 < i, ((2 ^ i * i1 * 2 + 2 ^ i * 2) + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 30:
⊦ i + j + i0 = (i + j) + i0
Proof step 31:
1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-basic2, name:add-a, seq: ⊦ i + j + i0 = (i + j) + i0, subst:[i0, j, i] → [2 ^ i * j1, 2 ^ i * 2, 2 ^ i * i1 * 2], <rotated> <all paths>

Additional information

Used terms: 2 ^ i * j1, 2 ^ i * 2, 2 ^ i * i1 * 2

Proof step 30 from proof div-div-rec (previous step) (back to tree)

⊦ i + j + i0 = (i + j) + i0

A spec-lemma

Proof step 31 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 - 2 ^ i * 2) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 32:
⊦ i + j = j + i
Proof step 33:
1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 < i, 0 < i, (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-basic2, name:add-c, seq: ⊦ i + j = j + i, subst:[j, i] → [2 ^ i * j1, 2 ^ i * 2], <all paths>

Additional information

Used terms: 2 ^ i * j1, 2 ^ i * 2

Proof step 32 from proof div-div-rec (previous step) (back to tree)

⊦ i + j = j + i

A spec-lemma

Proof step 33 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 - 2 ^ i * 2) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 < i, 0 < i, (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 34:
⊦ i + (j - i0) = i + j - i0
Proof step 35:
1 = 1, i1 ≠ (j0 + (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 - 2 ^ i * 2)) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-abs, name:sub-add-01, seq: ⊦ i + (j - i0) = i + j - i0, subst:[i0, j, i] → [2 ^ i * 2, 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2, j0], <rotated> <all paths>

Additional information

Used terms: 2 ^ i * 2, 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2, j0

Proof step 34 from proof div-div-rec (previous step) (back to tree)

⊦ i + (j - i0) = i + j - i0

A spec-lemma

Proof step 35 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 - 2 ^ i * 2)) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 36:
⊦ i + (j - i0) = i + j - i0
Proof step 37:
1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 ^ i * j1 + 2 ^ i * 2 - 2 ^ i * 2)) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 < i, 0 < i, (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-abs, name:sub-add-01, seq: ⊦ i + (j - i0) = i + j - i0, subst:[i0, j, i] → [2 ^ i * 2, 2 ^ i * j1 + 2 ^ i * 2, 2 ^ i * i1 * 2], <rotated> <all paths>

Additional information

Used terms: 2 ^ i * 2, 2 ^ i * j1 + 2 ^ i * 2, 2 ^ i * i1 * 2

Proof step 36 from proof div-div-rec (previous step) (back to tree)

⊦ i + (j - i0) = i + j - i0

A spec-lemma

Proof step 37 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 ^ i * j1 + 2 ^ i * 2 - 2 ^ i * 2)) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2 < i, 0 < i, (2 ^ i * i1 * 2 + 2 ^ i * j1 + 2 ^ i * 2) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 38:
⊦ i + j = j + i
Proof step 39:
1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 ^ i * 2 + 2 ^ i * j1 - 2 ^ i * 2)) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-basic2, name:add-c, seq: ⊦ i + j = j + i, subst:[j, i] → [2 ^ i * 2, 2 ^ i * j1], <all paths>

Additional information

Used terms: 2 ^ i * 2, 2 ^ i * j1

Proof step 38 from proof div-div-rec (previous step) (back to tree)

⊦ i + j = j + i

A spec-lemma

Proof step 39 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 ^ i * 2 + 2 ^ i * j1 - 2 ^ i * 2)) / (2 ^ i * 2), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 40:
⊦ i + j - i0 = (i - i0) + j
Proof step 41:
1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 ^ i * 2 - 2 ^ i * 2) + 2 ^ i * j1) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 < i, 0 < i, (2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-abs, name:sub-shift, seq: ⊦ i + j - i0 = (i - i0) + j, subst:[i0, j, i] → [2 ^ i * 2, 2 ^ i * j1, 2 ^ i * 2], <all paths>

Additional information

Used terms: 2 ^ i * 2, 2 ^ i * j1, 2 ^ i * 2

Proof step 40 from proof div-div-rec (previous step) (back to tree)

⊦ i + j - i0 = (i - i0) + j

A spec-lemma

Proof step 41 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 ^ i * 2 - 2 ^ i * 2) + 2 ^ i * j1) / (2 ^ i * 2), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1 < i, 0 < i, (2 ^ i * i1 * 2 + 2 ^ i * 2 + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 42:
⊦ i * j = j * i
Proof step 43:
1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 * 2 ^ i - 2 * 2 ^ i) + 2 ^ i * j1) / (2 * 2 ^ i), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

Rule argument

spec: int-mult, name:commutativity, seq: ⊦ i * j = j * i, subst:[j, i] → [2, 2 ^ i], <all paths>

Additional information

Used terms: 2, 2 ^ i

Proof step 42 from proof div-div-rec (previous step) (back to tree)

⊦ i * j = j * i

A spec-lemma

Proof step 43 from proof div-div-rec (previous step) (back to tree)

1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + (2 * 2 ^ i - 2 * 2 ^ i) + 2 ^ i * j1) / (2 * 2 ^ i), j1 < i, i1 < i, (i1 * 2 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, (2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1) + (j0 - 1) < 0, 0 < i, j0 + 2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1 < i, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, abs(j1) < 2, i1 * 2 + j1 < 0, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 44:
⊦ i = j → i - j = 0
Proof step 45:
2 * 2 ^ i = 2 * 2 ^ i, 1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + 0 + 2 ^ i * j1) / (2 * 2 ^ i), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1 < i, 0 < i, (2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-abs, name:sub-eq-01, seq: ⊦ i = j → i - j = 0, subst:[j, i] → [2 * 2 ^ i, 2 * 2 ^ i], <all paths>

Additional information

Used terms: 2 * 2 ^ i, 2 * 2 ^ i

Proof step 44 from proof div-div-rec (previous step) (back to tree)

⊦ i = j → i - j = 0

A spec-lemma

Proof step 45 from proof div-div-rec (previous step) (back to tree)

2 * 2 ^ i = 2 * 2 ^ i, 1 = 1, i1 ≠ (j0 + 2 ^ i * i1 * 2 + 0 + 2 ^ i * j1) / (2 * 2 ^ i), i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, j0 + 2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1 < i, 0 < i, (2 ^ i * i1 * 2 + 2 * 2 ^ i + 2 ^ i * j1) + (j0 - 1) < 0, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule simplifier

And obtained the following new goals

Proof step 46:
i1 ≠ (2 ^ i * (i1 * 2 + j1) + j0) / (2 * 2 ^ i), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * j + i * j0 = i * (j + j0); (s) ⊦ i * j + i = i * (j + 1); (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i + (j - i0) = i + j - i0; (s) ⊦ i + 0 = i; (s)

Proof step 46 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (i1 * 2 + j1) + j0) / (2 * 2 ^ i), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (i1 * 2 + j1) + 1 < i, i1 < i, j1 < i, i1 * 2 + j1 < 0, abs(j1) < 2, 2 ^ i * ((i1 * 2 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 47:
⊦ i * j = j * i
Proof step 48:
i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 * 2 ^ i), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦

Rule argument

spec: int-mult, name:commutativity, seq: ⊦ i * j = j * i, subst:[j, i] → [2, i1], <all paths>

Additional information

Used terms: 2, i1

Proof step 47 from proof div-div-rec (previous step) (back to tree)

⊦ i * j = j * i

A spec-lemma

Proof step 48 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 * 2 ^ i), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 49:
⊦ i + j = j + i
Proof step 50:
i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 * 2 ^ i), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-basic2, name:add-c, seq: ⊦ i + j = j + i, subst:[j, i] → [2 * i1, j1], <all paths>

Additional information

Used simplifier rules: add-c: ⊦ i + j = j + i; from specification int-basic2 Used terms: 2 * i1, j1

Proof step 49 from proof div-div-rec (previous step) (back to tree)

⊦ i + j = j + i

A spec-lemma

Proof step 50 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 * 2 ^ i), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 51:
⊦ i * (j + j0) = i * j + i * j0
Proof step 52:
i1 ≠ ((2 ^ i * 2 * i1 + 2 ^ i * j1) + j0) / (2 * 2 ^ i), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦

Rule argument

spec: int-mult, name:dist-rsplit, seq: ⊦ i * (j + j0) = i * j + i * j0, subst:[j0, j, i] → [j1, 2 * i1, 2 ^ i], <all paths>

Additional information

Used terms: j1, 2 * i1, 2 ^ i

Proof step 51 from proof div-div-rec (previous step) (back to tree)

⊦ i * (j + j0) = i * j + i * j0

A spec-lemma

Proof step 52 from proof div-div-rec (previous step) (back to tree)

i1 ≠ ((2 ^ i * 2 * i1 + 2 ^ i * j1) + j0) / (2 * 2 ^ i), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 53:
⊦ i + j + i0 = (i + j) + i0
Proof step 54:
i1 ≠ (2 ^ i * 2 * i1 + 2 ^ i * j1 + j0) / (2 * 2 ^ i), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-basic2, name:add-a, seq: ⊦ i + j + i0 = (i + j) + i0, subst:[i0, j, i] → [j0, 2 ^ i * j1, 2 ^ i * 2 * i1], <rotated> <all paths>

Additional information

Used terms: j0, 2 ^ i * j1, 2 ^ i * 2 * i1

Proof step 53 from proof div-div-rec (previous step) (back to tree)

⊦ i + j + i0 = (i + j) + i0

A spec-lemma

Proof step 54 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * 2 * i1 + 2 ^ i * j1 + j0) / (2 * 2 ^ i), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 55:
⊦ i * j * j0 = (i * j) * j0
Proof step 56:
i1 ≠ ((2 ^ i * 2) * i1 + 2 ^ i * j1 + j0) / (2 * 2 ^ i), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦

Rule argument

spec: int-mult, name:associativity, seq: ⊦ i * j * j0 = (i * j) * j0, subst:[j0, j, i] → [i1, 2, 2 ^ i], <all paths>

Additional information

Used terms: i1, 2, 2 ^ i

Proof step 55 from proof div-div-rec (previous step) (back to tree)

⊦ i * j * j0 = (i * j) * j0

A spec-lemma

Proof step 56 from proof div-div-rec (previous step) (back to tree)

i1 ≠ ((2 ^ i * 2) * i1 + 2 ^ i * j1 + j0) / (2 * 2 ^ i), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 57:
⊦ i * j = j * i
Proof step 58:
i1 ≠ ((2 ^ i * 2) * i1 + 2 ^ i * j1 + j0) / (2 ^ i * 2), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-mult, name:commutativity, seq: ⊦ i * j = j * i, subst:[j, i] → [2 ^ i, 2], <all paths>

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: 2 ^ i, 2

Proof step 57 from proof div-div-rec (previous step) (back to tree)

⊦ i * j = j * i

A spec-lemma

Proof step 58 from proof div-div-rec (previous step) (back to tree)

i1 ≠ ((2 ^ i * 2) * i1 + 2 ^ i * j1 + j0) / (2 ^ i * 2), 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 59:
⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 ∧ abs(i0) < j → (j * i + i0) / j = i
Proof step 60:
i1 ≠ ((2 ^ i * 2) * i1 + 2 ^ i * j1 + j0) / (2 ^ i * 2), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦ 0 < 2 ^ i * 2 ∧ i1 ≤ 0 ∧ 2 ^ i * j1 + j0 ≤ 0 ∧ abs(2 ^ i * j1 + j0) < 2 ^ i * 2

Rule argument

spec: int-div, name:div-mult-neg, seq: ⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 ∧ abs(i0) < j → (j * i + i0) / j = i, subst:[i0, i, j] → [2 ^ i * j1 + j0, i1, 2 ^ i * 2], <all paths>

Additional information

Used terms: 2 ^ i * j1 + j0, i1, 2 ^ i * 2

Proof step 59 from proof div-div-rec (previous step) (back to tree)

⊦ 0 < j ∧ i ≤ 0 ∧ i0 ≤ 0 ∧ abs(i0) < j → (j * i + i0) / j = i

A spec-lemma

Proof step 60 from proof div-div-rec (previous step) (back to tree)

i1 ≠ ((2 ^ i * 2) * i1 + 2 ^ i * j1 + j0) / (2 ^ i * 2), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0 ⊦ 0 < 2 ^ i * 2 ∧ i1 ≤ 0 ∧ 2 ^ i * j1 + j0 ≤ 0 ∧ abs(2 ^ i * j1 + j0) < 2 ^ i * 2

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 61:
i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * j1 + j0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0), 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: pot2-pos: ⊦ 0 < 2 ^ i ↔ 0 ≤ i; two-lsz: ⊦ ¬ 2 ^ i < 0; ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i ≤ 0 → (0 < i * j ↔ j < 0 ∧ i ≠ 0); (s) ⊦ i < i + j ↔ 0 < j; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s) ⊦ i * j + i * j0 = i * (j + j0); (s)

Proof step 61 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * j1 + j0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, abs(j1) < 2, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0), 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 62:
⊦ i ≠ 1 ∧ 0 ≤ i → (i < 2 ↔ i = 0)
Proof step 63:
i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * j1 + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0) ⊦ abs(j1) ≠ 1 ∧ 0 ≤ abs(j1)

Rule argument

spec: int-abs, name:lstwo, seq: ⊦ i ≠ 1 ∧ 0 ≤ i → (i < 2 ↔ i = 0), subst:[i] → [abs(j1)], <all paths>

Additional information

Used simplifier rules: ls-mult-2pot: ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0 → (j * 2 ^ i < 2 ^ i0 ↔ j < 2 ^ (i0 - i)); ⊦ abs(i) = 0 ↔ i = 0; (s) ⊦ 0 ≤ abs(i); (s) ⊦ 0 < i → (i * j < 0 ↔ j < 0); (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i * 0 = 0; (s) ⊦ 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 forward-lels: ⊦ 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 forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs 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 - i = 0; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: abs(j1)

Proof step 62 from proof div-div-rec (previous step) (back to tree)

⊦ i ≠ 1 ∧ 0 ≤ i → (i < 2 ↔ i = 0)

A spec-lemma

Proof step 63 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, abs(j1) < 2, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * j1 + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0) ⊦ abs(j1) ≠ 1 ∧ 0 ≤ abs(j1)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 64:
abs(j1) = 1, i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * j1 + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0) ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs forward-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 ⊦ 0 ≤ abs(i); (s)

Proof step 64 from proof div-div-rec (previous step) (back to tree)

abs(j1) = 1, i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, 2 * i1 + j1 < 0, j1 < i, i1 < i, (2 * i1 + j1) + 1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 2 ^ i * j1 + j0 < i, j0 ≤ 0, 0 ≤ i, j1 ≤ 0, i1 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0) ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 65:
⊦ j < 0 → abs(j) = 0 - j
Proof step 66:
0 - j1 = 1, i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * j1 + j0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, j1 < 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0), 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Rule argument

spec: int-abs, name:Abs-neg, seq: ⊦ j < 0 → abs(j) = 0 - j, subst:[j] → [j1], <all paths>

Additional information

Used simplifier rules: ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i = 1 → i * j = j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) forward-lels: ⊦ 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 forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs Used terms: j1

Proof step 65 from proof div-div-rec (previous step) (back to tree)

⊦ j < 0 → abs(j) = 0 - j

A spec-lemma

Proof step 66 from proof div-div-rec (previous step) (back to tree)

0 - j1 = 1, i1 ≠ (2 ^ i * (2 * i1 + j1) + j0) / (2 ^ i * 2), 2 ^ i * j1 + j0 < i, 2 ^ i * (2 * (i1 + 1) + j1) + j0 < i, 0 < i, abs(j0) < 2 ^ i, j0 < i, (2 * i1 + j1) + 1 < i, i1 < i, j1 < i, 2 * i1 + j1 < 0, 2 ^ i * ((2 * i1 + j1) + 1) + j0 < 0, j1 < 0, 2 ^ i * 2 ≤ abs(2 ^ i * j1 + j0), 2 ^ i * j1 + j0 ≤ 0, 2 ^ i * (2 * (i1 + 1) + j1) + j0 ≤ 0, i1 ≤ 0, j1 ≤ 0, 0 ≤ i, j0 ≤ 0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 67:
i1 ≠ (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2), 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, 2 ^ i * 2 * i1 + j0 < 0, i1 < i, 2 * i1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, j0 < 2 ^ i + i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0, j0 ≤ 2 ^ i, 2 ^ i * 2 ≤ abs(j0 - 2 ^ i), j0 ≤ 0, 0 ≤ i, i1 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (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 < 0 ⊦ (* i) + j = j - ~ i; (s) ⊦ i + 0 = i; (s) ⊦ i - j ≤ i0 ↔ i ≤ j + i0; (s) ⊦ i + ~ j = i - j; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ i * ~1 = ~ i; (s) ⊦ i < 1 ↔ i ≤ 0; (s) ⊦ 0 < i ∧ 0 ≤ j → ((* i) * i0 < (* j) ↔ i0 < (i + j - 1) / i); (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ 0 - i = ~ i; (s)

Proof step 67 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2), 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, 2 ^ i * 2 * i1 + j0 < 0, i1 < i, 2 * i1 < i, j0 < i, abs(j0) < 2 ^ i, 0 < i, j0 < 2 ^ i + i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0, j0 ≤ 2 ^ i, 2 ^ i * 2 ≤ abs(j0 - 2 ^ i), j0 ≤ 0, 0 ≤ i, i1 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 68:
⊦ j < 0 → abs(j) = 0 - j
Proof step 69:
i1 ≠ (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2), j0 < 2 ^ i + i, 0 < i, abs(j0) < 2 ^ i, j0 < i, 2 * i1 < i, i1 < i, 2 ^ i * 2 * i1 + j0 < 0, 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, j0 - 2 ^ i < 0, i1 ≤ 0, 0 ≤ i, j0 ≤ 0, 2 ^ i * 2 ≤ 0 - (j0 - 2 ^ i), j0 ≤ 2 ^ i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0 ⊦

Rule argument

spec: int-abs, name:Abs-neg, seq: ⊦ j < 0 → abs(j) = 0 - j, subst:[j] → [j0 - 2 ^ i], <all paths>

Additional information

Used simplifier rules: two-zero: ⊦ 0 ≤ j → 2 ^ j ≠ 0; ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i + 0 = i; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ i * j + i = i * (j + 1); (s) ⊦ 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 j ≠ 0, i0 ≠ 0 ⊦ (i * i0) / (j * i0) = i / j; (s) j ≠ 0 ⊦ (i * j) / j = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0 - 2 ^ i

Proof step 68 from proof div-div-rec (previous step) (back to tree)

⊦ j < 0 → abs(j) = 0 - j

A spec-lemma

Proof step 69 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2), j0 < 2 ^ i + i, 0 < i, abs(j0) < 2 ^ i, j0 < i, 2 * i1 < i, i1 < i, 2 ^ i * 2 * i1 + j0 < 0, 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, j0 - 2 ^ i < 0, i1 ≤ 0, 0 ≤ i, j0 ≤ 0, 2 ^ i * 2 ≤ 0 - (j0 - 2 ^ i), j0 ≤ 2 ^ i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0 ⊦

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 70:
i1 ≠ (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2), 2 ^ i + j0 < i, j0 < 2 ^ i, j0 < 2 ^ i + i, 0 < i, abs(j0) < 2 ^ i, j0 < i, 2 * i1 < i, i1 < i, 2 ^ i * 2 * i1 + j0 < 0, 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, i1 ≤ 0, 0 ≤ i, j0 ≤ 0, 2 ^ i + j0 ≤ 0, j0 ≤ 2 ^ i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (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 + 0 = i; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 1 * i = i; (s) ⊦ (* i1) * j + i ≤ j ↔ (i1 - 1) * j + i ≤ 0; (s) ⊦ i ≤ j - i0 ↔ i + i0 ≤ j; (s) ⊦ ~(i - j) = j - i; (s) ⊦ 0 - i = ~ i; (s)

Proof step 70 from proof div-div-rec (previous step) (back to tree)

i1 ≠ (2 ^ i * (2 * i1 - 1) + j0) / (2 ^ i * 2), 2 ^ i + j0 < i, j0 < 2 ^ i, j0 < 2 ^ i + i, 0 < i, abs(j0) < 2 ^ i, j0 < i, 2 * i1 < i, i1 < i, 2 ^ i * 2 * i1 + j0 < 0, 2 ^ i * (2 * (i1 + 1) - 1) + j0 < i, i1 ≤ 0, 0 ≤ i, j0 ≤ 0, 2 ^ i + j0 ≤ 0, j0 ≤ 2 ^ i, 2 ^ i * (2 * (i1 + 1) - 1) + j0 ≤ 0 ⊦

User applied rule apply rewrite lemma

And obtained the following new goals

Proof step 71:
⊦ j < 0 → abs(j) = 0 - j

Rule argument

spec: int-abs, name:Abs-neg, seq: ⊦ j < 0 → abs(j) = 0 - j, subst:[j] → [j0], <all paths>

Additional information

Used simplifier rules: two-zero: ⊦ 0 ≤ j → 2 ^ j ≠ 0; ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 - i = ~ i; (s) ⊦ ~ i < j ↔ 0 < j + i; (s) ⊦ i ≤ j → ¬ j < i; (s) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) lf-01: ⊦ i < j ∧ j < i0 → i +1 < i0; (forward) from specification int-basic1 j ≠ 0, i0 ≠ 0 ⊦ (i * i0) / (j * i0) = i / j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i +1 = i + 1; (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 ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) Used terms: j0

Proof step 1 from proof div-div-rec (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

Rule argument

Additional information

Proof step 2 from proof div-div-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Proof step 3 from proof div-div-rec (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

Rule argument

Additional information

Proof step 4 from proof div-div-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Proof step 5 from proof div-div-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

Rule argument

Additional information

Proof step 6 from proof div-div-rec (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof div-div-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Proof step 8 from proof div-div-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

Rule argument

Additional information

Proof step 9 from proof div-div-rec (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

Rule argument

Additional information

Proof step 10 from proof div-div-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Proof step 11 from proof div-div-rec (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

Rule argument

Additional information

Proof step 12 from proof div-div-rec (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Proof step 13 from proof div-div-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

Rule argument

Additional information

Proof step 14 from proof div-div-rec (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

Rule argument

Additional information

Proof step 15 from proof div-div-rec (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

Rule argument

Additional information

Proof step 16 from proof div-div-rec (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

Rule argument

Additional information

Proof step 17 from proof div-div-rec (previous step) (back to tree)

A spec-lemma

Proof step 18 from proof div-div-rec (previous step) (back to tree)