---

Step * 2 of Lemma assert-has-src


1. i : Id
2. k : Knd
3. ↑has-src(i;k)
⊢ source(lnk(k)) = i ∈ Id
BY
{ (DVar `k'
   THEN Repeat (((Unfolds ``has-src isrcv lnk`` (-1)) THEN (Reduce (-1))))
   THEN Auto
   THEN Unfold `lnk` 0
   THEN Reduce 0
   THEN Auto
   THEN (RW assert_pushdownC (-1))
   THEN Auto) }

---

Latex:



1.  i  :  Id
2.  k  :  Knd
3.  \muparrow{}has-src(i;k)
\mvdash{}  source(lnk(k))  =  i


By

(DVar  `k'
  THEN  Repeat  (((Unfolds  ``has-src  isrcv  lnk``  (-1))  THEN  (Reduce  (-1))))
  THEN  Auto
  THEN  Unfold  `lnk`  0
  THEN  Reduce  0
  THEN  Auto
  THEN  (RW  assert\_pushdownC  (-1))
  THEN  Auto)

---

Home Index