---

Step * of Lemma islocal-not-isrcv

∀[k:Knd]. (islocal(k) ~ ¬bisrcv(k))
BY
{ (Auto THEN (D (-1)) THEN Unfolds ``islocal isrcv`` 0 THEN Reduce 0 THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  (islocal(k)  \msim{}  \mneg{}\msubb{}isrcv(k))


By

(Auto  THEN  (D  (-1))  THEN  Unfolds  ``islocal  isrcv``  0  THEN  Reduce  0  THEN  Auto)

---

Home Index