Step
*
of Lemma
less-as-ifthenelse
∀[r,s,x,y:Top]. (if (r) < (s) then x else y ~ if r <z s then x else y fi )
BY
{ (Auto THEN RW (BasicSymbolicComputeC []) 0 THEN Auto) }
Latex:
Latex:
\mforall{}[r,s,x,y:Top]. (if (r) < (s) then x else y \msim{} if r <z s then x else y fi )
By
Latex:
(Auto THEN RW (BasicSymbolicComputeC []) 0 THEN Auto)
Home
Index