proposition: Lemma trans_rwr_rule_H_not_H : forall s t, Acc (one_step R) s -> trans_clos (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' K; induction K as [t1 t2 K | t1 t2 t3 K1 K2]. apply rwr_rule_H_not_H; trivial. apply acc_one_step_interp_dom; assumption. apply acc_one_step_interp_dom; apply Acc_inv with t2; assumption. intros t3' t1' I3 I1. assert (Acc_t2 : Interp_dom t2). apply acc_one_step_interp_dom; apply Acc_incl with (trans_clos (one_step R)). do 3 intro; left; assumption. apply Acc_inv with t3; trivial. apply acc_trans; assumption. destruct (interp_defined _ (interp_well_defined _ Acc_t2)) as [t2' I2]. apply trans_clos_is_trans with t2'. apply rwr_rule_H_not_H with t2 t1; trivial. apply acc_one_step_interp_dom; apply Acc_incl with (trans_clos (one_step R)). do 3 intro; left; assumption. apply Acc_inv with t3. apply acc_trans; assumption. right with t2; assumption. apply IHK2; trivial. 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)