---

Step * 1 of Lemma rcv_one_one


1. l1 : IdLnk
2. l2 : IdLnk
3. tg1 : Id
4. tg2 : Id
5. rcv(l1,tg1) = rcv(l2,tg2) ∈ Knd
⊢ {(l1 = l2 ∈ IdLnk) ∧ (tg1 = tg2 ∈ Id)}
BY
{ ((Unfolds ``Knd rcv`` (-1)) THEN Unfold `guard` 0) }

1
1. l1 : IdLnk
2. l2 : IdLnk
3. tg1 : Id
4. tg2 : Id
5. (inl <l1, tg1>) = (inl <l2, tg2>) ∈ (IdLnk × Id + Id)
⊢ (l1 = l2 ∈ IdLnk) ∧ (tg1 = tg2 ∈ Id)

---

Latex:



1.  l1  :  IdLnk
2.  l2  :  IdLnk
3.  tg1  :  Id
4.  tg2  :  Id
5.  rcv(l1,tg1)  =  rcv(l2,tg2)
\mvdash{}  \{(l1  =  l2)  \mwedge{}  (tg1  =  tg2)\}


By

((Unfolds  ``Knd  rcv``  (-1))  THEN  Unfold  `guard`  0)

---

Home Index