proposition: Lemma rwr_rule_H_not_H : forall s t, Interp_dom s -> Interp_dom t -> one_step R t s -> forall s' t', Interp s s' -> Interp t t' -> rwr (union _ (UsableRules R P) (Pi pi V0 V1)) t' s'.
proof: Proof. intros s t Acc_s Acc_t K s' t' Is It. destruct (split_rules _ _ Rlist_ok _ _ Plist_ok R_var G Gdef') as [U1 U2]. assert (Erule := one_step_one_rule R _ _ K). destruct Erule as [r [l [K1 K2]]]. destruct l as [x | f l]. apply False_rect; apply (R_var _ _ K1). destruct (Gdec _ _ Rlist_ok _ _ Plist_ok f) as [f_in_H | f_not_in_H]. apply trans_incl with (one_step (union term (fun r' l' : term => In (r', l') ((r, Term f l) :: nil)) (Pi pi V0 V1))). intros x y; apply one_step_incl; clear x y. intros x y [[K3 | Abs] | K3]. injection K3; clear K3; intros; subst x y; left. rewrite U1 in K1; destruct K1 as [K1 | K1]. assumption. destruct K1 as [_ K1]; apply False_rect; apply f_in_H; rewrite <- Gdef'; assumption. contradiction. right; assumption. rewrite <- Gdef' in f_in_H. apply (rwr_rule_H _ _ K1 f_in_H _ _ Acc_s Acc_t K2 _ _ Is It). apply trans_incl with (one_step (Pi pi V0 V1)). intros x y; apply one_step_incl; clear x y. intros x y K3; right; assumption. rewrite <- Gdef' in f_not_in_H. apply (rwr_rule_not_H _ _ K1 f_not_in_H _ _ Acc_s Acc_t K2 _ _ Is It). 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)