fact: Fixpoint exp (alpha beta : T1) :T1 := match alpha ,beta with | _, zero => cons zero 0 zero | cons zero 0 _ , _ => cons zero 0 zero | zero, _ => zero | x , cons zero n' _ => exp_F x (S n') | cons zero n _, cons (cons zero 0 zero) n' b' => ((cons (cons zero n' zero) 0 zero) * ((cons zero n zero) ^ b')) | cons zero n _, cons a' n' b' => (omega_term (omega_term (a' - 1) n') 0) * ((cons zero n zero) ^ b') | cons a n b, cons a' n' b' => ((omega_term (a * (cons a' n' zero)) 0) * ((cons a n b) ^ b')) end where "alpha ^ beta " := (exp alpha beta) : t1_scope.
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)