---

Step * of Lemma not_locl_rcv

∀[a:Id]. ∀[l:IdLnk]. ∀[tg:Id].  False supposing locl(a) = rcv(l,tg) ∈ Knd
BY
{ (Auto THEN Assert ⌜rcv(l,tg) = locl(a) ∈ Knd⌝⋅ THEN Auto THEN (FLemma `not_rcv_locl` [(-1)]) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a:Id].  \mforall{}[l:IdLnk].  \mforall{}[tg:Id].    False  supposing  locl(a)  =  rcv(l,tg)


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}rcv(l,tg)  =  locl(a)\mkleeneclose{}\mcdot{}  THEN  Auto  THEN  (FLemma  `not\_rcv\_locl`  [(-1)])  THEN  Auto)

---

Home Index