proposition: Lemma Q8_strong : forall mark, (forall f, ~defined R (mark f)) -> (forall v u, P u v -> mrel mark (dp R) u v) -> well_founded (rdp_step (axiom P) (union _ (UsableRules R P) (Pi pi V0 V1))) -> well_founded (rest (acc_sub R) (rdp_step (axiom P) R)).
proof: Proof. intros mark mark_ok P_in_dpR Wf t. apply Acc_intro; intros s H; apply Acc_inv with t; trivial. destruct H as [H [_ Ht]]. inversion H as [f l1 l2 s' H1 H2 H3 H4]; clear H; subst. inversion H2 as [_t1 _t2 sigma _H2]; clear H2; subst. assert (_K2 := P_in_dpR _ _ _H2). inversion _K2 as [t1 t2 K2]; clear _K2; subst. inversion K2 as [u1 u2 p f2 k2 H Sub Df2]; subst. destruct t2 as [x2 | g2]. apply False_rect; apply (R_var _ _ H). simpl in H0; injection H0; clear H0; intros; subst. assert (Acc_t : Interp_dom (Term (mark g2) l1)). intros [ | i q] f k Sub' Gf. simpl in Sub'; injection Sub'; clear Sub'; intros; subst. rewrite Gdef' in Gf. inversion Gf as [f l' t [K _]]; subst. apply False_rect; apply (mark_ok g2); constructor 1 with l' t; assumption. simpl in Sub'. generalize (nth_error_ok_in i l1). destruct (nth_error l1 i) as [ai | ]; [ | discriminate]. intro K; destruct (K _ (eq_refl _)) as [kk1 [kk2 [L K1]]]; clear K. apply acc_subterms_3 with q ai; trivial. apply Ht; subst l1; simpl; apply in_or_app; right; left; apply eq_refl. destruct (interp_defined (Term (mark g2) l1)) as [t' It]. apply interp_well_defined; assumption. apply Q8_weak with mark t'; 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)