---

Step * of Lemma ifthenelse_sqle

∀[a,x1,y1,x2,y2:Base].
  if a then x1 else y1 fi  ≤ if a then x2 else y2 fi  
  supposing ((∃z:Base. (a ~ inl z)) ⇒ (x1 ≤ x2)) ∧ ((∃z:Base. (a ~ inr z )) ⇒ (y1 ≤ y2))
BY
{ (Unfold `ifthenelse` 0 THEN SqReasoning) }

---

Latex:

---

Latex:
\mforall{}[a,x1,y1,x2,y2:Base].
    if  a  then  x1  else  y1  fi    \mleq{}  if  a  then  x2  else  y2  fi   
    supposing  ((\mexists{}z:Base.  (a  \msim{}  inl  z))  {}\mRightarrow{}  (x1  \mleq{}  x2))  \mwedge{}  ((\mexists{}z:Base.  (a  \msim{}  inr  z  ))  {}\mRightarrow{}  (y1  \mleq{}  y2))


By

---

Latex:
(Unfold  `ifthenelse`  0  THEN  SqReasoning)

---

Home Index