---

Step * of Lemma ifthenelse_functionality_wrt_uimplies

∀b1,b2:𝔹.
  ∀[p1,q1,p2,q2:ℙ].
    (b1 = b2
    ⇒ {q2 supposing q1}
    ⇒ {p2 supposing p1}
    ⇒ {if b2 then p2 else q2 fi  supposing if b1 then p1 else q1 fi })
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN (AutoSplit THEN ElimVar `b1' THEN Auto THEN All Reduce THEN BackThruSomeHyp THEN Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}b1,b2:\mBbbB{}.
    \mforall{}[p1,q1,p2,q2:\mBbbP{}].
        (b1  =  b2
        {}\mRightarrow{}  \{q2  supposing  q1\}
        {}\mRightarrow{}  \{p2  supposing  p1\}
        {}\mRightarrow{}  \{if  b2  then  p2  else  q2  fi    supposing  if  b1  then  p1  else  q1  fi  \})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  (AutoSplit  THEN  ElimVar  `b1'  THEN  Auto  THEN  All  Reduce  THEN  BackThruSomeHyp  THEN  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  AutoSplit)

---

Home Index