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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j ≠ 0, i % j < i0, i0 - 1 ≤ ~ abs(j) ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  j ≠ 0, i % j < i0, i0 + abs(j) ≤ 1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i ≤ j - i0 ↔ i + i0 ≤ 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 + ~ j = i - j; (s) ⊦ i - j ≤ i0 ↔ i ≤ j + i0; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  j ≠ 0, i % j < i0, abs(i % j) < abs(j), i0 + abs(j) ≤ 1 ⊦

• Proof step 20:

  j ≠ 0, i % j < i0, i0 + abs(j) ≤ 1, ¬ abs(i % j) < abs(j) ⊦

Rule argument

Additional information

Used formulas: abs(i % j) < abs(j)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

  j ≠ 0, abs(i % j) < j, i % j < i0, i0 + j ≤ 1, ¬ j < 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i - j ≤ i0 ↔ i ≤ j + i0; (s) ⊦ i < ~ j ↔ i + j < 0; (s) 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 < j + 1 ↔ i ≤ j; (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i + ~ j = i - j; (s) ⊦ i - j < i0 ↔ i < j + i0; (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; (s) Used terms: j

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  i % j < i0, abs(i % j) < j, 0 < j, i0 + j ≤ 1 ⊦

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 7 from proof mod-nls-04 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 8:

  0 < j, abs(i % j) < j, i % j < i0, i0 < 0, i0 + j ≤ 1 ⊦

• Proof step 17:

  0 < j, abs(i % j) < j, i % j < i0, i0 + j ≤ 1, ¬ i0 < 0 ⊦

Rule argument

Additional information

Used formulas: i0 < 0

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 9:

  ⊦ i ≠ j → (i ≤ j ↔ i ≤ j - 1)

• Proof step 10:

  i0 + j = 1, i0 < 0, i % j < i0, abs(i % j) < j, 0 < j, i0 + j ≤ 1 ⊦

• Proof step 12:

  i0 + j ≠ 1, i0 < 0, i % j < i0, abs(i % j) < j, 0 < j, i0 + j ≤ 1 - 1 ⊦

Rule argument

Additional information

Used terms: 1, i0 + j

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 11:

  i0 + j = 1, i0 < 0, i % j < i0, abs(i % j) < j, 0 < j ⊦

Rule argument

Additional information

Used simplifier rules: 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

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

User applied rule cut formula

And closed the goal!

Rule argument

Additional information

Used simplifier rules: mod-lezero: ⊦ 0 < j → ¬ j + i % j ≤ 0; ⊦ ~(i - 1) = ~ i + 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 ⊦ i - j = i0 ↔ i = i0 + j; (s) ⊦ i + (j - i) = j; (s) ⊦ i - j < i0 ↔ i < j + i0; (s) ⊦ i + 0 = i; (s) ⊦ i < j - i0 ↔ i + i0 < j; (s) ⊦ i < 1 ↔ i ≤ 0; (s) Used formulas: i0 = ~(j - 1)

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  i0 + j ≠ 1, i0 < 0, i % j < i0, abs(i % j) < j, 0 < j, i0 + j ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ 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 + j < j ↔ i < 0; (s) forward-le-02: ⊦ j < i ∧ i ≤ 0 → j < 0; (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

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

User applied rule cut formula

And obtained the following new goals

• Proof step 14:

  i0 + j ≠ 1, 0 < j, abs(i % j) < j, i % j < i0, i0 < 0, abs(i % j) < abs(i0), i0 + j ≤ 0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i < ~ j ↔ i + j < 0; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (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 ⊦ i < 0 ∧ 0 ≤ j → i < j; (s) ⊦ i + j ≤ i0 + j ↔ i ≤ i0; (s) ⊦ i < j → (j ≤ i ↔ false); (as) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 Used formulas: abs(i % j) < abs(i0)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 15:

  i0 + j ≠ 1, abs(i % j) < abs(i0), i0 < 0, i % j < i0, abs(i % j) < j, 0 < j, i0 + j ≤ 0, j ≤ abs(i0) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < ~ j ↔ i + j < 0; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i ≤ j → ¬ j < i; (s) Used formulas: j ≤ abs(i0)

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ i ≤ 0 ∧ j ≤ 0 → (abs(i) < abs(j) ↔ j < i)

Rule argument

Additional information

Used simplifier rules: mod-less-01: ⊦ 0 < j → i % j < j; ⊦ i < 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < 0 → abs(i) = ~ i; (s) ⊦ i ≤ ~ j ↔ i + j ≤ 0; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) ⊦ i < j → ¬ j < i; (s) ⊦ i < ~ j ↔ i + j < 0; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) ⊦ 0 < j → abs(j) = j; (s) forward-le-02: ⊦ 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-pos: ⊦ i < j ∧ 0 < i → 0 < j ∧ 1 < j; (forward) from specification int-basic1 forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs Used terms: i0, i % j

Proof step 16 from proof mod-nls-04 (previous step) (back to tree)

A spec-lemma

Proof step 17 from proof mod-nls-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 18:

  i % j < i0, abs(i % j) < j, 0 < j, i0 + j ≤ 1, 0 ≤ i0 ⊦

Rule argument

Additional information

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

Proof step 18 from proof mod-nls-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 19:

  ⊦ i ≠ j → (i ≤ j ↔ i ≤ j - 1)

Rule argument

Additional information

Used simplifier rules: one-01: ⊦ i = 1 → j % i = 0; 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 ⊦ i + j < j ↔ i < 0; (s) ⊦ i ≤ j → ¬ j < i; (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 ∧ 0 ≤ j → (1 = i + j ↔ i = 1 ∧ j = 0); (ws) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs Used terms: 1, i0 + j

Proof step 19 from proof mod-nls-04 (previous step) (back to tree)

A spec-lemma

Proof step 20 from proof mod-nls-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 21:

  ⊦ j ≠ 0 → abs(i % j) = abs(i) % abs(j)

• Proof step 22:

  j ≠ 0, i % j < i0, i0 + abs(j) ≤ 1, ¬ abs(i) % abs(j) < abs(j) ⊦

Rule argument

Additional information

Used terms: j, i

Proof step 21 from proof mod-nls-04 (previous step) (back to tree)

Lemma abs-shift

Proof step 22 from proof mod-nls-04 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 23:

  j ≠ 0, i % j < i0, i0 + abs(j) ≤ 1, abs(j) ≤ abs(i) % abs(j) ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 23 from proof mod-nls-04 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  ⊦ 0 < j → ¬ j ≤ i % j

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < abs(i) ↔ i ≠ 0; (s) Used terms: abs(i), abs(j)

Proof step 24 from proof mod-nls-04 (previous step) (back to tree)

Lemma mod-les