---

Step * of Lemma ifthenelse_functionality_wrt_implies3

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

---

Latex:

---

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


By

---

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

---

Home Index