---

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


1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. (rcv(l,tg) ∈ fpf-domain(da))@i
⊢ ∃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)))
BY
{ InstConcl [⌈rcv(l,tg)⌉]⋅ }

1
.....wf..... 
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. (rcv(l,tg) ∈ fpf-domain(da))@i
⊢ rcv(l,tg) ∈ Knd

2
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. (rcv(l,tg) ∈ fpf-domain(da))@i
⊢ (rcv(l,tg) ∈ fpf-domain(da))
∧ ((↑isl(if isrcv(rcv(l,tg)) then if lnk(rcv(l,tg)) = l then inl tag(rcv(l,tg)) else inr ⋅  fi  else inr ⋅  fi ))
  c∧ (tg
     = outl(if isrcv(rcv(l,tg)) then if lnk(rcv(l,tg)) = l then inl tag(rcv(l,tg)) else inr ⋅  fi  else inr ⋅  fi )
     ∈ Id))

3
.....wf..... 
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. (rcv(l,tg) ∈ fpf-domain(da))@i
5. 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)) ∈ ℙ

---

Latex:



1.  l  :  IdLnk@i
2.  da  :  k:Knd  fp->  Type@i'
3.  tg  :  Id@i
4.  (rcv(l,tg)  \mmember{}  fpf-domain(da))@i
\mvdash{}  \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  ))))


By

InstConcl  [\mkleeneopen{}rcv(l,tg)\mkleeneclose{}]\mcdot{}

---

Home Index