fact: Fixpoint pp0 (alpha : T1) : ppT1 := match alpha with | zero => PP_fin 0 | cons zero n zero => PP_fin (S n) | cons one 0 zero => ω | cons one 0 beta => (ω + pp0 beta)%pT1 | cons one n zero => (ω * (S n))%pT1 | cons one n beta => (ω * (S n) + pp0 beta)%pT1 | cons alpha 0 zero => (ω ^ pp0 alpha)%pT1 | cons alpha 0 beta => (ω ^ pp0 alpha + pp0 beta)%pT1 | cons alpha n zero => (ω ^ pp0 alpha * (S n))%pT1 | cons alpha n beta => (ω ^ pp0 alpha * (S n) + pp0 beta)%pT1 end.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)