Step * of Lemma ifthenelse_functionality_wrt_uimplies3

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


Latex:


Latex:
\mforall{}b1,b2:\mBbbB{}.
    \mforall{}[p,q1,q2:\mBbbP{}].
        (b1  =  b2  {}\mRightarrow{}  \{q2  supposing  q1\}  {}\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  Try  ((ElimVar  `b1'  THEN  Auto  THEN  All  Reduce)))
  THEN  Try  ((RepeatFor  2  (MoveToConcl  (-1))  THEN  AutoSplit))
  THEN  (ElimVar  `b2'  THEN  Auto  THEN  All  Reduce  THEN  Auto)\mcdot{})




Home Index