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:
\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
ProveCoDatatypeExt
Home
Index