proposition: Lemma is_mod_loop_correct : forall t mds ds p, is_mod_loop t mds ds p = true -> EIS (red_mod E R).
proof: Proof. intros t mds ds p. unfold is_mod_loop. case_eq (mod_rewrites t mds). 2: discr. destruct l. discr. set (us := s::l). set (u := last us default). case_eq (rewrites E u ds). 2: discr. intro us'. set (u' := last us' u). case_eq (split u' p). 2: discr. intros [v w]. case_eq (matches t w); intros. 2: discr. assert (h0 : k us > 0). unfold k, us. simpl. lia. assert (h : u = last_string us). unfold last_string, k, nth. rewrite <- last_nth. refl. exists (seq us h0 v s0). eapply IS_seq. apply H2. rewrite <- h. apply H1. unfold last_string'. rewrite <- h. fold u'. apply H0. hyp. Qed.
imports: Coq(Euclid Wf_nat) CoLoR(Srs LogicUtil SLoop ListUtil NatUtil RelUtil)