---

Step * 1 of Lemma assert-rcvset


1. a : Id@i
2. b : Id@i
3. S : Id List@i
4. k : Knd@i
5. ↑rcvset(a;b;S;k)@i
⊢ ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (k = rcv((link(a) from i to j),b) ∈ Knd))
BY
{ ((D -2 THEN Try ((D -2 THEN RepeatFor 2 (D -3))))
   THEN ((RepUR ``rcvset isrcv tagof lnk`` -1⋅ THEN Auto) THEN (RW assert_pushdownC (-1) THENA Auto))⋅
   ) }

1
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))

---

Latex:



1.  a  :  Id@i
2.  b  :  Id@i
3.  S  :  Id  List@i
4.  k  :  Knd@i
5.  \muparrow{}rcvset(a;b;S;k)@i
\mvdash{}  \mexists{}i,j:Id.  ((i  \mmember{}  S)  \mwedge{}  (j  \mmember{}  S)  \mwedge{}  (k  =  rcv((link(a)  from  i  to  j),b)))


By

((D  -2  THEN  Try  ((D  -2  THEN  RepeatFor  2  (D  -3))))
  THEN  ((RepUR  ``rcvset  isrcv  tagof  lnk``  -1\mcdot{}  THEN  Auto)  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto))\mcdot{}
  )

---

Home Index