Proof step 1 from proof not-mtwo (conclusion) (back to tree)

System applied rule normalize

And obtained the following new goals

• Proof step 2:

  r + r0 = ~ 1.r + ~ 1.r, 0.r ≤ r0, 0.r ≤ r ⊦

Rule argument

Additional information

Proof step 2 from proof not-mtwo (previous step) (back to tree)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 3:

  2.r + r + r0 = 0.r, ¬ r < 0.r, ¬ r0 < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: le-def: ⊦ r ≤ r0 ↔ ¬ r0 < r; add-comm: ⊦ r + r0 = r0 + r; from specification real-basic add-assoc: ⊦ (r + r0) + r1 = r + r0 + r1; from specification real-basic add-c: ⊦ i + j = j + i; from specification int-basic2 add-a: ⊦ i + j + i0 = (i + j) + i0; from specification int-basic2 ⊦ (* i).r + (* j).r = (i + j).r; (s) ⊦ r + 1.r = ~ 1.r ↔ r + 1.r + 1.r = 0.r; (s) ⊦ ~ r + r0 = r1 ↔ r0 = r1 + r; (as)

Proof step 3 from proof not-mtwo (previous step) (back to tree)

User applied rule cut formula

And obtained the following new goals

• Proof step 4:

  2.r + r + r0 = 0.r, 2.r ≤ 2.r + r + r0, ¬ r < 0.r, ¬ r0 < 0.r ⊦

Rule argument

Additional information

Used simplifier rules: le-def: ⊦ r ≤ r0 ↔ ¬ r0 < r; lf-02: ⊦ r < r0 ∧ r0 = r1 → r < r1; (forward) from specification real-basic lf-07: ⊦ ¬ r < r1 ∧ r0 < r1 → r0 < r; (forward) from specification real-basic ⊦ r + r0 < r + r1 ↔ r0 < r1; (s) ⊦ r < r + r0 ↔ 0.r < r0; (s) ⊦ i.r < j.r ↔ i < j; (s) ⊦ r + r0 < r0 ↔ r < 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 Used formulas: 2.r ≤ 2.r + r + r0

Proof step 4 from proof not-mtwo (previous step) (back to tree)

User applied rule subst equation

And closed the goal!

Rule argument

Additional information

Used simplifier rules: le-def: ⊦ r ≤ r0 ↔ ¬ r0 < r; ⊦ i.r < j.r ↔ i < j; (s)