fact: Definition is_loop t ds p := match rewrites t ds with | None => false | Some us => match us with | nil => false | _ => let u := last us default in match subterm_pos u p with | None => false | Some v => match matches t v with | None => false | Some _ => true end end end end.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil ATrs ListUtil RelUtil AMatching ListDec APosition NatUtil)