---

Step * 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. ↑graph-rcvset(a;b;S;G;k)@i
⊢ ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (i─→j)∈G ∧ (k = rcv((link(a i j) from i to j),b) ∈ Knd))
BY
{ (Unfold `id-graph` 4
   THEN (D -2 THEN Try ((D -2 THEN RepeatFor 2 (D -3))))
   THEN ((RepUR ``graph-rcvset isrcv tagof lnk`` -1⋅ THEN Try (Trivial))
         THEN MoveToConcl (-1)
         THEN AutoBoolCase ⌈x3 ∈b S)⌉⋅
         THEN (D 0 THENA Auto)
         THEN (RW assert_pushdownC (-1) THENA Auto)
         THEN Auto
         THEN Fold `id-graph-edge` (-1))⋅) }

1
1. a : Id ─→ Id ─→ Id@i
2. b : Id@i
3. S : Id List@i
4. G : {i:Id| (i ∈ S)}  ─→ ({i:Id| (i ∈ S)}  List)@i
5. x3 : Id@i
6. x5 : Id@i
7. x6 : Id@i
8. x2 : Id@i
9. (x3 ∈ S)
10. x2 = b ∈ Id
11. x6 = (a x3 x5) ∈ Id
12. (x3─→x5)∈G
⊢ ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (i─→j)∈G ∧ ((inl <<x3, x5, x6>, x2>) = rcv((link(a i j) from i to j),b) ∈ Knd))

---

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.  \muparrow{}graph-rcvset(a;b;S;G;k)@i
\mvdash{}  \mexists{}i,j:Id.  ((i  \mmember{}  S)  \mwedge{}  (j  \mmember{}  S)  \mwedge{}  (i{}\mrightarrow{}j)\mmember{}G  \mwedge{}  (k  =  rcv((link(a  i  j)  from  i  to  j),b)))


By

(Unfold  `id-graph`  4
  THEN  (D  -2  THEN  Try  ((D  -2  THEN  RepeatFor  2  (D  -3))))
  THEN  ((RepUR  ``graph-rcvset  isrcv  tagof  lnk``  -1\mcdot{}  THEN  Try  (Trivial))
              THEN  MoveToConcl  (-1)
              THEN  AutoBoolCase  \mkleeneopen{}x3  \mmember{}\msubb{}  S)\mkleeneclose{}\mcdot{}
              THEN  (D  0  THENA  Auto)
              THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
              THEN  Auto
              THEN  Fold  `id-graph-edge`  (-1))\mcdot{})

---

Home Index