---

Step * 2 of Lemma assert-rcvset


1. a : Id@i
2. b : Id@i
3. S : Id List@i
4. k : Knd@i
5. ∃i,j:Id. ((i ∈ S) ∧ (j ∈ S) ∧ (k = rcv((link(a) from i to j),b) ∈ Knd))@i
⊢ ↑rcvset(a;b;S;k)
BY
{ ((ExRepD THEN HypSubst' -1 0) THEN RepUR ``rcvset`` 0 THEN RW assert_pushdownC 0 THEN Auto) }

---

Latex:



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


By

((ExRepD  THEN  HypSubst'  -1  0)  THEN  RepUR  ``rcvset``  0  THEN  RW  assert\_pushdownC  0  THEN  Auto)

---

Home Index