Proof step 1 from proof square-le (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(r * r ≤ r0 * r0 ↔ abs(r) ≤ abs(r0)) ⊦

Rule argument

Additional information

Proof step 2 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  ¬(r * r ≤ r0 * r0 ↔ (r < 0.r ⊃ ~ r;r) ≤ (r0 < 0.r ⊃ ~ r0;r0)) ⊦

Rule argument

Additional information

Used simplifier rules: abs-ite: ⊦ abs(r) = (r < 0.r ⊃ ~ r;r);

Proof step 3 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 4:

  r * r ≤ r0 * r0, ¬ (r < 0.r ⊃ ~ r;r) ≤ (r0 < 0.r ⊃ ~ r0;r0) ⊦

• Proof step 50:

  (r < 0.r ⊃ ~ r;r) ≤ (r0 < 0.r ⊃ ~ r0;r0), ¬ r * r ≤ r0 * r0 ⊦

Rule argument

Additional information

Proof step 4 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

  (r0 < 0.r ⊃ ~ r0;r0) < (r < 0.r ⊃ ~ r;r), r * r ≤ r0 * r0 ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 5 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 6:

  r * r ≤ r0 * r0, r0 < 0.r, ~ r0 < (r < 0.r ⊃ ~ r;r) ⊦

• Proof step 25:

  r * r ≤ r0 * r0, r0 < (r < 0.r ⊃ ~ r;r), ¬ r0 < 0.r ⊦

Rule argument

Additional information

Proof step 6 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 7:

  0.r < (r < 0.r ⊃ ~ r;r) + r0, 0.r < (r < 0.r ⊃ ~ r;r), r * r ≤ r0 * r0, r0 < 0.r, r0 < (r < 0.r ⊃ ~ r;r) ⊦

Rule argument

Additional information

Used simplifier rules: trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r < r + r0 ↔ 0.r < r0; (s) ⊦ ~ r < r0 ↔ 0.r < r0 + r; (s)

Proof step 7 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 8:

  0.r < (r < 0.r ⊃ ~ r;r), 0.r < ~ r + r0, r * r ≤ r0 * r0, r < 0.r, r0 < (r < 0.r ⊃ ~ r;r), r0 < 0.r ⊦

• Proof step 11:

  0.r < (r < 0.r ⊃ ~ r;r), 0.r < r + r0, r * r ≤ r0 * r0, r0 < (r < 0.r ⊃ ~ r;r), r0 < 0.r, ¬ r < 0.r ⊦

Rule argument

Additional information

Proof step 8 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 9:

  r * r ≤ r0 * r0, r < r0, r < 0.r, r0 < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ 0.r < ~ r ↔ r < 0.r; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ 0.r < r + ~ r0 ↔ r0 < r; (s) ⊦ r < 0.r ∧ r0 < 0.r → r + r0 < 0.r; (s) ⊦ r0 < ~ r ↔ r0 + r < 0.r; (s)

Proof step 9 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

  ⊦ ¬ r ≤ r1 ∧ r ≤ r0 → ¬ r0 ≤ r1

Rule argument

Additional information

Used simplifier rules: le-neg: ⊦ r < 0.r → (r * r0 ≤ r * r1 ↔ r1 ≤ r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r < r0 → (r0 ≤ r ↔ false); (as) ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) ⊦ r < r0 → ¬ r0 < r; (s) Used terms: r * r0, r * r, r0 * r0

Proof step 10 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 11 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

  0.r < r, 0.r < r + r0, r * r ≤ r0 * r0, r0 < r, r0 < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ 0.r < r → r0 < r0 + r; (s) trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ r < r0 → ¬ r0 < r; (s)

Proof step 12 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 13:

  ⊦ ¬ r ≤ r1 ∧ r ≤ r0 → ¬ r0 ≤ r1

• Proof step 14:

  0.r < r + r0, 0.r < r, r * r ≤ r0 * r0, r0 < 0.r, r0 < r ⊦ ¬ r * ~ r0 ≤ r0 * r0 ∧ r * ~ r0 ≤ r * r

Rule argument

Additional information

Used terms: r * ~ r0, r * r, r0 * r0

Proof step 13 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 14 from proof square-le (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 15:

  0.r < r, 0.r < r + r0, r * ~ r0 ≤ r0 * r0, r * r ≤ r0 * r0, r0 < r, r0 < 0.r ⊦

• Proof step 23:

  0.r < r, 0.r < r + r0, r * r ≤ r0 * r0, r0 < r, r0 < 0.r, ¬ r * ~ r0 ≤ r * r ⊦

Rule argument

Additional information

Proof step 15 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 16:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 17:

  0.r < r + r0, 0.r < r, r * r ≤ r0 * r0, r0 < 0.r, r0 < r, ~(r0 * r) ≤ r0 * r0 ⊦

Rule argument

Additional information

Used simplifier rules: mult-com: ⊦ r * r0 = r0 * r; Used terms: r0, r

Proof step 16 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 17 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 18:

  ⊦ r * r0 = r0 * r

• Proof step 19:

  0.r < r, 0.r < r + r0, r * r ≤ r0 * r0, r0 < r, r0 < 0.r, ~(r * r0) ≤ r0 * r0 ⊦

Rule argument

Additional information

Used terms: r0, r

Proof step 18 from proof square-le (previous step) (back to tree)

Lemma mult-com

Proof step 19 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 20:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 21:

  0.r < r + r0, 0.r < r, r * r ≤ r0 * r0, r0 < 0.r, r0 < r, ~ r * r0 ≤ r0 * r0 ⊦

Rule argument

Additional information

Used terms: r, r0

Proof step 20 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 21 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 22:

  ⊦ r < 0.r → (r0 * r ≤ r1 * r ↔ r1 ≤ r0)

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: ~ r, r0, r0

Proof step 22 from proof square-le (previous step) (back to tree)

Lemma le-neg-01

Proof step 23 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 24:

  0.r < r, 0.r < r0, r ≤ r1, r0 ≤ r2 ⊦ r * r0 ≤ r1 * r2

Rule argument

Additional information

Used simplifier rules: minus-left: ⊦ ~ r * r0 = ~(r * r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ 0.r < ~ r ↔ r < 0.r; (s) ⊦ r ≤ r; (s) ⊦ ~ r ≤ r0 ↔ 0.r ≤ r + r0; (s) ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → ¬ r0 < r; (s) Used terms: r, ~ r0, r, r

Proof step 24 from proof square-le (previous step) (back to tree)

Lemma ple-pos

Proof step 25 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 26:

  0.r ≤ r0, 0.r < (r < 0.r ⊃ ~ r;r), r * r ≤ r0 * r0, r0 < (r < 0.r ⊃ ~ r;r) ⊦

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ r ≤ r0 ∧ r0 < r1 → r < r1; (forward) from specification real-abs ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss)

Proof step 26 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 27:

  0.r < (r < 0.r ⊃ ~ r;r), 0.r ≤ r0, r * r ≤ r0 * r0, r < 0.r, r0 < ~ r ⊦

• Proof step 44:

  0.r < (r < 0.r ⊃ ~ r;r), 0.r ≤ r0, r * r ≤ r0 * r0, r0 < r, ¬ r < 0.r ⊦

Rule argument

Additional information

Proof step 27 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 28:

  0.r ≤ r0, r * r ≤ r0 * r0, r < 0.r, r0 + r < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + r0 < r0 ↔ r < 0.r; (s) ⊦ r < 0.r ∧ 0.r ≤ r0 → r < r0; (s) forward-lsle: ⊦ r < r0 ∧ r0 ≤ r1 → r < r1; (forward) from specification real-abs ⊦ 0.r < ~ r ↔ r < 0.r; (s) ⊦ r0 < ~ r ↔ r0 + r < 0.r; (s)

Proof step 28 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 29:

  ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0)

• Proof step 30:

  0.r ≤ r0, r < 0.r, r * r ≤ r0 * r0, r0 + r < 0.r, ¬ r0 ≤ 0.r ⊦

Rule argument

Additional information

Used simplifier rules: mult-zero: ⊦ 0.r * r = 0.r; zero-le-01: ⊦ r < 0.r → (r * r0 ≤ 0.r ↔ 0.r ≤ r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r ≤ r; (s) ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: 0.r, r0

Proof step 29 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 30 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 31:

  0.r ≠ r0, 0.r < r0, r * r ≤ r0 * r0, r < 0.r, r0 + r < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s)

Proof step 31 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 32:

  ⊦ ¬ r ≤ r1 ∧ r ≤ r0 → ¬ r0 ≤ r1

• Proof step 33:

  0.r ≠ r0, 0.r < r0, r < 0.r, r * r ≤ r0 * r0, r0 + r < 0.r ⊦ ¬ r0 * ~ r ≤ r0 * r0 ∧ r0 * ~ r ≤ r * r

Rule argument

Additional information

Used terms: r0 * ~ r, r * r, r0 * r0

Proof step 32 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 33 from proof square-le (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 34:

  0.r ≠ r0, 0.r < r0, r * r ≤ r0 * r0, r < 0.r, r0 * ~ r ≤ r0 * r0, r0 + r < 0.r ⊦

• Proof step 36:

  0.r ≠ r0, 0.r < r0, r * r ≤ r0 * r0, r < 0.r, r0 + r < 0.r, ¬ r0 * ~ r ≤ r * r ⊦

Rule argument

Additional information

Proof step 34 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 35:

  ⊦ 0.r < r → (r * r0 ≤ r * r1 ↔ r0 ≤ r1)

Rule argument

Additional information

Used simplifier rules: ⊦ ~ r ≤ r0 ↔ 0.r ≤ r + r0; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: r0, ~ r, r0

Proof step 35 from proof square-le (previous step) (back to tree)

Lemma le-pos

Proof step 36 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 37:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 38:

  0.r ≠ r0, 0.r < r0, r < 0.r, r * r ≤ r0 * r0, r0 + r < 0.r, ¬ ~(r * r0) ≤ r * r ⊦

Rule argument

Additional information

Used simplifier rules: mult-com: ⊦ r * r0 = r0 * r; Used terms: r, r0

Proof step 37 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 38 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 39:

  ⊦ r * r0 = r0 * r

• Proof step 40:

  0.r ≠ r0, 0.r < r0, r * r ≤ r0 * r0, r < 0.r, r0 + r < 0.r, ¬ ~(r0 * r) ≤ r * r ⊦

Rule argument

Additional information

Used terms: r, r0

Proof step 39 from proof square-le (previous step) (back to tree)

Lemma mult-com

Proof step 40 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 41:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 42:

  0.r ≠ r0, 0.r < r0, r < 0.r, r * r ≤ r0 * r0, r0 + r < 0.r, ¬ ~ r0 * r ≤ r * r ⊦

Rule argument

Additional information

Used terms: r0, r

Proof step 41 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 42 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 43:

  ⊦ r < 0.r → (r0 * r ≤ r1 * r ↔ r1 ≤ r0)

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s) ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → ¬ r0 < r; (s) Used terms: ~ r0, r, r

Proof step 43 from proof square-le (previous step) (back to tree)

Lemma le-neg-01

Proof step 44 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 45:

  0.r ≤ r0, 0.r < r, r * r ≤ r0 * r0, r0 < r ⊦

Rule argument

Additional information

Used simplifier rules: forward-le-05: ⊦ r < r0 ∧ 0.r ≤ r → 0.r < r0; (forward) from specification real-abs ⊦ r < r0 → ¬ r0 < r; (s)

Proof step 45 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 46:

  ⊦ ¬ r ≤ r1 ∧ r ≤ r0 → ¬ r0 ≤ r1

• Proof step 47:

  0.r < r, 0.r ≤ r0, r * r ≤ r0 * r0, r0 < r ⊦ ¬ r * r0 ≤ r0 * r0 ∧ r * r0 ≤ r * r

Rule argument

Additional information

Used terms: r * r0, r * r, r0 * r0

Proof step 46 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 47 from proof square-le (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 48:

  0.r ≤ r0, 0.r < r, r * r0 ≤ r0 * r0, r * r ≤ r0 * r0, r0 < r ⊦

Rule argument

Additional information

Used simplifier rules: le-pos: ⊦ 0.r < r → (r * r0 ≤ r * r1 ↔ r0 ≤ r1); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) ⊦ r < r0 → ¬ r0 < r; (s)

Proof step 48 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 49:

  ⊦ 0.r < r → (r0 * r ≤ r1 * r ↔ r0 ≤ r1)

Rule argument

Additional information

Used simplifier rules: mult-zero: ⊦ 0.r * r = 0.r; zero-le: ⊦ 0.r < r → (r * r0 ≤ 0.r ↔ r0 ≤ 0.r); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r < r0 → (r0 ≤ r ↔ false); (as) ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s) lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic ⊦ r ≤ r; (s) Used terms: r, r0, r0

