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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

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

User applied rule structural induction

And obtained the following new goals

• Proof step 3:

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

• Proof step 8:

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

Rule argument

Additional information

Used simplifier rules: int generated by 0, +1, -1;; ⊦ 0 + i = 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)

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

User applied rule all left

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used terms: j, i, i0

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

User applied rule case distinction

And obtained the following new goals

• Proof step 5:

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

• Proof step 6:

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

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: zero-gr: ⊦ 0 < i → (0 < i * j ↔ 0 < j); ls-pos: ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); associativity: ⊦ i * j * j0 = (i * j) * j0; commutativity: ⊦ i * j = j * i; ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) ⊦ i +1 = i + 1; (s) forward-le-01: ⊦ i ≤ j ∧ 0 ≤ i → 0 ≤ j; (forward) from specification int-abs forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs forward-le-05: ⊦ i < j ∧ 0 ≤ i → 0 < j; (forward) from specification int-abs ⊦ (* j) < i0 + (* j0) ↔ j - j0 < i0; (s) ⊦ ~1 < i ↔ 0 ≤ i; (s) ⊦ i < j + 1 ↔ i ≤ j; (s) ⊦ i ≤ i + j ↔ 0 ≤ j; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 add-c: ⊦ i + j = j + i; from specification int-basic2 i0 ≠ 0, i0 ≤ i ⊦ (* i) ≤ j → (* i0) ≤ j; (s) ⊦ i < j ↔ ¬ j ≤ i; (ss) ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) Used terms: i0 + i2

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

User applied rule exists left

And obtained the following new goals

• Proof step 7:

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

Rule argument

Additional information

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

User applied rule exists right

And closed the goal!

Rule argument

Additional information

Used simplifier rules: ⊦ (* j) ≤ i0 + (* j0) ↔ j - j0 ≤ i0; (s) add-c: ⊦ i + j = j + i; from specification int-basic2 ⊦ i +1 = i + 1; (s) add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ i ≤ 0 ∧ 0 ≤ j → i ≤ j; (s) Used terms: i1

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

User applied rule all left

And closed the goal!

Rule argument

Additional information

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