---

Step * 3 of Lemma assert-has-src


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

---

Latex:



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


By

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

---

Home Index