proposition: Lemma Q8_weak : forall mark, (forall f, ~defined R (mark f)) -> (forall v u, P u v -> mrel mark (dp R) u v) -> forall s, Interp_dom s -> forall s', Interp s s' -> Acc (rdp_step (axiom P) (union _ (UsableRules R P) (Pi pi V0 V1))) s' -> Acc (rest (acc_sub R) (rdp_step (axiom P) R)) s.
proof: Proof. intros mark mark_ok P_in_dpR. assert (acc_rdp_var : forall x, Acc (rest (acc_sub R) (rdp_step (axiom P) R)) (Var x)). intros x; apply Acc_intro; intros s [H _]. inversion H as [f l1 l2 t3 H1 H2]; subst. intros s Acc_s s' Is Acc_s'; revert s Acc_s Is. induction Acc_s' as [s' Acc_s'' IH]. assert (Acc_s' : Acc (rdp_step (axiom P) (union _ (UsableRules R P) (Pi pi V0 V1))) s'). apply Acc_intro; exact Acc_s''. clear Acc_s''. intros s Acc_s Is. destruct s as [x | f ls]. apply acc_rdp_var. destruct (Gdec _ _ Rlist_ok _ _ Plist_ok f) as [f_in_H | f_not_in_H]; [ rewrite <- Gdef' in f_in_H | rewrite <- Gdef' in f_not_in_H]. apply Acc_intro; intros t [K [Acc_sub_t Acc_sub_s]]. assert (Acc_t := interp_dom_interp_dom_2 mark P_in_dpR _ _ Acc_sub_s Acc_sub_t K Acc_s). destruct (interp_defined _ (interp_well_defined _ Acc_t)) as [t' It]. apply IH with t'; trivial. inversion K as [_f _ls l H1 H2 H3 H4 H5]; clear K; subst. inversion H3 as [_v _fl sigma H1 H4 H5']; clear H3; subst. assert (_K := P_in_dpR _ _ H1). inversion _K as [v fl K]; subst. inversion K as [fl' r p g lv H0 Sub Dg]; clear K; subst. inversion Is as [ | f' _ls ls' lls _ H8 H9 Ills | ]; [subst f' _ls s' | absurd (G f); assumption]. assert (g_in_H := head_P_in_H mark P_in_dpR _ _ sigma _ _ H1 (eq_refl _)). inversion It as [ | g' lt lt' llt _ H4 H5 Illt | ]; [ subst g' t' | absurd (G (mark g)); assumption]. assert (Acc_fl := interp_dom_interp_dom_1 _ _ _ f_in_H Acc_sub_s H2). rewrite <- H5' in Acc_fl; destruct (interp_subst _ sigma Acc_fl) as [sigma' Isigma]. destruct (interp_defined _ (interp_well_defined _ Acc_fl)) as [fl' Ifl]. rewrite H5' in Ifl; inversion Ifl as [ | f' _l l' ll _ H10 H11 Ill | ]; [subst f' _l fl' | absurd (G f); assumption]. apply rwr_subterm_rdp_rdp with l'. subst; revert Ills Ill Acc_sub_s H2; clear -R_reg Rlist_ok P Plist Plist_ok Gdef' V0_diff_V1 R_var; revert ll. induction lls as [ | [s s'] lls]; intros [ | [u u'] ll] Ills Ill Acc_sub_s K. left. generalize (refl_trans_clos_one_step_list_length_eq K); intro; discriminate. generalize (refl_trans_clos_one_step_list_length_eq K); intro; discriminate. simpl in K; rewrite refl_trans_clos_one_step_list_head_tail in K. destruct K as [K1 K2]. simpl; rewrite refl_trans_clos_one_step_list_head_tail; split. assert (Acc_s : Acc (one_step R) s). apply Acc_sub_s; left; apply eq_refl. inversion K1; subst. assert (Acc_s' : Acc interp_call s). apply interp_well_defined; apply acc_one_step_interp_dom; assumption. rewrite (interp_unicity s Acc_s' s' u'). left. apply Ills; left; apply eq_refl. apply Ill; left; apply eq_refl. right; apply trans_rwr_rule_H_not_H with s u; trivial. apply Ills; left; apply eq_refl. apply Ill; left; apply eq_refl. apply IHlls; trivial. intros; apply Ills; right; assumption. intros; apply Ill; right; assumption. do 2 intro; apply Acc_sub_s; right; assumption. assert (Acc_sub : acc_sub R (Term f l)). unfold acc_sub; apply (rwr_sub_acc_sub_acc_sub R _ _ H2 Acc_sub_s). rewrite <- H5' in Ifl. generalize (rwr_interp_subst _ _ Acc_fl (Term f l') sigma' Ifl Isigma). destruct fl as [x | _f _l]. apply False_rect; apply (R_var _ _ H0). simpl in H5'; injection H5'; intros; subst f. apply rwr_subterm_rdp_rdp with (map (apply_subst sigma') _l). destruct H7 as [_ H7]. generalize (H7 f_in_H); clear H7; intros [_ H7]. apply refl_trans_incl with (one_step_list (one_step (Pi pi V0 V1))); trivial. do 2 intro; apply one_step_list_incl. do 2 intro; apply one_step_incl. do 3 intro; right; assumption. assert (t'_eq_glvs' : Term (mark g) lt' = apply_subst sigma' (Term (mark g) lv)). apply (interp_unicity _ (interp_well_defined _ Acc_t)); trivial. apply interp_in_H. intros g' g'_glv. rewrite symb_in_term_unfold in g'_glv. generalize (eq_symb_bool_ok g' (mark g)); destruct (eq_symb_bool g' (mark g)). intro; subst g'; assumption. simpl in g'_glv; intros _. rewrite Gdef'. intro Dg'; inversion Dg' as [g'' k t [K K']]; subst g''; apply K'. exists (mark_term mark (Term g lv)); exists (mark_term mark (Term _f _l)); split; [ | split]; trivial. exists g'; split; [ | left]. rewrite symb_in_term_unfold; simpl; rewrite g'_glv. destruct (eq_symb_bool g' (mark g)); apply eq_refl. intros x x_in_lv; apply Isigma. apply (R_reg _ _ H0 x). apply var_in_subterm with (Term g lv) p; trivial. rewrite t'_eq_glvs'. apply Rdp_step with (map (apply_subst sigma') _l). left. apply (instance P (Term (mark g) lv) (Term (mark _f) _l) sigma'); trivial. apply Acc_intro; intros s [H _]; inversion H; clear H; subst. inversion H4 as [_t1 _t2 sigma]; clear H4; subst. assert (_K1 := P_in_dpR _ _ H). inversion _K1 as [t1 t2 K1]; subst. inversion K1; clear K1; subst. destruct t2 as [x2 | g2 k2]. apply False_rect; apply (R_var _ _ H0). simpl in H1; injection H1; clear H1; intros; subst. rewrite Gdef' in f_not_in_H. apply False_rect; apply (mark_ok g2). inversion f_not_in_H as [g2' l t [H' _]]. constructor 1 with l 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)