Proof step 1 from proof equal-minus-one (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i ^ j = ~1 ↔ i = ~1 ∧ j ≠ 0 ∧ abs(j) % 2 = 1), i ≠ 0 ∨ 0 ≤ j ⊦

Rule argument

Additional information

Proof step 2 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(i ^ j = ~1 ↔ i = ~1 ∧ j ≠ 0 ∧ abs(j) % 2 = 1), i ≠ 0 ∨ 0 ≤ j ⊦

Rule argument

Additional information

Proof step 3 from proof equal-minus-one (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 4:

  i ^ j = ~1, i ≠ 0 ∨ 0 ≤ j ⊦ i = ~1 ∧ j ≠ 0 ∧ abs(j) % 2 = 1

• Proof step 50:

  abs(j) % 2 = 1, i = ~1, i ^ j ≠ ~1, j ≠ 0, i ≠ 0 ∨ 0 ≤ j ⊦

Rule argument

Additional information

Proof step 4 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i ^ j = ~1, j ≠ 0, i ≠ 0 ∨ 0 < j ⊦ abs(j) % 2 = 1 ∧ i = ~1

Rule argument

Additional information

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

Proof step 5 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  i ^ j = ~1, i = ~1, j ≠ 0, i ≠ 0 ∨ 0 < j ⊦ abs(j) % 2 = 1 ∧ i = ~1

• Proof step 11:

  i ^ j = ~1, i ≠ ~1, j ≠ 0, i ≠ 0 ∨ 0 < j ⊦ abs(j) % 2 = 1 ∧ i = ~1

Rule argument

Additional information

Used formulas: i = ~1

Proof step 6 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  ~1 ^ j = ~1, abs(j) % 2 ≠ 1, j ≠ 0 ⊦

Rule argument

Additional information

Proof step 7 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  ~1 ^ j = ~1, abs(j) % 2 ≠ 1, j ≠ 0, ¬ 0 < j ⊦

Rule argument

Additional information

Used simplifier rules: minus-one-even: ⊦ 0 < j ∧ j % 2 = 0 → ~1 ^ j = 1; ⊦ 0 < j → abs(j) = j; (s) ⊦ 0 < i → (i % 2 = 1 ↔ i % 2 ≠ 0); (ss) Used formulas: 0 < j

Proof step 8 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  j % 2 = 0, 1 / ~1 ^ ~ j = ~1, j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: Pot-neg: ⊦ i < 0 → j ^ i = 1 / j ^ abs(i); forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i < j → ¬ j < 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 < 0 → (j % 2 = ~1 ↔ j % 2 ≠ 0); (ss) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) ⊦ ~ i = j ↔ i + j = 0; (s) j ≠ 0 ⊦ ~ i % j = ~(i % j); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss)

Proof step 9 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ 0 < j ∧ j % 2 = 0 → ~1 ^ j = 1

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < ~ i ↔ i < 0; (s) j ≠ 0 ⊦ ~ i % j = ~(i % j); (s) ⊦ ~ i = 0 ↔ i = 0; (s) Used terms: ~ j

Proof step 10 from proof equal-minus-one (previous step) (back to tree)

Lemma minus-one-even

Proof step 11 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  i ^ j = ~1, i ≠ ~1, j ≠ 0, i ≠ 0 ∨ 0 < j ⊦

Rule argument

Additional information

Proof step 12 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 13:

  i ^ j = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, i ≠ 0 ∨ 0 < j ⊦

Rule argument

Additional information

Used simplifier rules: zero-01: ⊦ 0 < j → 0 ^ j = 0; Used formulas: i = 0

Proof step 13 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  i ^ j = ~1, i ≠ 0, i ≠ ~1, j ≠ 0 ⊦

Rule argument

Additional information

Proof step 14 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ i < 0 → j ^ i = 1 / j ^ abs(i)

• Proof step 16:

  i ^ j = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, ¬ j < 0 ⊦

• Proof step 30:

  1 / i ^ abs(j) = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 15 from proof equal-minus-one (previous step) (back to tree)

Lemma Pot-neg

Proof step 16 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 17:

  i ^ j = ~1, i ≠ 0, i ≠ ~1, 0 < j ⊦

Rule argument

Additional information

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

Proof step 17 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 19:

  i ^ j -1 * i = ~1, i ≠ 0, i ≠ ~1, 0 < j ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 18 from proof equal-minus-one (previous step) (back to tree)

Lemma Pot-pos

Proof step 19 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 20:

  i + i ^ (j - 1) = 0, abs(i ^ (j - 1)) = 1, i ≠ 0, i ≠ ~1, 0 < j ⊦

Rule argument

Additional information

Used simplifier rules: commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ i * j = ~1 ↔ abs(i) = 1 ∧ i = ~ j; (ws) ⊦ i -1 = i - 1; (s)

