Step
*
of Lemma
isl-not-isr
∀x:Top + Top. ((↑isl(x)) 
⇒ (isr(x) ~ ff))
BY
{ ((Auto THEN D 1) THEN All Reduce THEN Auto) }
Latex:
Latex:
\mforall{}x:Top  +  Top.  ((\muparrow{}isl(x))  {}\mRightarrow{}  (isr(x)  \msim{}  ff))
By
Latex:
((Auto  THEN  D  1)  THEN  All  Reduce  THEN  Auto)
Home
Index