Step
*
of Lemma
map-ifthenelse
∀[f,x,y,b:Top].  (map(f;if b then x else y fi ) ~ if b then map(f;x) else map(f;y) fi )
BY
{ (Auto THEN UnrollLoopsOnce) }
Latex:
Latex:
\mforall{}[f,x,y,b:Top].    (map(f;if  b  then  x  else  y  fi  )  \msim{}  if  b  then  map(f;x)  else  map(f;y)  fi  )
By
Latex:
(Auto  THEN  UnrollLoopsOnce)
Home
Index