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