Proof step 49 from proof square-le (previous step) (back to tree)

Lemma le-pos-01

Proof step 50 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 51:

  (r < 0.r ⊃ ~ r;r) ≤ (r0 < 0.r ⊃ ~ r0;r0), r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss)

Proof step 51 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 52:

  r < 0.r, r0 * r0 < r * r, ~ r ≤ (r0 < 0.r ⊃ ~ r0;r0) ⊦

• Proof step 82:

  r ≤ (r0 < 0.r ⊃ ~ r0;r0), r0 * r0 < r * r, ¬ r < 0.r ⊦

Rule argument

Additional information

Proof step 52 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 53:

  0.r ≤ r + (r0 < 0.r ⊃ ~ r0;r0), r < 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r < 0.r ∧ 0.r ≤ r0 → r < r0; (s) forward-lsle: ⊦ r < r0 ∧ r0 ≤ r1 → r < r1; (forward) from specification real-abs ⊦ ~ r ≤ r0 ↔ 0.r ≤ r + r0; (s)

Proof step 53 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 54:

  0.r ≤ r + ~ r0, r < 0.r, r0 * r0 < r * r, r0 < 0.r ⊦

• Proof step 57:

  0.r ≤ r + r0, r < 0.r, r0 * r0 < r * r, ¬ r0 < 0.r ⊦

