fact: Variables (succ succ_eq : relation term) (Hredord : weak_rewrite_ordering succ succ_eq) (Hreword : rewrite_ordering succ_eq) (Habsorb : absorbs_left succ succ_eq) (HcompR : compat succ_eq R) (HcompDP : compat succ_eq (dp R)) (Hwf : WF succ) (Hcycle : forall a l, length l < length DP -> cycle_min dp_graph a l -> exists b, In b (a :: l) /\ succ (lhs b) (rhs b)).
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)