---

Step * 1 1 of Lemma assert-graph-rcvset


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))
BY
{ ((Fold `mk_lnk` 0 THEN Fold `rcv` 0) THEN At ⌈Type⌉ (InstConcl [⌈x3⌉;⌈x5⌉])⋅ THEN Auto)⋅ }

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
13. (x3 ∈ S)
⊢ (x5 ∈ S)

---

Latex:



1.  a  :  Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Id@i
2.  b  :  Id@i
3.  S  :  Id  List@i
4.  G  :  \{i:Id|  (i  \mmember{}  S)\}    {}\mrightarrow{}  (\{i:Id|  (i  \mmember{}  S)\}    List)@i
5.  x3  :  Id@i
6.  x5  :  Id@i
7.  x6  :  Id@i
8.  x2  :  Id@i
9.  (x3  \mmember{}  S)
10.  x2  =  b
11.  x6  =  (a  x3  x5)
12.  (x3{}\mrightarrow{}x5)\mmember{}G
\mvdash{}  \mexists{}i,j:Id.  ((i  \mmember{}  S)  \mwedge{}  (j  \mmember{}  S)  \mwedge{}  (i{}\mrightarrow{}j)\mmember{}G  \mwedge{}  ((inl  <<x3,  x5,  x6>,  x2>)  =  rcv((link(a  i  j)  from  i  to  j)\000C,b)))


By

((Fold  `mk\_lnk`  0  THEN  Fold  `rcv`  0)  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  (InstConcl  [\mkleeneopen{}x3\mkleeneclose{};\mkleeneopen{}x5\mkleeneclose{}])\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index