fact: Definition bsucceq t u := match rpo_eval (term_of_aterm t) (term_of_aterm u) with | Some Greater_than | Some Equivalent => true | _ => false end.
imports: CoLoR(LogicUtil ATerm VecUtil) CoLoR(term_spec EqUtil) CoLoR(NatUtil) Coq(List Relations) CoLoR(term SN ASubstitution) CoLoR(rpo rpo_extension) CoLoR(ARedPair ARelation RelUtil BoolUtil)