---

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