proposition: Lemma split_rules : forall R Rlist, (forall l r, R r l <-> In (l,r) Rlist) -> forall P Plist, (forall u v, P v u <-> In (u,v) Plist) -> (forall v t, ~ R t (Var v)) -> forall G, (forall f, G f <-> defined (fun r l => R r l /\ ~ UsableRules R P r l) f) -> (forall r l, R r l <-> (UsableRules R P r l \/ filter_top R G r l)) /\ (forall r l, UsableRules R P r l -> forall g, symb_in_term g r = true -> ~G g).
proof: Proof. intros R Rlist Rlist_ok P Plist Plist_ok R_var G Gdef. assert (Pdec := rel_dec P Plist Plist_ok). destruct (usablerules_dec _ _ Rlist_ok _ _ Plist_ok) as [URlist URlist_ok]. split. intros r l; split; intro H. rewrite URlist_ok. destruct (In_dec eq_term_dec2 (l,r) URlist) as [lr_in_U | lr_not_in_U]. left; assumption. right; split; [assumption | destruct l as [x | f l]]. apply (R_var _ _ H). rewrite Gdef; constructor 1 with l r; split; [ | rewrite URlist_ok]; assumption. destruct H as [[v [u [_ [H _]]]] | [H _]]; assumption. intros r [x | f l] [v [u [H1 [H2 H3]]]] g g_in_r Gg. contradiction H3. rewrite Gdef in Gg; inversion Gg as [g' k t [K1 K2]]; subst g'. apply K2; constructor 1 with v; exists u; split. assumption. split; [assumption | destruct H3 as [f' [H3 H4]]; exists f'; split]. assumption. apply refl_trans_clos_is_trans with f; trivial. right; left; constructor 1 with r; exists (Term f l); split. split; [assumption | apply eq_refl]. split; [ | constructor 1 with k t]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)