Rule argument

Additional information

Proof step 54 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 55:

  r < 0.r, r0 * r0 < r * r, r0 ≤ r, r0 < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: forward-lels: ⊦ r ≤ r0 ∧ r0 < r1 → r < r1; (forward) from specification real-abs add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + 0.r = r; (s) ⊦ r ≤ r0 + ~ r1 ↔ r + r1 ≤ r0; (s)

Proof step 55 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 56:

  ¬ r < r1, r < r0 ⊦ ¬ r0 < r1

Rule argument

Additional information

Used simplifier rules: ls-neg: ⊦ r < 0.r → (r * r0 < r * r2 ↔ r2 < r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s) lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic ⊦ r ≤ r0 → ¬ r0 < r; (s) Used terms: r * r0, r0 * r0, r * r

Proof step 56 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 57 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 58:

  0.r ≤ r0, 0.r ≤ r + r0, r < 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r < 0.r ∧ 0.r ≤ r0 → r < r0; (s) forward-lsle: ⊦ r < r0 ∧ r0 ≤ r1 → r < r1; (forward) from specification real-abs ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss)

Proof step 58 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 59:

  ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0)

• Proof step 60:

  0.r ≤ r + r0, 0.r ≤ r0, r < 0.r, r0 * r0 < r * r, ¬ r0 ≤ 0.r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r; (s) ⊦ r + 0.r = r; (s) add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: 0.r, r0

