---

Step * 1 1 1 1 3 2 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
⊢ (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))
BY
{ ((((Unfolds ``isrcv rcv lnk tagof`` 0 THEN Reduce 0 THEN Fold `rcv` 0 THEN SplitOnConclITE) THENA Auto)
    THENL [Reduce 0; (D (-1))]
   )
   THEN Auto
   ) }

---

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{}  (rcv(l,tg)  \mmember{}  fpf-domain(da))
\mwedge{}  ((\muparrow{}isl(if  isrcv(rcv(l,tg))
    then  if  lnk(rcv(l,tg))  =  l  then  inl  tag(rcv(l,tg))  else  inr  \mcdot{}    fi 
    else  inr  \mcdot{} 
    fi  ))
    c\mwedge{}  (tg
          =  outl(if  isrcv(rcv(l,tg))
              then  if  lnk(rcv(l,tg))  =  l  then  inl  tag(rcv(l,tg))  else  inr  \mcdot{}    fi 
              else  inr  \mcdot{} 
              fi  )))


By

((((Unfolds  ``isrcv  rcv  lnk  tagof``  0  THEN  Reduce  0  THEN  Fold  `rcv`  0  THEN  SplitOnConclITE)
      THENA  Auto
      )
    THENL  [Reduce  0;  (D  (-1))]
  )
  THEN  Auto
  )

---

Home Index