Proof step 1 from proof modmod-mult-07 (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  (i % j * i0) % j ≠ (i * i0) % j, 0 < j ⊦

Rule argument

Additional information

Proof step 2 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 3:

  0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j * i0) % j = (i * i0) % j

• Proof step 4:

  (i % j * i0) % j ≠ (i * i0) % j, 0 < j ⊦ 0 < j ∧ 0 ≤ i ∧ 0 ≤ i0

Rule argument

Additional information

Used terms: i0, j, i

Proof step 3 from proof modmod-mult-07 (previous step) (back to tree)

Lemma modmod-mult-08

Proof step 4 from proof modmod-mult-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (i % j * i0) % j ≠ (i * i0) % j, 0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0

Rule argument

Additional information

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

Proof step 5 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  (i % j * i0) % j ≠ (i * i0) % j, 0 < j, i < 0 ⊦ 0 ≤ i ∧ 0 ≤ i0

• Proof step 22:

  (i % j * i0) % j ≠ (i * i0) % j, 0 < j, ¬ i < 0 ⊦ 0 ≤ i ∧ 0 ≤ i0

Rule argument

Additional information

Used formulas: i < 0

Proof step 6 from proof modmod-mult-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  (i % j * i0) % j ≠ (i * i0) % j, 0 < j, i < 0 ⊦

Rule argument

Additional information

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

Proof step 7 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  j ≠ 0 ⊦ i < 0 → (* i) % j = ~(~ i % j)

• Proof step 9:

  (~(~ i % j) * i0) % j ≠ (i * i0) % j, j ≠ 0, 0 < j, i < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) Used terms: j, i

Proof step 8 from proof modmod-mult-07 (previous step) (back to tree)

Lemma modnum-neg

Proof step 9 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ~ i * j = ~(i * j)

• Proof step 11:

  ~(~ i % j * i0) % j ≠ (i * i0) % j, j ≠ 0, i < 0, 0 < j ⊦

Rule argument

Additional information

Used terms: i0, ~ i % j

Proof step 10 from proof modmod-mult-07 (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  j ≠ 0 ⊦ ~ i % j = ~(i % j)

• Proof step 13:

  j ≠ 0, ~((~ i % j * i0) % j) ≠ (i * i0) % j, 0 < j, i < 0 ⊦

Rule argument

Additional information

Used terms: j, ~ i % j * i0

Proof step 12 from proof modmod-mult-07 (previous step) (back to tree)

Lemma mod-neg-01

Proof step 13 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 14:

  0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j * i0) % j = (i * i0) % j

• Proof step 15:

  j ≠ 0, ~((~ i % j * i0) % j) ≠ (i * i0) % j, i < 0, 0 < j ⊦ 0 < j ∧ 0 ≤ ~ i ∧ 0 ≤ i0

Rule argument

Additional information

Used simplifier rules: mod-neg-01: j ≠ 0 ⊦ ~ i % j = ~(i % j); ⊦ ~ i * j = ~(i * j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ ~ ~ i = i; (s) Used terms: i0, j, ~ i

Proof step 14 from proof modmod-mult-07 (previous step) (back to tree)

Lemma modmod-mult-08

Proof step 15 from proof modmod-mult-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 16:

  (i % j * i0) % j ≠ (i * i0) % j, j ≠ 0, i < 0, 0 < j, i0 < 0, i ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: mod-neg-01: j ≠ 0 ⊦ ~ i % j = ~(i % j); forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 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 ⊦ i + 0 = i; (s) ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) ⊦ ~ ~ i = i; (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); (s)

Proof step 16 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 17:

  j ≠ 0 ⊦ i < 0 → (* i) % j = ~(~ i % j)

• Proof step 18:

  (~(~ i % j) * i0) % j ≠ (i * i0) % j, j ≠ 0, i0 < 0, 0 < j, i < 0, i ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) Used terms: j, i

Proof step 17 from proof modmod-mult-07 (previous step) (back to tree)

Lemma modnum-neg

Proof step 18 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 19:

  ~(~ i % j) * i0 = ~ i % j * ~ i0, (~(~ i % j) * i0) % j ≠ (i * i0) % j, j ≠ 0, i < 0, 0 < j, i0 < 0, i ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: mod-neg-01: j ≠ 0 ⊦ ~ i % j = ~(i % j); ⊦ ~ i * j = ~(i * j); (s) ⊦ ~ ~ i = i; (s) ⊦ i < 0 → (i * j = i * j0 ↔ j = j0); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: ~(~ i % j) * i0 = ~ i % j * ~ i0

Proof step 19 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 20:

  (~ i % j * ~ i0) % j ≠ (i * i0) % j, j ≠ 0, i0 < 0, 0 < j, i < 0, i ≤ 0 ⊦

Rule argument

Additional information

Proof step 20 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j * i0) % j = (i * i0) % j

Rule argument

Additional information

Used simplifier rules: mod-neg-01: j ≠ 0 ⊦ ~ i % j = ~(i % j); ⊦ ~ i * j = ~(i * j); (s) ⊦ ~ ~ i = i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i ≤ ~ j ↔ i + j ≤ 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 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: ~ i0, j, ~ i

Proof step 21 from proof modmod-mult-07 (previous step) (back to tree)

Lemma modmod-mult-08

Proof step 22 from proof modmod-mult-07 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  (i % j * i0) % j ≠ (i * i0) % j, i0 < 0, 0 < j, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) forward-le-01: ⊦ 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 forward-lsle: ⊦ i < j ∧ j ≤ j0 → i < j0; (forward) from specification int-abs ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 23 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 24:

  (i % j * i0) % j = ~(i % j * ~ i0) % j, (i % j * i0) % j ≠ (i * i0) % j, 0 < j, i0 < 0, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i * j = ~(i * j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ ~ ~ i = i; (s) Used formulas: (i % j * i0) % j = ~(i % j * ~ i0) % j

Proof step 24 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule subst equation

And obtained the following new goals

• Proof step 25:

  ~(i % j * ~ i0) % j ≠ (i * i0) % j, i0 < 0, 0 < j, 0 ≤ i ⊦

Rule argument

Additional information

Proof step 25 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 26:

  j ≠ 0 ⊦ ~ i % j = ~(i % j)

• Proof step 27:

  j ≠ 0, ~((i % j * ~ i0) % j) ≠ (i * i0) % j, 0 < j, i0 < 0, 0 ≤ i ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ ~ i * j = ~(i * j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ ~ ~ i = i; (s) Used terms: j, i % j * ~ i0

Proof step 26 from proof modmod-mult-07 (previous step) (back to tree)

Lemma mod-neg-01

Proof step 27 from proof modmod-mult-07 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 28:

  0 < j ⊦ 0 ≤ i ∧ 0 ≤ i0 → (i % j * i0) % j = (i * i0) % j

Rule argument

Additional information

Used simplifier rules: mod-neg-01: j ≠ 0 ⊦ ~ i % j = ~(i % j); mod-neg-01: j ≠ 0 ⊦ ~ i % j = ~(i % j); ⊦ ~ i * j = ~(i * j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ ~ ~ i = i; (s) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i ≤ ~ j ↔ i + j ≤ 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 ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ i < j → ¬ j < i; (s) Used terms: ~ i0, j, i

Proof step 28 from proof modmod-mult-07 (previous step) (back to tree)

Lemma modmod-mult-08