---

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


1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@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)))
⇐⇒ (rcv(l,tg) ∈ fpf-domain(da))
BY
{ (D 0 THEN D 0) }

1
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))

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

3
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)))

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

---

Latex:



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


By

(D  0  THEN  D  0)

---

Home Index