Proof step 20 from proof equal-minus-one (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 21:

  i + i ^ i0 = 0, abs(i ^ i0) = 1, j = i0 + 1, i ≠ 0, i ≠ ~1, 0 < j ⊦

Rule argument

Additional information

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

Proof step 21 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 22:

  i + i ^ i0 = 0, abs(i ^ i0) = 1, i ≠ 0, i ≠ ~1, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-01: ⊦ 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 ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s)

Proof step 22 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 23:

  i + i ^ i0 = 0, abs(i ^ i0) = 1, i ≠ 0, i ≠ ~1, i0 ≠ 0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: Pot-zero: ⊦ j ^ 0 = 1; ⊦ (* j) = i0 + (* j0) ↔ j - j0 = 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: i0 = 0

Proof step 23 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 24:

  i + i ^ i0 = 0, abs(i ^ i0) = 1, i ≠ 0, i ≠ ~1, i0 ≠ 0, 0 < i0 ⊦

Rule argument

Additional information

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

Proof step 24 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 25:

  i + i ^ i0 = 0, i ^ i0 = ~ i, abs(i ^ i0) = 1, i ≠ 0, i ≠ ~1, i0 ≠ 0, 0 < i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i = j ↔ i + j = 0; (s) Used formulas: i ^ i0 = ~ i

Proof step 25 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 26:

  i + i ^ i0 = 0, i ^ i0 = ~ i, abs(i ^ i0) = 1, i ≠ 0, i ≠ ~1, i0 ≠ 0, 0 < i0, i < 0 ⊦

• Proof step 27:

  i + i ^ i0 = 0, i ^ i0 = ~ i, abs(i ^ i0) = 1, i ≠ 0, i ≠ ~1, i0 ≠ 0, 0 < i0, ¬ i < 0 ⊦

Rule argument

Additional information

Used formulas: i < 0

