proposition: Lemma polyInterpretationTermination : forall R, lforall (fun r => coef_pos (rulePoly_gt r)) R -> WF (red R).
proof: Proof. intros R H. apply manna_ness with (succ := succ). apply pi_red_ord. apply pi_compat. exact H. Qed.
imports: CoLoR(ATerm ABterm ListUtil VecUtil PositivePolynom AInterpretation ZUtil NaryFunction ARelation RelUtil LogicUtil SN Polynom MonotonePolynom NatUtil ATrs BoundNat AWFMInterpretation ZUtil ACompat AMannaNess)