---

Step * 1 of Lemma assert-isrcvl


1. k : Knd
2. l : IdLnk
3. ↑(isrcv(k) ∧b lnk(k) = l)
⊢ (↑isrcv(k)) ∧ (lnk(k) = l ∈ IdLnk)
BY
{ (MoveToConcl (-1) THEN AutoBoolCase ⌈isrcv(k)⌉⋅ THEN RW assert_pushdownC 0 THEN Auto) }

---

Latex:



1.  k  :  Knd
2.  l  :  IdLnk
3.  \muparrow{}(isrcv(k)  \mwedge{}\msubb{}  lnk(k)  =  l)
\mvdash{}  (\muparrow{}isrcv(k))  \mwedge{}  (lnk(k)  =  l)


By

(MoveToConcl  (-1)  THEN  AutoBoolCase  \mkleeneopen{}isrcv(k)\mkleeneclose{}\mcdot{}  THEN  RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index