---

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

.....subterm..... T:t
2:n
1. l : IdLnk@i
2. da : k:Knd fp-> Type@i'
3. tg : Id@i
4. x : Knd@i
⊢ (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
{ (SplitOnConclITE
   THEN Try (Complete (Auto))
   THEN Try ((Reduce 0 THEN Complete (Auto)))
   THEN SplitOnConclITE
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN Try ((Reduce 0 THEN Complete (Auto)))) }

---

Latex:


.....subterm.....  T:t
2:n
1.  l  :  IdLnk@i
2.  da  :  k:Knd  fp->  Type@i'
3.  tg  :  Id@i
4.  x  :  Knd@i
\mvdash{}  (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  )))
    \mmember{}  \mBbbP{}


By

(SplitOnConclITE
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((Reduce  0  THEN  Complete  (Auto)))
  THEN  SplitOnConclITE
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((Reduce  0  THEN  Complete  (Auto))))

---

Home Index