Proof step 26 from proof equal-minus-one (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ abs(~ i) = abs(i); (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) ⊦ ~ i + i = 0; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

Proof step 27 from proof equal-minus-one (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 28:

  i + ~ i = 0, i ^ i0 = ~ i, abs(~ i) = 1, i ≠ 0, i ≠ ~1, i0 ≠ 0, 0 < i0, ¬ i < 0 ⊦

Rule argument

Additional information

Proof step 28 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

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

Rule argument

Additional information

Used simplifier rules: one-01: ⊦ 1 ^ j = 1; ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ 0 - i = ~ i; (s) ⊦ ~ ~ i = i; (s) ⊦ ~ i + i = 0; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ ~ i < 0 ↔ 0 < i; (s) ⊦ i < j → ¬ j < i; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (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 ⊦ abs(~ i) = abs(i); (s) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: ~ i

Proof step 29 from proof equal-minus-one (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  1 / i ^ ~ j = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i < 0 → abs(i) = ~ i; (s)

Proof step 31 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  0 < j, j ≤ i ⊦ i / j = (i - j) / j + 1

• Proof step 33:

  1 / i ^ ~ j = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦ 0 < i ^ ~ j ∧ i ^ ~ j ≤ 1

Rule argument

Additional information

Used simplifier rules: ⊦ i + 1 = ~1 ↔ i + 1 + 1 = 0; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = 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 = 1); (s) ⊦ i = j → i - j = 0; (s) j ≠ 0 ⊦ 0 / j = 0; (s) Used terms: i ^ ~ j, 1

Proof step 32 from proof equal-minus-one (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 34:

  1 / i ^ ~ j = ~1, i ≠ ~1, i ≠ 0, j ≠ 0, j < 0, i ^ ~ j ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-04: ⊦ j ≤ i ∧ i ≤ 0 → j ≤ 0; (forward) from specification int-abs j0 ≠ 0, j ≤ j0 ⊦ i ≤ (* j) → i ≤ (* j0); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ 1 < j → 1 / j = 0; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss)

Proof step 34 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 35:

  1 / i ^ ~ j = ~1, i ≠ ~1, i ≠ 0, j ≠ 0, j < 0, i ^ ~ j < 0, i ^ ~ j ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: zero-02: ⊦ j < 0 → (i ^ ~ j = 0 ↔ i = 0); ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) Used formulas: i ^ ~ j < 0

Proof step 35 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 36:

  1 / i ^ ~ j = ~1, i ≠ ~1, i ≠ 0, j ≠ 0, j < 0, i ^ ~ j < 0 ⊦

Rule argument

Additional information

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

Proof step 36 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ j < 0 → i / (* j) = ~(i / ~ j)

• Proof step 38:

  ~(1 / ~(i ^ ~ j)) = ~1, i ≠ ~1, i ≠ 0, j ≠ 0, j < 0, i ^ ~ j < 0 ⊦

Rule argument

Additional information

Used terms: i ^ ~ j, 1

Proof step 37 from proof equal-minus-one (previous step) (back to tree)

A spec-lemma

Proof step 38 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  0 < j, j ≤ i ⊦ i / j = (i - j) / j + 1

• Proof step 40:

  ~(1 / ~(i ^ ~ j)) = ~1, i ≠ ~1, i ≠ 0, j ≠ 0, i ^ ~ j < 0, j < 0 ⊦ 0 < ~(i ^ ~ j) ∧ ~(i ^ ~ j) ≤ 1

• Proof step 43:

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

Rule argument

Additional information

Used terms: ~(i ^ ~ j), 1

Proof step 39 from proof equal-minus-one (previous step) (back to tree)

A spec-lemma

Proof step 40 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 41:

  1 / i ^ ~ j = ~1, i ^ ~ j ≠ ~1, i ≠ ~1, i ≠ 0, j ≠ 0, j < 0, i ^ ~ j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: zero-02: ⊦ j < 0 → (i ^ ~ j = 0 ↔ i = 0); add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); (s) ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ ~ i ≤ j ↔ 0 ≤ i + j; (s) ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ ~ ~ i = i; (s) j ≠ 0 ⊦ i / ~ j = ~(i / j); (s)

Proof step 41 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 42:

  abs(i) < abs(j) ⊦ i / j = 0

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i < ~ j ↔ i + j < 0; (s) ⊦ i + (* j) < (* j0) ↔ i < j0 - j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i < 0 → (~1 ≤ i ↔ i = ~1); (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: i ^ ~ j, 1

Proof step 42 from proof equal-minus-one (previous step) (back to tree)

A spec-lemma

Proof step 43 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 44:

  i ^ ~ j = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

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

Proof step 44 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 45:

  ⊦ 0 < i → j ^ i = j ^ i -1 * j

• Proof step 46:

  i ^ (~ j)-1 * i = ~1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0, 0 < ~ j ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < ~ i ↔ i < 0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≠ j → (i ≤ j ↔ i < j); (s) ⊦ i < j → ¬ j < i; (s) Used terms: ~ j, i

Proof step 45 from proof equal-minus-one (previous step) (back to tree)

Lemma Pot-pos

Proof step 46 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 47:

  i + i ^ ~(j + 1) = 0, abs(i ^ ~(j + 1)) = 1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ 0 < ~ i ↔ i < 0; (s) commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ i * j = ~1 ↔ abs(i) = 1 ∧ i = ~ j; (ws) ⊦ ~ i - j = ~(i + j); (s) ⊦ i -1 = i - 1; (s)

Proof step 47 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 48:

  i + i ^ ~(j + 1) = 0, i ^ ~(j + 1) = ~ i, abs(i ^ ~(j + 1)) = 1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i = j ↔ i + j = 0; (s) Used formulas: i ^ ~(j + 1) = ~ i

Proof step 48 from proof equal-minus-one (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 49:

  i + ~ i = 0, i ^ ~(j + 1) = ~ i, abs(~ i) = 1, i ≠ 0, i ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

Proof step 49 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: one-01: ⊦ 1 ^ j = 1; ⊦ abs(~ i) = abs(i); (s) ⊦ ¬ j < 0 → abs(j) = j; (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ ~ i + i = 0; (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ i < j → ¬ j < i; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (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 ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = i0; (s) Used formulas: i < 0

Proof step 50 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  abs(j) % 2 = 1, ~1 ^ j ≠ ~1, j ≠ 0 ⊦

Rule argument

Additional information

Proof step 51 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 52:

  ⊦ 0 < j ∧ j % 2 = 1 → ~1 ^ j = ~1

• Proof step 53:

  abs(j) % 2 = 1, ~1 ^ j ≠ ~1, j ≠ 0 ⊦ 0 < j ∧ j % 2 = 1

Rule argument

Additional information

Used terms: j

Proof step 52 from proof equal-minus-one (previous step) (back to tree)

Lemma minus-one-odd

Proof step 53 from proof equal-minus-one (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 54:

  ~1 = j % 2, 1 / ~1 ^ ~ j ≠ ~1, j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: minus-one-odd: ⊦ 0 < j ∧ j % 2 = 1 → ~1 ^ j = ~1; Pot-neg: ⊦ i < 0 → j ^ i = 1 / j ^ abs(i); forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i < j → ¬ j < i; (s) ⊦ i < 0 → 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 = j ↔ i + j = 0; (s) j ≠ 0 ⊦ ~ i % j = ~(i % j); (s) ⊦ ¬ i < j → (i = j ↔ ¬ j < i); (ss) ⊦ 0 < j → abs(j) = j; (s)

Proof step 54 from proof equal-minus-one (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 55:

  ~1 = j % 2, 1 / ~1 ^ ~ j ≠ ~1, j ≠ 0, j < 0 ⊦

Rule argument

Additional information

Used formulas: j = 0

Proof step 55 from proof equal-minus-one (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ⊦ 0 < j ∧ j % 2 = 1 → ~1 ^ j = ~1

Rule argument

Additional information

Used simplifier rules: j ≠ 0 ⊦ ~ i % j = ~(i % j); (s) ⊦ ~ i = j ↔ i + j = 0; (s) ⊦ (* j) = i0 + (* j0) ↔ j - j0 = 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 < 0; (s) Used terms: ~ j

Proof step 56 from proof equal-minus-one (previous step) (back to tree)

Lemma minus-one-odd