---

Step * of Lemma rsqrt1

rsqrt(r1) = r1
BY
{ ((BLemma `req_inversion` THENA Auto) THEN BLemma `rsqrt-unique` THEN Auto) }

---

Latex:

---

Latex:
rsqrt(r1)  =  r1


By

---

Latex:
((BLemma  `req\_inversion`  THENA  Auto)  THEN  BLemma  `rsqrt-unique`  THEN  Auto)

---

Home Index