proposition: Lemma WF_rp_red_mod : forall E R, forallb (brule bsucceq) E = true -> forallb (brule bsucceq) R = true -> WF (red_mod (filter (brule (neg bsucc)) E) (filter (brule (neg bsucc)) R)) -> WF (red_mod E R).
proof: Proof. intros. set (Rge := filter (brule (neg bsucc)) R). set (Ege := filter (brule (neg bsucc)) E). set (Rgt := removes (@eq_rule_dec Sig) Rge R). set (Egt := removes (@eq_rule_dec Sig) Ege E). apply WF_incl with (red_mod (Egt ++ Ege) (Rgt ++ Rge)). apply red_mod_incl; apply incl_removes_app. apply rule_elimination_mod with (rp:=mkReduction_pair sc_succ sc_succeq cc_succ cc_succeq succ_succeq_compat wf_succ). intros l r h. unfold Rgt in h. rewrite In_removes in h. destruct h. unfold Rge in H3. rewrite (notIn_filter _ (@eq_rule_dec Sig)) in H3. destruct H3. contr. destruct H3. clear H3. apply bsucc_sub. unfold rel. unfold brule, neg in H4. simpl in H4. rewrite negb_lr in H4. hyp. apply incl_compat with R. unfold Rge. apply filter_incl. intros l r h. apply bsucceq_sub. rewrite forallb_forall in H0. change (brule bsucceq (mkRule l r) = true). apply H0. hyp. intros l r h. unfold Egt in h. rewrite In_removes in h. destruct h. unfold Ege in H3. rewrite (notIn_filter _ (@eq_rule_dec Sig)) in H3. destruct H3. contr. destruct H3. clear H3. apply bsucc_sub. unfold rel. unfold brule, neg in H4. simpl in H4. rewrite negb_lr in H4. hyp. apply incl_compat with E. unfold Ege. apply filter_incl. intros l r h. apply bsucceq_sub. rewrite forallb_forall in H. change (brule bsucceq (mkRule l r) = true). apply H. hyp. hyp. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat)