Proof step 1 from proof i2n-mod (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  i→n(i % j) ≠ i→n(i) % i→n(j), 0 < j, 0 ≤ i ⊦

Rule argument

Additional information

Proof step 2 from proof i2n-mod (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  i→n(i % j) ≠ i→n(i) % i→n(j), 0 < j, 0 ≤ i ⊦

Rule argument

Additional information

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

Proof step 3 from proof i2n-mod (previous step) (back to tree)

Heuristic elimination applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

  i = i0 * j + j0, i→n(j0) ≠ i→n(i) % i→n(j), 0 < j, j0 < j, 0 ≤ i, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

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

Proof step 4 from proof i2n-mod (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  i→n(j0) ≠ i→n(i0 * j + j0) % i→n(j), 0 < j, j0 < j, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs 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 ⊦ 0 ≤ j1 ∧ j1 < j → (0 ≤ i0 * j + j1 ↔ 0 ≤ i0); (s)

Proof step 5 from proof i2n-mod (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 6:

  0 ≤ i, 0 ≤ j ⊦ i→n(i + j) = i→n(i) + i→n(j)

• Proof step 7:

  i→n(j0) ≠ (i→n(i0 * j) + i→n(j0)) % i→n(j), j0 < j, 0 < j, 0 ≤ i0, 0 ≤ i0 * j, 0 ≤ j0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j0, i0 * j

Proof step 6 from proof i2n-mod (previous step) (back to tree)

Lemma add-01

Proof step 7 from proof i2n-mod (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  i→n(j0) ≠ (i→n(i0 * j) + i→n(j0)) % i→n(j), 0 < j, j0 < j, 0 ≤ j0, 0 ≤ i0 ⊦

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 ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ 0 < i → (0 ≤ i * j ↔ 0 ≤ j); (s)

Proof step 8 from proof i2n-mod (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ 0 ≤ i ∧ 0 ≤ j → i→n(i * j) = i→n(i) * i→n(j)

• Proof step 10:

  i→n(j0) ≠ (i→n(i0) * i→n(j) + i→n(j0)) % i→n(j), j0 < j, 0 < j, 0 ≤ j0, 0 ≤ i0, 0 ≤ j ⊦

Rule argument

Additional information

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

Proof step 9 from proof i2n-mod (previous step) (back to tree)

Lemma i2n-mult

Proof step 10 from proof i2n-mod (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  i→n(j0) ≠ i→n(j0) % i→n(j), 0 < j, j0 < j, 0 ≤ i0, 0 ≤ j0, 0 ≤ j ⊦

Rule argument

Additional information

Used simplifier rules: abs-zero: ⊦ i→n(i) = 0 ↔ i = 0; forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs c: ⊦ m + n = n + m; from specification nat-basic a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic mult-c: ⊦ m * n = n * m; from specification nat-mult mult-a: ⊦ m0 * m * n = (m0 * m) * n; from specification nat-mult n ≠ 0 ⊦ (m + n0 * n) % n = m % n; (s)

Proof step 11 from proof i2n-mod (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 12:

  ⊦ m < n → m % n = m

• Proof step 13:

  i→n(j0) ≠ i→n(j0) % i→n(j), j0 < j, 0 < j, 0 ≤ j, 0 ≤ j0, 0 ≤ i0, ¬ i→n(j0) < i→n(j) ⊦

Rule argument

Additional information

Used terms: i→n(j), i→n(j0)

Proof step 12 from proof i2n-mod (previous step) (back to tree)

A spec-lemma

Proof step 13 from proof i2n-mod (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 14:

  i→n(j0) ≠ i→n(j0) % i→n(j), 0 < j, j0 < j, 0 ≤ i0, 0 ≤ j0, 0 ≤ j, i→n(j) ≤ i→n(j0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)

Proof step 14 from proof i2n-mod (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 15:

  ⊦ i→n(i) ≤ i→n(j) ↔ abs(i) ≤ abs(j)

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < j → abs(j) = j; (s) ⊦ 0 ≤ i → abs(i) = i; (s) ⊦ i < j → (j ≤ i ↔ false); (as) Used terms: j0, j

Proof step 15 from proof i2n-mod (previous step) (back to tree)

Lemma labs-01