fact: Fixpoint tSize {G : CFGV} {gs : (GSym G)} (t : Term gs) {struct t} : nat := match t with | tleaf _ _ => 1 | vleaf vcc var => 1 | tnode _ mix => mSize mix end with pSize {G : CFGV} {gs : (GSym G)} (p : Pattern gs) {struct p} : nat := match p with | ptleaf _ _ => 1 | pvleaf vcc var => 1 | pnode _ mix => mSize mix | embed _ t => 1 + tSize t end with mSize {G : CFGV} {lgs : list (bool * GSym G)} (pts : Mixture lgs) : nat := match pts with | mnil => 1 | mtcons _ _ ph ptl => (tSize ph) + (mSize ptl) | mpcons _ _ ph ptl => (pSize ph) + (mSize ptl) end.
imports: CFGV Omega