---

Step * of Lemma assert_dec2bool

∀[d:Decision]. uiff(↑dec2bool(d);↑d)
BY
{ (BasicUniformUnivCD Auto
   THEN RepUR ``assert dec2bool ifthenelse btrue bfalse`` 0
   THEN RepeatFor 2 (D 0)
   THEN Try (DVar `d')
   THEN All Reduce
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[d:Decision].  uiff(\muparrow{}dec2bool(d);\muparrow{}d)


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  RepUR  ``assert  dec2bool  ifthenelse  btrue  bfalse``  0
  THEN  RepeatFor  2  (D  0)
  THEN  Try  (DVar  `d')
  THEN  All  Reduce
  THEN  Auto)

---

Home Index