proposition: Lemma acc_build : well_founded (prec Prec) -> forall bb f_l, match f_l with (f, l) => (forall t, mem equiv t l -> Acc (rpo bb) t) -> Acc (rpo bb) (Term f l) end.
proof: Proof. intros wf_prec bb f_l; pattern f_l; apply (well_founded_induction_type (wf_rpo_rest wf_prec bb)); clear f_l. intros [f l] IH Acc_l; apply Acc_intro; intros s; pattern s; apply term_rec3_mem; clear s. intros v _; apply Acc_intro. intros t t_lt_v; inversion t_lt_v. intros g k IHl gk_lt_fl; inversion gk_lt_fl as [ f' l' s' t t_in_l H' | f' g' k' l' g_prec_f | f' g' k' l' Sf Sg f_eq_g L H' H'' | f' g' k' l' Sf Sg f_eq_g H']; subst. assert (Acc_t := Acc_l _ t_in_l). subst; inversion H' as [s' t' s_eq_t | s' t' s_lt_t ]; subst s' t'; [idtac | apply Acc_inv with t; trivial ]. apply Acc_intro; intro u. rewrite (@equiv_rpo_equiv_1 _ (Term g k) t); trivial; intro; apply Acc_inv with t; trivial. assert (Acc_k : forall s, mem equiv s k -> Acc (rpo bb) s). intros s s_mem_k; apply IHl; trivial. apply H; trivial. apply (IH (g,k)); trivial. apply Top_gt_rest; trivial. assert (Acc_k : forall s, mem equiv s k -> Acc (rpo bb) s). intros s s_mem_k; apply IHl; trivial. apply H''; trivial. apply (IH (g,k)); trivial. apply Top_eq_lex_rest; trivial. assert (Acc_k : forall s, mem equiv s k -> Acc (rpo bb) s). intros s s_mem_k; apply IHl; trivial. apply rpo_trans with (Term g k); trivial; apply Subterm with s; trivial; apply Equiv; apply Eq. apply (IH (g,k)); trivial. apply Top_eq_mul_rest; trivial. Qed.
imports: Coq(Bool Peano List PeanoNat) CoLoR(closure more_list equiv_list list_permut dickson) Coq(Relations Wellfounded Arith Wf_nat Recdef Program Morphisms Lia) CoLoR(term_spec term decidable_set ordered_set NatCompat)