proposition: Lemma modular_termination : well_founded (ddp_step (@union _ (@union _ R1 R2) (@union _ R3 (Pi pi V0 V1)))).
proof: Proof. intros s; apply ddp_necessary; simpl; trivial. apply R123_var'. clear s; intro s; pattern s; apply term_rec3; clear s; trivial. intro x; apply Acc_intro; intros s H; inversion H; subst. inversion H0; subst. destruct t2 as [v2 | f2 l2]. apply False_rect; apply (R123_var' _ _ H3). discriminate. intros f l IHl; generalize (F.Symb.eq_bool_ok f pi); case (F.Symb.eq_bool f pi); [intros f_eq_pi | intros f_diff_pi]. subst f. apply Acc_incl with (one_step (@union _ (@union _ (@union _ R1 R2) R3) (Pi pi V0 V1))). intros t1 t2; apply one_step_incl; clear t1 t2. intros t1 t2 [[H1 | H2] | [H3 | Hpi]]. do 3 left; trivial. do 2 left; right; trivial. left; right; trivial. right; trivial. apply acc_subterms_pi; trivial. intros x t [[H1 | H2] | H3]. apply (R1_var _ _ H1). apply (R2_var _ _ H2). apply (R3_var _ _ H3). intros t1 t2 [[H1 | H2] | H3]. apply (P1 t1 t2 H1). apply (P2 t1 t2 H2). apply (P3 t1 t2 H3). intros t t_in_ll; apply Acc_incl with (one_step (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))). intros t1 t2; apply one_step_incl; clear t1 t2. intros t1 t2 [[[H1 | H2] | H3] | Hpi]. do 2 left; trivial. left; right; trivial. right; left; trivial. right; right; trivial. apply IHl; trivial. apply ddp_simple_criterion_local; simpl; trivial. apply R123_var'. apply R123_reg'. apply def_dec123'. destruct (def_dec12 f) as [D12 | C12]. apply Case12; trivial. intros [ | i p] g k Sub D3. simpl in Sub; injection Sub; clear Sub; intros; subst g k. assert False; [idtac | contradiction]. apply (Incomp123' f); trivial. simpl in Sub; assert (H := nth_error_ok_in i l); destruct (nth_error l i) as [ti | ]; [idtac | discriminate]. destruct (H _ (eq_refl _)) as [ls1 [ls2 [L H']]]; clear H; subst l. assert (Hti : Interp_dom (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) ti). apply acc_interp_dom. apply IHl; apply in_or_app; right; left; trivial. apply (Hti p); trivial. destruct (def_dec3 f) as [D3' | C3]. apply Acc_incl with (ddp_step (@union term (@union term R1 R3) (@union term R2 (Pi pi V0 V1)))). refine (ddp_step_incl _ _ _). intros t1 t2 [[H1 | H2] | [H3 | HPi]]. do 2 left; assumption. right; left; assumption. left; right; assumption. do 2 right; assumption. apply Case3; trivial. intros t t_in_l; rewrite <- Dummy; apply IHl; trivial. apply Acc_intro; intros t H. inversion H as [g k l' s'' l_R_l' _Hm]; clear H; subst. inversion _Hm as [_t s sigma Hm K1 K2]; clear _Hm; subst. destruct Hm as [Hm _Sub]. inversion Hm as [_s [ v | f' k'] p g'' k'' t_R_s Sub Df'' H1 H']; subst. destruct p; discriminate. destruct s as [x | g k]. absurd (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) (Term f' k') (Var x)); trivial. apply R123_var'. simpl in K2; injection K2; clear K2; intros; subst. apply False_rect; destruct t_R_s as [H12 | [H3 | HPi]]. apply C12; apply (Def (@union _ R1 R2) f _ _ H12). apply C3; apply (Def R3 f _ _ H3). apply f_diff_pi; inversion HPi; subst; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)