proposition: Lemma rwr_at_top_H : forall l r, R r l -> (match l with Var _ => False | Term g _ => ~G g end) -> forall sigma, Interp_dom (apply_subst sigma r) -> Interp_dom (apply_subst sigma l) -> forall s' t', Interp (apply_subst sigma l) s' -> Interp (apply_subst sigma r) t' -> rwr (union _ (fun r' l' => In (r',l') ((r,l) :: nil)) (Pi pi V0 V1)) t' s'.
proof: Proof. intros l r K K' sigma Acc_rs Acc_ls s' t' Il Ir. destruct (interp_subst l sigma Acc_ls) as [sigma' Isigma]. assert (K'' : t' = apply_subst sigma' r). apply interp_unicity with (apply_subst sigma r); trivial. apply interp_well_defined; assumption. apply interp_in_H. destruct l as [ | f k]. contradiction. intros g g_in_r. destruct (Gdec _ _ Rlist_ok _ _ Plist_ok g) as [not_Gg | Gg]. rewrite Gdef'; assumption. apply Hclosed with f; trivial. constructor 1 with r; exists (Term f k); split. constructor 1; trivial. split; [ | apply Gdef]. assumption. rewrite Gdef'; assumption. intros x x_in_r; apply Isigma; apply R_reg with r; trivial. subst t'; assert (K'' := proj1 (rwr_interp_subst _ _ Acc_ls _ sigma' Il Isigma)). inversion K''; clear K''; subst. left; left; constructor; do 2 left; apply eq_refl. apply trans_clos_is_trans with (apply_subst sigma' l). left; left; constructor; do 2 left; apply eq_refl. apply trans_incl with (one_step (Pi pi V0 V1)); trivial. refine (one_step_incl _ _ _); intros; right; 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)