---

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

.....wf..... 
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. ∃x:Knd
    ((x ∈ fpf-domain(da))
    ∧ ((↑isl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x))
      c∧ (tg = outl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x) ∈ Id)))
⇐⇒ (rcv(l,tg) ∈ fpf-domain(da))
⊢ ∃x:Knd
   ((x ∈ fpf-domain(da))
   ∧ ((↑isl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x))
     c∧ (tg = outl((λk.if isrcv(k) then if lnk(k) = l then inl tag(k) else inr ⋅  fi  else inr ⋅  fi ) x) ∈ Id)))
  ⇐⇒ (rcv(l,tg) ∈ fpf-domain(da)) ∈ Type
BY
{ (Reduce 0 THEN RepeatFor 3 ((MemCD THEN Try (Complete (Auto)))) THEN RepeatFor 2 (AutoSplit)) }

---

Latex:

---

Latex:
.....wf..... 
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((\mlambda{}k.if  isrcv(k)  then  if  lnk(k)  =  l  then  inl  tag(k)  else  inr  \mcdot{}    fi    else  inr  \mcdot{}    fi  )  x))
            c\mwedge{}  (tg
                  =  outl((\mlambda{}k.if  isrcv(k)  then  if  lnk(k)  =  l  then  inl  tag(k)  else  inr  \mcdot{}    fi    else  inr  \mcdot{}    fi  ) 
                                x))))
\mLeftarrow{}{}\mRightarrow{}  (rcv(l,tg)  \mmember{}  fpf-domain(da))
\mvdash{}  \mexists{}x:Knd
      ((x  \mmember{}  fpf-domain(da))
      \mwedge{}  ((\muparrow{}isl((\mlambda{}k.if  isrcv(k)  then  if  lnk(k)  =  l  then  inl  tag(k)  else  inr  \mcdot{}    fi    else  inr  \mcdot{}    fi  )  x))
          c\mwedge{}  (tg
                =  outl((\mlambda{}k.if  isrcv(k)  then  if  lnk(k)  =  l  then  inl  tag(k)  else  inr  \mcdot{}    fi    else  inr  \mcdot{}    fi  ) 
                              x))))
    \mLeftarrow{}{}\mRightarrow{}  (rcv(l,tg)  \mmember{}  fpf-domain(da))  \mmember{}  Type


By

---

Latex:
(Reduce  0  THEN  RepeatFor  3  ((MemCD  THEN  Try  (Complete  (Auto))))  THEN  RepeatFor  2  (AutoSplit))

---

Home Index