---

Step * of Lemma isrcv-implies

∀[k:Knd]. k = rcv(lnk(k),tag(k)) ∈ Knd supposing ↑isrcv(k)
BY
{ (((Auto THEN (MoveToConcl (-1)) THEN Unfolds ``isrcv rcv lnk tagof`` 0 THEN (D (-1)) THEN Reduce 0 THEN D 0)
    THENA Auto
    )
   THEN Try (Trivial)
   THEN (D (-2))
   THEN Reduce 0
   THEN Fold `rcv` 0
   THEN Auto) }

---

Latex:


\mforall{}[k:Knd].  k  =  rcv(lnk(k),tag(k))  supposing  \muparrow{}isrcv(k)


By

(((Auto
      THEN  (MoveToConcl  (-1))
      THEN  Unfolds  ``isrcv  rcv  lnk  tagof``  0
      THEN  (D  (-1))
      THEN  Reduce  0
      THEN  D  0)
    THENA  Auto
    )
  THEN  Try  (Trivial)
  THEN  (D  (-2))
  THEN  Reduce  0
  THEN  Fold  `rcv`  0
  THEN  Auto)

---

Home Index