fact: Fixpoint nfb (alpha : T2) : bool := match alpha with zero => true | gcons a b n zero => andb (nfb a) (nfb b) | gcons a b n ((gcons a' b' n' c') as c) => match compare [a', b'] [a, b] with Lt => andb (nfb a) (andb (nfb b) (nfb c)) | _ => false end end.
imports: Coq(Arith List Lia Compare_dec Relations Wellfounded RelationClasses) hydras(Epsilon0) hydras(More_Arith Restriction) hydras(ON_Generic) hydras(rpo.term rpo.rpo) hydras(T2) hydras(Compat815)