---

Step * of Lemma reduce-ifthenelse

∀[f,k,x,y,b:Top].  (reduce(f;k;if b then x else y fi ) ~ if b then reduce(f;k;x) else reduce(f;k;y) fi )
BY
{ (Auto THEN UnrollLoopsOnce) }

---

Latex:

---

Latex:
\mforall{}[f,k,x,y,b:Top].
    (reduce(f;k;if  b  then  x  else  y  fi  )  \msim{}  if  b  then  reduce(f;k;x)  else  reduce(f;k;y)  fi  )


By

---

Latex:
(Auto  THEN  UnrollLoopsOnce)

---

Home Index