Proof step 59 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 60 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 61:

  0.r ≠ r0, 0.r ≤ r + r0, 0.r < r0, r < 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s)

Proof step 61 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 62:

  ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0)

• Proof step 63:

  0.r ≠ r0, 0.r < r0, 0.r ≤ r + r0, r < 0.r, r0 * r0 < r * r, ¬ r + r0 ≤ 0.r ⊦

• Proof step 79:

  r + r0 = 0.r, 0.r ≠ r0, 0.r < r0, r < 0.r, r + r0 ≤ 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used terms: 0.r, r + r0

Proof step 62 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 63 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 64:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r0, 0.r < r + r0, r < 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s)

Proof step 64 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 65:

  ¬ r < r1, r < r0 ⊦ ¬ r0 < r1

• Proof step 66:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r + r0, 0.r < r0, r < 0.r, r0 * r0 < r * r ⊦ ¬ r0 * ~ r < r * r ∧ r0 * ~ r < r0 * r0

Rule argument

Additional information

Used terms: r0 * ~ r, r0 * r0, r * r

Proof step 65 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 66 from proof square-le (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 67:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r0, 0.r < r + r0, r < 0.r, r0 * ~ r < r * r, r0 * r0 < r * r ⊦

• Proof step 77:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r0, 0.r < r + r0, r < 0.r, r0 * r0 < r * r, ¬ r0 * ~ r < r0 * r0 ⊦

Rule argument

Additional information

Proof step 67 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 68:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 69:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r + r0, 0.r < r0, r < 0.r, r0 * r0 < r * r, ~(r * r0) < r * r ⊦

Rule argument

Additional information

Used simplifier rules: mult-com: ⊦ r * r0 = r0 * r; Used terms: r, r0

Proof step 68 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 69 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 70:

  ⊦ r * r0 = r0 * r

• Proof step 71:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r0, 0.r < r + r0, r < 0.r, r0 * r0 < r * r, ~(r0 * r) < r * r ⊦

Rule argument

Additional information

Used terms: r, r0

Proof step 70 from proof square-le (previous step) (back to tree)

Lemma mult-com

Proof step 71 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 72:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 73:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r + r0, 0.r < r0, r < 0.r, r0 * r0 < r * r, ~ r0 * r < r * r ⊦

Rule argument

Additional information

Used terms: r0, r

Proof step 72 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 73 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 74:

  ⊦ r * r0 = r0 * r

• Proof step 75:

  0.r ≠ r0, 0.r ≠ r + r0, 0.r < r0, 0.r < r + r0, r * ~ r0 < r * r, r < 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used terms: ~ r0, r

Proof step 74 from proof square-le (previous step) (back to tree)

Lemma mult-com

Proof step 75 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 76:

  ⊦ r < 0.r → (r * r0 < r * r2 ↔ r2 < r0)

Rule argument

Additional information

Used simplifier rules: ⊦ r0 < ~ r ↔ r0 + r < 0.r; (s) ⊦ r < r0 → ¬ r0 < r; (s) Used terms: r, ~ r0, r

Proof step 76 from proof square-le (previous step) (back to tree)

Lemma ls-neg

Proof step 77 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 78:

  ⊦ 0.r < r → (r * r0 < r * r2 ↔ r0 < r2)

Rule argument

Additional information

Used simplifier rules: ⊦ ~ r < r0 ↔ 0.r < r0 + r; (s) ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r < r0 → (r0 ≤ r ↔ false); (as) Used terms: r0, ~ r, r0

Proof step 78 from proof square-le (previous step) (back to tree)

Lemma ls-pos

Proof step 79 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 80:

  r + r0 = 0.r, 0.r ≠ r0, 0.r < r0, r < 0.r, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ r; (s) ⊦ r < 0.r ∧ 0.r ≤ r0 → r < r0; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + r0 < r0 ↔ r < 0.r; (s) forward-lsle: ⊦ r < r0 ∧ r0 ≤ r1 → r < r1; (forward) from specification real-abs forward-le-05: ⊦ r < r0 ∧ 0.r ≤ r → 0.r < r0; (forward) from specification real-abs lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic

Proof step 80 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 81:

  ⊦ ~ r = r0 ↔ r + r0 = 0.r

Rule argument

Additional information

Used simplifier rules: minus-left: ⊦ ~ r * r0 = ~(r * r0); ls-neg: ⊦ r < 0.r → (r * r0 < r * r2 ↔ r2 < r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ ~ r = 0.r ↔ r = 0.r; (s) ⊦ ~ ~ r = r; (s) ⊦ ¬ r < r; (s) Used terms: r, r0

Proof step 81 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 82 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 83:

  0.r ≤ r, 0.r ≤ (r0 < 0.r ⊃ ~ r0;r0), r ≤ (r0 < 0.r ⊃ ~ r0;r0), r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: forward-lele: ⊦ r ≤ r0 ∧ r0 ≤ r1 → r ≤ r1; (forward) from specification real-abs ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss)

Proof step 83 from proof square-le (previous step) (back to tree)

Heuristic if-then-else split applied rule case distinction

And obtained the following new goals

• Proof step 84:

  0.r ≤ (r0 < 0.r ⊃ ~ r0;r0), 0.r ≤ r, r ≤ ~ r0, r0 * r0 < r * r, r0 < 0.r ⊦

• Proof step 105:

  0.r ≤ (r0 < 0.r ⊃ ~ r0;r0), 0.r ≤ r, r ≤ r0, r0 * r0 < r * r, ¬ r0 < 0.r ⊦

Rule argument

Additional information

Proof step 84 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 85:

  0.r ≤ r, r + r0 ≤ 0.r, r0 * r0 < r * r, r0 < 0.r, r0 ≤ 0.r ⊦

Rule argument

Additional information

Used simplifier rules: ⊦ r < 0.r ∧ 0.r ≤ r0 → r < r0; (s) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + r0 ≤ r ↔ r0 ≤ 0.r; (s) ⊦ r < 0.r ∧ 0.r ≤ r0 → r ≤ r0; (s) forward-lsle: ⊦ r < r0 ∧ r0 ≤ r1 → r < r1; (forward) from specification real-abs forward-lele: ⊦ r ≤ r0 ∧ r0 ≤ r1 → r ≤ r1; (forward) from specification real-abs ⊦ r + 0.r = r; (s) ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s)

