---

Step * 1 1 1 1 1 1 of Lemma es-dt-dom


1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. x : Knd@i
5. (x ∈ fpf-domain(da))@i
6. True@i
7. tg = tag(x) ∈ Id@i
8. ↑isrcv(x)
9. lnk(x) = l ∈ IdLnk
10. ↑isrcv(x)
11. lnk(x) = l ∈ IdLnk
⊢ rcv(l,tg) = x ∈ Knd
BY
{ ((All (Unfolds ``rcv isrcv lnk tagof``))
   THEN DVar `x'
   THEN All Reduce
   THEN Try (Trivial)
   THEN DVar `x1'
   THEN All Reduce
   THEN Fold `rcv` 0
   THEN EqCD
   THEN Auto) }

---

Latex:



1.  l  :  IdLnk@i
2.  da  :  k:Knd  fp->  Type@i'
3.  tg  :  Id@i
4.  x  :  Knd@i
5.  (x  \mmember{}  fpf-domain(da))@i
6.  True@i
7.  tg  =  tag(x)@i
8.  \muparrow{}isrcv(x)
9.  lnk(x)  =  l
10.  \muparrow{}isrcv(x)
11.  lnk(x)  =  l
\mvdash{}  rcv(l,tg)  =  x


By

((All  (Unfolds  ``rcv  isrcv  lnk  tagof``))
  THEN  DVar  `x'
  THEN  All  Reduce
  THEN  Try  (Trivial)
  THEN  DVar  `x1'
  THEN  All  Reduce
  THEN  Fold  `rcv`  0
  THEN  EqCD
  THEN  Auto)

---

Home Index