---

Step * of Lemma RankEx2co-ext

∀[S,T:Type].
  RankEx2co(S;T) ≡ lbl:Atom × if lbl =a "LeafT" then T
                              if lbl =a "LeafS" then S
                              if lbl =a "Prod" then RankEx2co(S;T) × S × T
                              if lbl =a "Union" then S × RankEx2co(S;T) + RankEx2co(S;T)
                              if lbl =a "ListProd" then (S × RankEx2co(S;T)) List
                              if lbl =a "UnionList" then T + (RankEx2co(S;T) List)
                              else Void
                              fi 
BY
{ ProveCoDatatypeExt }

---

Latex:

---

Latex:
\mforall{}[S,T:Type].
    RankEx2co(S;T)  \mequiv{}  lbl:Atom  \mtimes{}  if  lbl  =a  "LeafT"  then  T
                                                            if  lbl  =a  "LeafS"  then  S
                                                            if  lbl  =a  "Prod"  then  RankEx2co(S;T)  \mtimes{}  S  \mtimes{}  T
                                                            if  lbl  =a  "Union"  then  S  \mtimes{}  RankEx2co(S;T)  +  RankEx2co(S;T)
                                                            if  lbl  =a  "ListProd"  then  (S  \mtimes{}  RankEx2co(S;T))  List
                                                            if  lbl  =a  "UnionList"  then  T  +  (RankEx2co(S;T)  List)
                                                            else  Void
                                                            fi 


By

---

Latex:
ProveCoDatatypeExt

---

Home Index