---

Step * of Lemma local_or_rcv

∀k:Knd. ((↑islocal(k)) ∨ (↑isrcv(k)))
BY
{ (Unfolds ``islocal isrcv Knd`` 0 THEN Auto THEN (D (-1)) THEN Reduce 0 THEN Obvious) }

---

Latex:


\mforall{}k:Knd.  ((\muparrow{}islocal(k))  \mvee{}  (\muparrow{}isrcv(k)))


By

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

---

Home Index