---

Step * of Lemma quadratic-1-2-equal

∀[a,b,c:ℝ].
  ({(quadratic1(a;b;c) = quadratic2(a;b;c)) ∧ (quadratic1(a;b;c) = (-(b)/r(2) * a))}) supposing 
     (((b * b) = (r(4) * a * c)) and 
     a ≠ r0)
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN (Assert r(2) * a ≠ r0 BY
               (RepeatFor 2 (ParallelOp 4) THEN Auto THEN nRMul ⌜r(2)⌝ 4⋅ THEN Auto))
   THEN Try (Trivial)
   THEN (Assert ((b * b) - r(4) * a * c) = r0 BY
               Auto)
   THEN (Assert rsqrt((b * b) - r(4) * a * c) = r0 BY
               (RWO  "-1" 0 THEN Auto))
   THEN RepUR ``quadratic1 quadratic2`` 0
   THEN (BLemma `rdiv_functionality` THEN Auto)
   THEN RWO "-1" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,c:\mBbbR{}].
    (\{(quadratic1(a;b;c)  =  quadratic2(a;b;c))  \mwedge{}  (quadratic1(a;b;c)  =  (-(b)/r(2)  *  a))\})  supposing 
          (((b  *  b)  =  (r(4)  *  a  *  c))  and 
          a  \mneq{}  r0)


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  (Assert  r(2)  *  a  \mneq{}  r0  BY
                          (RepeatFor  2  (ParallelOp  4)  THEN  Auto  THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  4\mcdot{}  THEN  Auto))
  THEN  Try  (Trivial)
  THEN  (Assert  ((b  *  b)  -  r(4)  *  a  *  c)  =  r0  BY
                          Auto)
  THEN  (Assert  rsqrt((b  *  b)  -  r(4)  *  a  *  c)  =  r0  BY
                          (RWO    "-1"  0  THEN  Auto))
  THEN  RepUR  ``quadratic1  quadratic2``  0
  THEN  (BLemma  `rdiv\_functionality`  THEN  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto)

---

Home Index