Proof step 85 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 86:

  ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0)

• Proof step 87:

  0.r ≤ r, r + r0 ≤ 0.r, r0 ≤ 0.r, r0 < 0.r, r0 * r0 < r * r, ¬ r ≤ 0.r ⊦

Rule argument

Additional information

Used simplifier rules: mult-zero: ⊦ 0.r * r = 0.r; zero-ls-01: ⊦ r < 0.r → (r * r0 < 0.r ↔ 0.r < r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r < r0 → ¬ r0 < r; (s) Used terms: 0.r, r

Proof step 86 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 87 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 88:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 ≤ 0.r, r0 * r0 < r * r, r0 < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic ⊦ r + r0 < r0 ↔ r < 0.r; (s) forward-lels: ⊦ r ≤ r0 ∧ r0 < r1 → r < r1; (forward) from specification real-abs ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s)

Proof step 88 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 89:

  ⊦ r < r0 ↔ ¬ r0 ≤ r

• Proof step 90:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 < 0.r, r0 ≤ 0.r, ¬ r * r ≤ r0 * r0 ⊦

Rule argument

Additional information

Used terms: r0 * r0, r * r

Proof step 89 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 90 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 91:

  ⊦ r ≤ r0 ∧ r0 ≤ r1 → r ≤ r1

