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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  j0 < i0, j < i, 0 < j, 0 < i0, 0 < i, ¬ j0 < (i * i0) / j ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  j < i, j0 < i0, 0 < i, 0 < i0, 0 < j, 1 < i, (i * i0) / j < i0, (i * i0) / j ≤ j0 ⊦

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 forward-lels: ⊦ i ≤ j ∧ j < j0 → i < j0; (forward) from specification int-abs ⊦ i < j ↔ ¬ j ≤ i; (ss)

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

User applied rule apply elim lemma

And obtained the following new goals

• Proof step 4:

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

• Proof step 5:

  i * i0 = i1 * j + j1, i1 < i0, 1 < i, 0 < j, 0 < i0, 0 < i, j0 < i0, j < i, j1 < j, 0 < i * i0, i1 ≤ j0, 0 ≤ j1 ⊦

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: i * i0, j, i1, j1

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

Lemma div-elim

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 6:

  i * i0 = i1 * j + j1, j1 < j, j < i, j0 < i0, 0 < i, 0 < j, 1 < i, 0 < i0, i1 < i0, i1 ≤ j0, 0 ≤ j1 ⊦

Rule argument

Additional information

Used simplifier rules: 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 commutativity: ⊦ i * j = j * i; from specification int-mult associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult ⊦ 0 < i → (0 < i * j ↔ 0 < j); (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 7:

  i * i0 = i1 * j + j1, i1 < i0, 0 < i0, 1 < i, 0 < j, 0 < i, j0 < i0, j < i, j1 < j, 0 ≤ j1, i1 ≤ j0, ¬ i1 * j + j1 < i * i0 ⊦

Rule argument

Additional information

Used simplifier rules: ls-forward: ⊦ i * j < i * j0 → i ≠ 0; (forward) from specification int-mult ⊦ 0 < i → (i * j < i * j0 ↔ j < j0); (s) ⊦ ¬ i < i; (s) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: i1 * j + j1 < i * i0

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

User applied rule weakening

And obtained the following new goals

• Proof step 8:

  j1 < j, j < i, j0 < i0, 0 < i, 0 < j, 1 < i, 0 < i0, i1 < i0, i1 ≤ j0, 0 ≤ j1, ¬ i1 * j + j1 < i * i0 ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  i1 < i0, 0 < i0, 1 < i, 0 < j, 0 < i, j0 < i0, j < i, j1 < j, 0 ≤ j1, i1 ≤ j0, i * i0 ≤ i1 * j + j1 ⊦

Rule argument

Additional information

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

Proof step 9 from proof estimate-01 (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 10:

  j1 < j, j < i, j0 < i0, 0 < i, 0 < j, 1 < i, 0 < i0, i1 < i0, j * i0 < i1 * j + j1, i * i0 ≤ i1 * j + j1, i1 ≤ j0, 0 ≤ j1 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ i < j ↔ ¬ j ≤ i; (ss) forward-lele: ⊦ j ≤ j0 ∧ j0 ≤ j1 → j ≤ j1; (forward) from specification int-abs ⊦ 0 < i → (i * j ≤ i * i0 ↔ j ≤ i0); (s) ⊦ i < j → (j ≤ i ↔ false); (as) associativity: ⊦ i * j * j0 = (i * j) * j0; from specification int-mult commutativity: ⊦ i * j = j * i; from specification int-mult Used formulas: j * i0 < i1 * j + j1

Proof step 10 from proof estimate-01 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 11:

  j * i < j * i0 + j0, 0 ≤ j0, j0 < j ⊦ i ≤ i0

Rule argument

Additional information

Used simplifier rules: ⊦ i < j → (j ≤ i ↔ false); (as) commutativity: ⊦ i * j = j * i; from specification int-mult Used terms: j, i0, i1, j1

Proof step 11 from proof estimate-01 (previous step) (back to tree)

A spec-lemma