---

Step * 2 1 of Lemma assert-graph-rcvset


1. a : Id ─→ Id ─→ Id@i
2. b : Id@i
3. S : Id List@i
4. G : Graph(S)@i
5. k : Knd@i
6. i : Id@i
7. j : Id@i
8. (i ∈ S)@i
9. (j ∈ S)@i
10. (i─→j)∈G@i
11. k = rcv((link(a i j) from i to j),b) ∈ Knd@i
⊢ ↑graph-rcvset(a;b;S;G;rcv((link(a i j) from i to j),b))
BY
{ (Unfold `id-graph` 4
   THEN ((ExRepD THEN HypSubst' -1 0) THEN RepUR ``graph-rcvset`` 0 THEN RW assert_pushdownC 0 THEN Auto)⋅
   ) }

---

Latex:



1.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id@i
2.  b  :  Id@i
3.  S  :  Id  List@i
4.  G  :  Graph(S)@i
5.  k  :  Knd@i
6.  i  :  Id@i
7.  j  :  Id@i
8.  (i  \mmember{}  S)@i
9.  (j  \mmember{}  S)@i
10.  (i{}\mrightarrow{}j)\mmember{}G@i
11.  k  =  rcv((link(a  i  j)  from  i  to  j),b)@i
\mvdash{}  \muparrow{}graph-rcvset(a;b;S;G;rcv((link(a  i  j)  from  i  to  j),b))


By

(Unfold  `id-graph`  4
  THEN  ((ExRepD  THEN  HypSubst'  -1  0)
              THEN  RepUR  ``graph-rcvset``  0
              THEN  RW  assert\_pushdownC  0
              THEN  Auto)\mcdot{}
  )

---

Home Index