• Proof step 92:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 ≤ 0.r, r0 < 0.r, ¬ r * r ≤ r0 * r0 ⊦ r * r ≤ r * ~ r0 ∧ r * ~ r0 ≤ r0 * r0

Rule argument

Additional information

Used terms: r * ~ r0, r * r, r0 * r0

Proof step 91 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 92 from proof square-le (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 93:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 < 0.r, r0 ≤ 0.r, ¬ r * r ≤ r * ~ r0, ¬ r * r ≤ r0 * r0 ⊦

• Proof step 95:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 < 0.r, r0 ≤ 0.r, ¬ r * ~ r0 ≤ r0 * r0, ¬ r * r ≤ r0 * r0 ⊦

Rule argument

Additional information

Proof step 93 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 94:

  ⊦ 0.r < r → (r * r0 ≤ r * r1 ↔ r0 ≤ r1)

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s) ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) ⊦ r ≤ r0 → ¬ r0 < r; (s) Used terms: r, r, ~ r0

Proof step 94 from proof square-le (previous step) (back to tree)

Lemma le-pos

Proof step 95 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 96:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 97:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 ≤ 0.r, r0 < 0.r, ¬ r * r ≤ r0 * r0, ¬ ~(r0 * r) ≤ r0 * r0 ⊦

Rule argument

Additional information

Used simplifier rules: mult-com: ⊦ r * r0 = r0 * r; Used terms: r0, r

Proof step 96 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 97 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 98:

  ⊦ r * r0 = r0 * r

