---

Step * 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
    ((x ∈ fpf-domain(da))
    ∧ ((↑isl(if isrcv(x) then if lnk(x) = l then inl tag(x) else inr ⋅  fi  else inr ⋅  fi ))
      c∧ (tg = outl(if isrcv(x) then if lnk(x) = l then inl tag(x) else inr ⋅  fi  else inr ⋅  fi ) ∈ Id)))@i
⊢ (rcv(l,tg) ∈ fpf-domain(da))
BY
{ (((((ExRepD THEN NthHypEq 5 THEN EqCD THEN Auto THEN (SplitOnHypITE (-2))) THENA Auto)
     THEN (Reduce (-3))
     THEN Try (Trivial)
     THEN (SplitOnHypITE (-3)))
    THENA Auto
    )
   THEN (Reduce (-4))
   THEN Try (Trivial)
   THEN (SplitOnHypITE (-3))
   THEN Auto
   THEN (SplitOnHypITE (-4))
   THEN Auto
   THEN (Reduce (-5))) }

1
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

---

Latex:



1.  l  :  IdLnk@i
2.  da  :  k:Knd  fp->  Type@i'
3.  tg  :  Id@i
4.  \mexists{}x:Knd
        ((x  \mmember{}  fpf-domain(da))
        \mwedge{}  ((\muparrow{}isl(if  isrcv(x)  then  if  lnk(x)  =  l  then  inl  tag(x)  else  inr  \mcdot{}    fi    else  inr  \mcdot{}    fi  ))
            c\mwedge{}  (tg
                  =  outl(if  isrcv(x)  then  if  lnk(x)  =  l  then  inl  tag(x)  else  inr  \mcdot{}    fi    else  inr  \mcdot{}    fi  ))))@i
\mvdash{}  (rcv(l,tg)  \mmember{}  fpf-domain(da))


By

(((((ExRepD  THEN  NthHypEq  5  THEN  EqCD  THEN  Auto  THEN  (SplitOnHypITE  (-2)))  THENA  Auto)
      THEN  (Reduce  (-3))
      THEN  Try  (Trivial)
      THEN  (SplitOnHypITE  (-3)))
    THENA  Auto
    )
  THEN  (Reduce  (-4))
  THEN  Try  (Trivial)
  THEN  (SplitOnHypITE  (-3))
  THEN  Auto
  THEN  (SplitOnHypITE  (-4))
  THEN  Auto
  THEN  (Reduce  (-5)))

---

Home Index