---

Step * of Lemma req-iff-bdd-diff

∀[x,y:ℝ].  uiff(x = y;bdd-diff(x;y))
BY
{ (Unfold `req` 0
   THEN Auto
   THEN Try ((With ⌜4⌝ (D 0)⋅ THEN Complete (Auto)))
   THEN DVar `x'
   THEN DVar `y'
   THEN Unhide
   THEN Auto
   THEN ((InstLemma Obid: bdd-diff-regular) [⌜x⌝;⌜y⌝;⌜1⌝;⌜1⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[x,y:\mBbbR{}].    uiff(x  =  y;bdd-diff(x;y))


By

---

Latex:
(Unfold  `req`  0
  THEN  Auto
  THEN  Try  ((With  \mkleeneopen{}4\mkleeneclose{}  (D  0)\mcdot{}  THEN  Complete  (Auto)))
  THEN  DVar  `x'
  THEN  DVar  `y'
  THEN  Unhide
  THEN  Auto
  THEN  ((InstLemma  Obid:  bdd-diff-regular)  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}1\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Auto)

---

Home Index