proposition: Lemma acc_interp_acc : forall S1, @inclusion _ S1 R1 -> forall s s', Interp_dom R1 R2 s -> Interp s s' -> Acc (rdp_step (axiom (ddp S1)) (@union _ R1 (Pi pi V0 V1))) s' -> Acc (rdp_step (axiom (ddp S1)) (@union _ R1 R2)) s.
proof: Proof. intros S1 S1_in_R1 s s' Is Hs' Acc_s'; generalize s Is Hs'; clear s Is Hs'; induction Acc_s' as [s' Acc_s' IH]. intros s Is Hs'; apply Acc_intro; intros t t_R_s. assert (It : Interp_dom R1 R2 t). inversion t_R_s as [f l1 l2 t'' l2_R_l1 H ]; subst; clear t_R_s. assert (Is2 : Interp_dom R1 R2 (Term f l2)). inversion l2_R_l1 as [l | k2 k1 l2_R_l1']; clear l2_R_l1; subst. assumption. apply interp_dom_R1_R2_rwr with (Term f l1); trivial. apply general_context; assumption. inversion H as [t'' _s'' sigma K' K1 K2]; clear H; subst. destruct K' as [K' Sub]; inversion K' as [s'' t' p f' l t''_S1_s'' H' Df H1 H2]; clear K'; subst. rewrite <- K2 in Is2. destruct (R1_at_top_dp _ S1_in_R1 _ _ _ _ t''_S1_s'' H' _ Is2) as [sigma' [_ [K _]]]; trivial. destruct (interp_defined _ It) as [t' Ht']. apply (IH t'); trivial. apply (technical_lemma _ S1_in_R1 s s' t t'); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)