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 split u p with | None => false | Some (_,w) => match matches t w with | None => false | Some _ => true end end end end.
imports: Coq(Euclid Wf_nat) CoLoR(LogicUtil Srs ListUtil EqUtil RelUtil ListDec NatUtil)