Proof step 1 from proof eq-nonzero (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

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

Rule argument

Additional information

Proof step 2 from proof eq-nonzero (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

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

Rule argument

Additional information

Proof step 3 from proof eq-nonzero (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

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

Rule argument

Additional information

Used simplifier rules: distr: ⊦ r * (r0 + r1) = r * r0 + r * r1; minus-left: ⊦ ~ r * r0 = ~(r * r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ r = r0 → r + ~ r0 = 0.r; (s) add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-comm: ⊦ r + r0 = r0 + r; from specification real-basic ⊦ i.r = j.r ↔ i = j; (s) Used formulas: (r0 + ~ r2) * r = 0.r

Proof step 4 from proof eq-nonzero (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 5:

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

Rule argument

Additional information

Used simplifier rules: distr: ⊦ r * (r0 + r1) = r * r0 + r * r1; minus-left: ⊦ ~ r * r0 = ~(r * r0); mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r; ⊦ i.r = j.r ↔ i = j; (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)

Proof step 5 from proof eq-nonzero (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 6:

  r * r0 = r * r2, r ^-1 * r * r0 ≠ r ^-1 * r * r2, r ≠ 0.r, r0 ≠ r2 ⊦

Rule argument

Additional information

Used simplifier rules: inv-def: ⊦ r * r ^-1 = 1.r; mult-one: ⊦ 1.r * r = r; mult-com: ⊦ r * r0 = r0 * r; mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; Used formulas: r ^-1 * r * r0 = r ^-1 * r * r2

Proof step 6 from proof eq-nonzero (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: mult-ass: ⊦ (r * r0) * r1 = r * r0 * r1; mult-com: ⊦ r * r0 = r0 * r;