Proof step 1 from proof modzero-08 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  0 < i, abs(j0) < j, i * j + j0 ≤ 0 ⊦

Rule argument

Additional information

Proof step 2 from proof modzero-08 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  abs(j0) < j, i * j + j0 < i, 0 < i, i * j + j0 ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: 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-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs

Proof step 3 from proof modzero-08 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  i * j + j0 = 0, 0 < i, i * j + j0 < i, abs(j0) < j, i * j + j0 ≤ 0 ⊦

• Proof step 11:

  i * j + j0 ≠ 0, 0 < i, i * j + j0 < i, abs(j0) < j, i * j + j0 ≤ 0 ⊦

Rule argument

Additional information

Used formulas: i * j + j0 = 0

Proof step 4 from proof modzero-08 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i * j + j0 = 0, 0 < i, abs(j0) < j ⊦

Rule argument

Additional information

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

Proof step 5 from proof modzero-08 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  ⊦ i + j = 0 ↔ j = ~ i

• Proof step 7:

  j0 = ~(i * j), abs(j0) < j, 0 < i ⊦

Rule argument

Additional information

Used terms: j0, i * j

Proof step 6 from proof modzero-08 (previous step) (back to tree)

A spec-lemma

Proof step 7 from proof modzero-08 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 8:

  0 < i, abs(~(i * j)) < j ⊦

Rule argument

Additional information

Proof step 8 from proof modzero-08 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  0 < i, i * abs(j) < j ⊦

Rule argument

Additional information

Used simplifier rules: abs-eqall: ⊦ abs(i * j) = abs(i) * abs(j); associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ 0 < j → abs(j) = j; (s) ⊦ abs(~ i) = abs(i); (s)

Proof step 9 from proof modzero-08 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ 0 < i → ¬ i * abs(j) < j

Rule argument

Additional information

Used terms: j, i

Proof step 10 from proof modzero-08 (previous step) (back to tree)

Lemma mods-nls

Proof step 11 from proof modzero-08 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  i * j + j0 ≠ 0, abs(j0) < j, i * j + j0 < i, 0 < i, i * j + j0 < 0 ⊦

Rule argument

Additional information

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

Proof step 12 from proof modzero-08 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ 0 < i ∧ abs(j0) < j → ¬ i * j + j0 < 0

Rule argument

Additional information

Used terms: j0, j, i

Proof step 13 from proof modzero-08 (previous step) (back to tree)

Lemma modzero