Proof step 1 from proof leone-two (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(i / 2 ≤ 1 ↔ i ≤ 1 + 1 + 1) ⊦

Rule argument

Additional information

Proof step 2 from proof leone-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(i / 2 ≤ 1 ↔ i ≤ 3) ⊦

Rule argument

Additional information

Used simplifier rules: add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2

Proof step 3 from proof leone-two (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  ¬(i / 2 ≤ 1 ↔ i ≤ 3), ¬ i < 0 ⊦

Rule argument

Additional information

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

Proof step 4 from proof leone-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  ¬(i / 2 ≤ 1 ↔ i ≤ 3), 0 ≤ i ⊦

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 5 from proof leone-two (previous step) (back to tree)

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 6:

  ⊦ 0 < j ∧ 0 ≤ i → (i0 = i / j ∧ j0 = i % j ↔ i = i0 * j + j0 ∧ 0 ≤ j0 ∧ j0 < j)

• Proof step 7:

  i = i0 * 2 + j0, ¬(i0 ≤ 1 ↔ i ≤ 3), j0 < 2, 0 < 2, 0 ≤ i, 0 ≤ j0 ⊦

Rule argument

Additional information

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

Proof step 6 from proof leone-two (previous step) (back to tree)

Lemma div-elim-pos

Proof step 7 from proof leone-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 8:

  ¬(i0 ≤ 1 ↔ i0 * 2 + j0 ≤ 3), j0 < 2, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs 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 8 from proof leone-two (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 9:

  j0 < 2, 0 ≤ i0, 0 ≤ j0, i0 ≤ 1, ¬ i0 * 2 + j0 ≤ 3 ⊦

• Proof step 12:

  j0 < 2, 0 ≤ i0, 0 ≤ j0, i0 * 2 + j0 ≤ 3, ¬ i0 ≤ 1 ⊦

Rule argument

Additional information

Proof step 9 from proof leone-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 10:

  j0 < 2, 3 < i0 * 2 + j0, 0 < i0 * 2 + j0, 1 < i0 * 2 + j0, i0 ≤ 1, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

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

Proof step 10 from proof leone-two (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

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

Rule argument

Additional information

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

Proof step 11 from proof leone-two (previous step) (back to tree)

A spec-lemma

Proof step 12 from proof leone-two (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 13:

  j0 < 2, 0 < i0, 1 < i0, i0 * 2 + j0 ≤ 3, 0 ≤ j0, 0 ≤ i0 ⊦

Rule argument

Additional information

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

Proof step 13 from proof leone-two (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 14:

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

Rule argument

Additional information

Used simplifier rules: ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s) ⊦ i = 1 → i * j = j; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult ⊦ i + (* j) ≤ (* j0) ↔ i ≤ j0 - j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 j0 ≠ 0, j < j0 ⊦ i ≤ (* j) → i < (* j0); (s) forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ 0 ≤ i → (i < 1 ↔ i = 0); (s) j0 ≠ 0, j ≤ j0 ⊦ i ≤ (* j) → i ≤ (* j0); (s) Used terms: i0, 1, j0, 1, 2

Proof step 14 from proof leone-two (previous step) (back to tree)

A spec-lemma