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

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  ¬(r * r0 = 0.r ↔ r0 = 0.r), 0.r < r ⊦

Rule argument

Additional information

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

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; lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic ⊦ i.r = j.r ↔ i = j; (s)

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

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

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

• Proof step 7:

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

Rule argument

Additional information

Used formulas: 0.r < r0

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic

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

User applied rule apply lemma

And obtained the following new goals

• Proof step 6:

  ⊦ r > 0.r ∧ r0 > 0.r → r * r0 > 0.r

Rule argument

Additional information

Used simplifier rules: ⊦ r > r0 ↔ r0 < r; (s) trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic lf-02: ⊦ r < r0 ∧ r0 = r1 → r < r1; (forward) from specification real-basic ⊦ r < r0 → ¬ r0 < r; (s) Used terms: r, r0

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

Lemma order

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 8:

  ⊦ r < r0 ↔ ¬ r0 ≤ r

• Proof step 9:

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

Rule argument

Additional information

Used terms: 0.r, r0

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

A spec-lemma

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

User applied rule apply rewrite lemma

And obtained the following new goals

• Proof step 10:

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

• Proof step 11:

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

Rule argument

Additional information

Used terms: r0, 0.r

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

A spec-lemma

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 12:

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

Rule argument

Additional information

Used simplifier rules: lf-02: ⊦ r < r0 ∧ r0 = r1 → r < r1; (forward) from specification real-basic trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ r < r0 → ¬ r0 < r; (s) ⊦ r ≠ r0 → (r ≤ r0 ↔ r < r0); (s)

Proof step 12 from proof zero-neq-01 (previous step) (back to tree)

User applied rule apply lemma

And obtained the following new goals

• Proof step 13:

  ⊦ r > 0.r ∧ r0 > 0.r → r * r0 > 0.r

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; ⊦ r > r0 ↔ r0 < r; (s) ⊦ 0.r < ~ r ↔ r < 0.r; (s) lf-03: ⊦ r < r0 ∧ r = r1 → r1 < r0; (forward) from specification real-basic lf-02: ⊦ r < r0 ∧ r0 = r1 → r < r1; (forward) from specification real-basic trans: ⊦ r < r0 ∧ r0 < r1 → r < r1; (forward) from specification real-basic ⊦ r < r0 → ¬ r0 < r; (s) Used terms: r, ~ r0

Proof step 13 from proof zero-neq-01 (previous step) (back to tree)

Lemma order