Proof step 1 from proof auxexdivmod-01 (conclusion) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 2:

  i0 * j ≤ i, i < (i0 + i1) * j, 0 ≤ i0, 0 < j, 0 ≤ i, 0 ≤ i1 ⊦ ∃ i0. i0 * j ≤ i ∧ i < (i0 + 1) * j ∧ 0 ≤ i0

• Proof step 3:

  0 < j, 0 ≤ i ⊦ ∃ i0. i0 * j ≤ i ∧ i < (i0 + 1) * j ∧ 0 ≤ i0, 0 * j ≤ i ∧ i < (0 + i) * j ∧ 0 ≤ 0

Rule argument

Additional information

Used terms: 0, j, i, i

Proof step 2 from proof auxexdivmod-01 (previous step) (back to tree)

Lemma auxexdivmod

Proof step 3 from proof auxexdivmod-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 4:

  0 < j, i * j ≤ i, 0 ≤ i ⊦ ∃ i0. i0 * j ≤ i ∧ i < i0 * j + j ∧ 0 ≤ i0

Rule argument

Additional information

Used simplifier rules: Mult-zero: ⊦ i * 0 = 0; dist-lsplit: ⊦ (i + i0) * j = i * j + i0 * j; one: ⊦ 1 * i = i; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; 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 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; (ss) ⊦ i + 0 = i; (s)

Proof step 4 from proof auxexdivmod-01 (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 5:

  ⊦ 0 < i → (i * j ≤ i ↔ j ≤ 1)

• Proof step 6:

  0 < j, 0 ≤ i, i * j ≤ i, ¬ 0 < i ⊦ ∃ i0. i0 * j ≤ i ∧ i < i0 * j + j ∧ 0 ≤ i0

• Proof step 8:

  0 < j, 0 < i, 0 ≤ i, j ≤ 1 ⊦ ∃ i0. i0 * j ≤ i ∧ i < i0 * j + j ∧ 0 ≤ i0

Rule argument

Additional information

Used terms: j, i

Proof step 5 from proof auxexdivmod-01 (previous step) (back to tree)

Lemma le-same

Proof step 6 from proof auxexdivmod-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  0 < j ⊦ ∃ i0. i0 * j ≤ 0 ∧ 0 < i0 * j + j ∧ 0 ≤ i0

Rule argument

Additional information

Used simplifier rules: Mult-zero: ⊦ i * 0 = 0; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ i ≤ j → (j ≤ i ↔ i = j); (s) ⊦ i < j ↔ ¬ j ≤ i; (ss)

Proof step 7 from proof auxexdivmod-01 (previous step) (back to tree)

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: Mult-zero: ⊦ i * 0 = 0; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ 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 Used terms: 0

Proof step 8 from proof auxexdivmod-01 (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And closed the goal!

Rule argument

Additional information

Used simplifier rules: one-01: ⊦ i = 1 → i * j = j; associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ ¬ i < i; (s) ⊦ i ≤ j ↔ ¬ j < i; (ss) 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 ↔ i = j); (s) ⊦ i < j + 1 ↔ i ≤ j; (s) forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ 0 < i → (i ≤ 1 ↔ i = 1); (s)