---

Step * 1 1 of Lemma assert-rcvset


1. a : Id@i
2. b : Id@i
3. S : Id List@i
4. x3 : Id@i
5. x5 : Id@i
6. x6 : Id@i
7. x2 : Id@i
8. (x2 = b ∈ Id) ∧ (x6 = a ∈ Id) ∧ (x3 ∈ S) ∧ (x5 ∈ S)
⊢ ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ ((inl <<x3, x5, x6>, x2>) = rcv((link(a) from i to j),b) ∈ Knd))
BY
{ ((Fold `mk_lnk` 0 THEN Fold `rcv` 0) THEN InstConcl [⌈x3⌉;⌈x5⌉]⋅ THEN Auto) }

---

Latex:



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


By

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

---

Home Index