• Proof step 99:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 < 0.r, r0 ≤ 0.r, ¬ r * r ≤ r0 * r0, ¬ ~(r * r0) ≤ r0 * r0 ⊦

Rule argument

Additional information

Used terms: r0, r

Proof step 98 from proof square-le (previous step) (back to tree)

Lemma mult-com

Proof step 99 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 100:

  ⊦ ~ r * r0 = ~(r * r0)

• Proof step 101:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 ≤ 0.r, r0 < 0.r, ¬ r * r ≤ r0 * r0, ¬ ~ r * r0 ≤ r0 * r0 ⊦

Rule argument

Additional information

Used terms: r, r0

Proof step 100 from proof square-le (previous step) (back to tree)

Lemma minus-left

Proof step 101 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 102:

  ⊦ r * r0 = r0 * r

• Proof step 103:

  0.r ≠ r, 0.r < r, r + r0 ≤ 0.r, r0 < 0.r, r0 ≤ 0.r, ¬ r * r ≤ r0 * r0, ¬ r0 * ~ r ≤ r0 * r0 ⊦

Rule argument

Additional information

Used terms: ~ r, r0

Proof step 102 from proof square-le (previous step) (back to tree)

Lemma mult-com

Proof step 103 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 104:

  ⊦ r < 0.r → (r * r0 ≤ r * r1 ↔ r1 ≤ r0)

Rule argument

Additional information

Used simplifier rules: ⊦ r ≤ ~ r0 ↔ r + r0 ≤ 0.r; (s) ⊦ r ≤ r0 ↔ ¬ r0 < r; (ss) add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ r ≤ r0 → ¬ r0 < r; (s) Used terms: r0, ~ r, r0

Proof step 104 from proof square-le (previous step) (back to tree)

Lemma le-neg

Proof step 105 from proof square-le (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 106:

  0.r ≤ r, 0.r ≤ r0, r ≤ r0, r0 * r0 < r * r ⊦

Rule argument

Additional information

Used simplifier rules: forward-lele: ⊦ r ≤ r0 ∧ r0 ≤ r1 → r ≤ r1; (forward) from specification real-abs ⊦ r ≤ r0 → ¬ r0 < r; (s)

Proof step 106 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 107:

  ¬ r < r1, r < r0 ⊦ ¬ r0 < r1

• Proof step 108:

  0.r ≤ r0, 0.r ≤ r, r ≤ r0, r0 * r0 < r * r ⊦ ¬ r * r0 < r * r ∧ r * r0 < r0 * r0

Rule argument

Additional information

Used terms: r * r0, r0 * r0, r * r

Proof step 107 from proof square-le (previous step) (back to tree)

A spec-lemma

Proof step 108 from proof square-le (previous step) (back to tree)

User applied rule case distinction

And obtained the following new goals

• Proof step 109:

  0.r ≤ r, 0.r ≤ r0, r ≤ r0, r0 * r0 < r * r, ¬ r * r0 < r0 * r0 ⊦

Rule argument

Additional information

Used simplifier rules: ls-forward: ⊦ r * r0 < r * r2 → r ≠ 0.r; ls-pos: ⊦ 0.r < r → (r * r0 < r * r2 ↔ r0 < r2); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s) ⊦ r ≤ r0 → ¬ r0 < r; (s)

Proof step 109 from proof square-le (previous step) (back to tree)

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 110:

  ⊦ 0.r < r0 → (r * r0 < r1 * r0 ↔ r < r1)

Rule argument

Additional information

Used simplifier rules: mult-zero: ⊦ 0.r * r = 0.r; mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ls-pos: ⊦ 0.r < r → (r * r0 < r * r2 ↔ r0 < r2); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r < r0 ↔ ¬ r0 ≤ r; (ss) ⊦ r ≤ r0 → (r0 ≤ r ↔ r = r0); (s) lf-02: ⊦ r < r0 ∧ r0 = r1 → r < r1; (forward) from specification real-basic ⊦ r ≤ r0 → ¬ r0 < r; (s) ⊦ r ≤ 0.r ∧ 0.r ≤ r0 → r ≤ r0; (s) Used terms: r, r0, r0

Proof step 110 from proof square-le (previous step) (back to tree)

Lemma ls-pos-01