proposition: Lemma acc_build : well_founded prec -> forall f l, Acc rpo (Term f (map (fun sn_tt => tt sn_tt) l)).
proof: Proof. intros wf_prec f l; refine (well_founded_induction_type (wf_rpo_term wf_prec) (fun f_l => match f_l with | (f,l) => Acc rpo (Term f (map (fun sn_tt : SN_term => tt sn_tt) l)) end) _ (f,l)). clear f l; intros x IH; destruct x; rename s into f. apply Acc_intro; intros t; pattern t; apply term_rec3; clear t. intros v _; apply Acc_intro; intros u lt_u_t; inversion lt_u_t. intros g l' IH' lt_t_s; inversion lt_t_s. subst t f0 l0; assert (Acc rpo s). apply (in_sn_sn _ _ H2). inversion H3; subst s; trivial; apply Acc_inv with t; trivial. subst g0 l'0 f0 l0; assert (forall s', In s' l' -> Acc rpo s'). intros s' In_s'; apply IH'; trivial; apply H4; trivial. rewrite <- (projection_list_of_SN_terms l' H); apply (IH (g,(build_list_of_SN_terms l' H))); simpl; elim (F.eq_symbol_dec g f); intro eq1; trivial; subst g; generalize (prec_antisym _ H2); contradiction. subst f0 l'0 g l0; assert (forall s', In s' l' -> Acc rpo s'). intros s' In_s'; apply IH'; trivial; apply H5; trivial. rewrite <- (projection_list_of_SN_terms l' H); apply (IH (f,(build_list_of_SN_terms l' H))); simpl; elim (F.eq_symbol_dec f f); intro eq1. rewrite H3; generalize l' H H4; clear l' H H4 H5 IH IH' lt_t_s eq1; induction l; intros l' H H4; inversion H4; clear H4. subst l' t l'0; simpl; apply List_gt_rest. unfold rpo_rest; trivial. rewrite <- (projection_list_of_SN_terms l0 (fun (t : term) (H0 : In t l0) => H t (or_intror (s = t) H0))) in H6; do 2 rewrite length_map in H6; trivial. subst l' s l'0; simpl; apply List_eq_rest; trivial; apply IHl; trivial. absurd (f=f); trivial. subst f0 l'0 g l0; assert (forall s', In s' l' -> Acc rpo s'). intros s' In_s'; apply IH'; trivial; apply (rpo_subterm _ _ lt_t_s); simpl; trivial. rewrite <- (projection_list_of_SN_terms l' H); apply (IH (f,(build_list_of_SN_terms l' H))); simpl; elim (F.eq_symbol_dec f f); intro eq1. rewrite H2; inversion H4; subst l'0 l0; assert (Acc rpo a). apply in_sn_sn with l; refine (in_permut_in a _ (list_permut_sym H1)); left; trivial. assert (forall t, In t lg -> Acc rpo t). intros; apply in_sn_sn with l; refine (in_permut_in _ _ (list_permut_sym H1)); right; apply in_or_app; left; trivial. assert (forall t, In t ls -> Acc rpo t). intros; apply H; refine (in_permut_in _ _ (list_permut_sym H0)); apply in_or_app; left; trivial. assert (forall t, In t lc -> Acc rpo t). intros; apply H; refine (in_permut_in _ _ (list_permut_sym H0)); apply in_or_app; right; trivial. apply (List_mul_rest (mk_sn a H5) (build_list_of_SN_terms lg H6) (build_list_of_SN_terms ls H7) (build_list_of_SN_terms lc H8)). rewrite map_app; do 3 rewrite projection_list_of_SN_terms; trivial. simpl; rewrite map_app; do 2 rewrite projection_list_of_SN_terms; trivial. intros b In_b; destruct b; elim (H3 tt0). intros x H'; elim H'; clear H'; intros In_x H'; elim In_x; clear In_x; intro In_x. subst x; exists (mk_sn a H5); intuition. assert (exists a', In a' (build_list_of_SN_terms lg H6) /\ tt a' = x). generalize lg H6 In_x; clear lg H1 H3 H6 In_x; induction lg. contradiction. intros H6 In_x; elim In_x; clear In_x; intro In_x; simpl. subst a0; econstructor; intuition. elim (IHlg (fun (t : term) (H1 : In t lg) => H6 t (or_intror (a0 = t) H1)) In_x); intros a' H''; elim H''; clear H''; intros In_a' H''. exists a'; split; trivial; right; trivial. elim H9; clear H9; intros a' H9; elim H9; clear H9; intros In_a' H9; exists a'; split; [ right | unfold rpo_rest; simpl; rewrite H9 ]; trivial. clear H0 H3; induction ls. contradiction. elim In_b; clear In_b; intro In_b; [ left; injection In_b; trivial | right; refine (IHls _ In_b)]. absurd (f=f); trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term