proposition: Lemma Case12 : forall f l, defined (@union _ R1 R2) f -> (Interp_dom (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) (Term f l)) -> Acc (ddp_step (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))) (Term f l).
proof: Proof. intros f l D12 It. inversion D12 as [f' k u H12]; subst. assert (Ts := T12 _ It). assert (D12' : match Term f l with | Var _ => False | Term g _ => defined (@union _ R1 R2) g end). trivial. generalize (Term f l) Ts D12' It; clear f l It Ts D12' D12 H12. intros t Acc_t; induction Acc_t as [[ v | f l] Acc_t IH]; intros D12f It. contradiction. apply Acc_intro; intros t H. assert (Simple_step : forall l (IH : forall y : term, rdp_step (axiom (ddp (@union term R1 R2))) (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) y (Term f l) -> match y with | Var _ => False | Term g _ => defined (@union term R1 R2) g end -> Interp_dom (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) y -> Acc (ddp_step (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))) y) (It : Interp_dom (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) (Term f l)) (t : term) (H : axiom (ddp (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))) t (Term f l)), Acc (ddp_step (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)))) t). clear l Acc_t IH It t H; intros l IH It t Hm. inversion Hm as [_t s sigma _Hm K1 K2]; subst. destruct _Hm as [_Hm _Sub]. inversion _Hm as [_s t p g'' k'' t_R_s Sub Df'' H1 H']; clear _Hm; subst. destruct t as [v | f' k']. destruct p; discriminate. destruct (split_dp_top _ _ _ _ Hm) as [D12' | [D13 | D3]]; clear Hm. destruct D12' as [Df Dg]. assert (t_R12_s : (@union term R1 R2) (Term f' k') s). clear k; destruct s as [ v | g k]. absurd (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) (Term f' k') (Var v)); trivial. intros [[H1 | H2] | [H3 | Hpi]]. apply (R1_var _ _ H1). apply (R2_var _ _ H2). apply (R3_var _ _ H3). inversion Hpi. simpl in K2; injection K2; clear K2; intros H' f_eq_g; subst. destruct t_R_s as [H12 | H3']; trivial. destruct module123' as [M]. clear u; inversion Df as [f'' l u H12]; subst. assert (F := M f _ _ (Def (@union _ R3 (Pi pi V0 V1)) f k (Term f' k') H3') H12). simpl in F; destruct (symb_in_term f u). discriminate. rewrite eq_symb_bool_refl in F; discriminate. assert (H : rdp_step (axiom (ddp (@union term R1 R2))) (@union term (@union term R1 R2) (@union term R3 (Pi pi V0 V1))) (Term g'' (map (apply_subst sigma) k'')) (Term f l)). apply Rdp_step with l. left. clear k; destruct s as [ v | g k]. absurd ((@union term R1 R2) (Term f' k') (Var v)); trivial. intros [H1 | H2]. apply (R1_var _ _ H1). apply (R2_var _ _ H2). simpl in K2; injection K2; clear K2; intros H' f_eq_g; subst. refine (instance _ (Term g'' k'') (Term f k) sigma _). split; [apply (Dp (@union _ R1 R2) (Term f k) (Term f' k') p g'' k'') | idtac]; trivial. apply IH; trivial. assert (s_not_in_F3 : forall g : symbol, symb_in_term g s = true -> ~ defined (@union term R3 (Pi pi V0 V1)) g). intros g g_in_s D3g. destruct module123' as [M]. assert (H'' := M g _ _ D3g t_R12_s). change ((symb_in_term g (Term f' k') || (symb_in_term g s || false))%bool = false) in H''. rewrite g_in_s in H''; destruct (symb_in_term g (Term f' k')); discriminate. destruct s as [v | ff ll]. absurd (@union term R1 R2 (Term f' k') (Var v)); trivial. apply R12_var. assert (f'k'_not_in_F3 : forall g : symbol, symb_in_term g (Term f' k') = true -> ~ defined (@union term R3 (Pi pi V0 V1)) g). intros g g_in_s D3g. destruct module123' as [M]. assert (H'' := M g _ _ D3g t_R12_s). pattern (Term f' k') in H''; simpl symb_in_term_list in H''; cbv beta in H''. simpl symb_in_term_list in H''; fold symb_in_term_list in H''. simpl in g_in_s; fold symb_in_term_list in g_in_s. rewrite g_in_s in H''; discriminate. assert (interp_dom_var : forall v, In v (var_list (Term ff ll)) -> Interp_dom (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) (apply_subst sigma (Var v))). intros v v_in_s'. rewrite <- K2 in It. exact (interp_dom_subst (@union term R1 R2) (@union term R3 (Pi pi V0 V1)) _ sigma It v v_in_s'). intros [ | i q] h kk Sub' D3h. simpl in Sub'; injection Sub'; clear Sub'; intros; subst. apply False_rect. destruct module123' as [M]. inversion Dg as [g' kk v H1 H2]; subst. generalize (M h _ _ D3h H1); simpl. destruct (symb_in_term h v). discriminate. rewrite eq_symb_bool_refl; discriminate. generalize (subterm_in_instantiated_term _ _ _ Sub'). case_eq (subterm_at_pos (Term g'' k'') (i :: q)). intros t Sub4 K. assert (Sub5 := subterm_in_subterm _ _ _ Sub Sub4). destruct t as [v | h' ll']. assert (v_in_s : In v (var_list (Term ff ll))). apply R12_reg with (Term f' k'); trivial. apply var_in_subterm with (Var v) (p ++ i :: q); trivial. left; trivial. apply (interp_dom_var v v_in_s nil); trivial. rewrite K; trivial. simpl in K; injection K; clear K; intros; subst. absurd (defined (@union term R3 (Pi pi V0 V1)) h'); trivial. apply f'k'_not_in_F3. rewrite (symb_in_subterm h' _ _ Sub5); trivial. simpl; rewrite eq_symb_bool_refl; trivial. intros _ [v [q' [q'' [H1 [v_in_g''k'' [Sub3 Sub4]]]]]]. assert (v_in_s : In v (var_list (Term ff ll))). apply R12_reg with (Term f' k'); trivial. apply var_in_subterm with (Term g'' k'') p; trivial. apply (interp_dom_var v v_in_s q''); trivial. destruct D13 as [D3 _]. destruct module123' as [M]. clear k u; inversion D12f as [g k u H12]; subst. inversion D3 as [g' k''' u' H3]; subst. assert (F := M f _ _ (Def (@union _ R3 (Pi pi V0 V1)) f k''' u' (or_introl _ H3)) H12). simpl in F; destruct (symb_in_term f u). discriminate. simpl in F; revert F; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intros f_diff_f; absurd (f =f); trivial]. intro; discriminate. destruct D3 as [D3 _]. destruct module123' as [M]. clear k u; inversion D12f as [g k u H12]; subst. inversion D3 as [g' k''' u' H3]; subst. assert (F := M f _ _ (Def (@union _ R3 (Pi pi V0 V1)) f k''' u' (or_introl _ H3)) H12). simpl in F; destruct (symb_in_term f u). discriminate. rewrite eq_symb_bool_refl in F; discriminate. clear k; inversion H as [g k l' s'' l_R_l' Hm]; clear H; subst. apply (Simple_step l'); trivial. intros [v | g k] H D12 Iu. contradiction. apply IH; trivial. inversion H as [g' k' l'' s''' l'_R_l'' Hm']; clear H; subst. apply Rdp_step with l''; trivial. apply refl_trans_clos_is_trans with l'; trivial. intros [ | i p] g k Sub Dg. simpl in Sub; injection Sub; clear Sub; intros; subst g k. assert False; [apply (Incomp123' f); trivial | contradiction]. inversion l_R_l' as [l1 | l1 l1' l1_R_l1']; clear l_R_l'; subst. apply (It (i :: p)); trivial. assert (It' := interp_dom_R1_R2_rwr _ _ module123' def_dec3' R12_reg R3_var' _ _ It (general_context _ f _ _ l1_R_l1')). apply (It' (i :: p)); trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)