fact: Definition is_mod_loop t mds ds p := match mod_rewrites t mds with | None => false | Some us => match us with | nil => false | _ => let u := last us default in match rewrites E u ds with | None => false | Some us' => let u' := last us' u in match split u' p with | None => false | Some (_,w) => match matches t w with | None => false | Some _ => true end end end end end.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)