proposition: Lemma wf_rpo_rest : well_founded (prec Prec) -> forall bb, well_founded (rpo_rest bb).
proof: Proof. intros wf_prec bb; unfold well_founded; intros [f l]; generalize l; clear l; pattern f; apply (well_founded_induction_type wf_prec); clear f. intros f IHf l; assert (Sf : forall f', f' = f -> status Prec f' = status Prec f). intros; subst; trivial. destruct (status Prec f); generalize (Sf _ (eq_refl _)); clear Sf; intro Sf. pattern l; apply (well_founded_induction_type (wf_rpo_lex_rest bb bb)); clear l. intros l IHl; apply Acc_intro; intros [g l'] H. inversion H as [ f' g' k k' g_prec_f Acc_l Acc_l' | f' g' k k' Sf' Sg' eq_f'_g' L H' Acc_l Acc_l' | f' g' k k' Sf' Sg' eq_f'_g' H' Acc_l Acc_l' ]; subst. apply IHf; trivial. apply rpo_rest_prec_eq with f. apply prec_eq_sym; trivial. apply rpo_rest_prec_eq with f. apply prec_eq_refl. apply IHl; apply Rpo_lex_rest; trivial. rewrite Sf in Sg'; discriminate. pattern l; apply (well_founded_induction_type (wf_rpo_mul_rest bb)); clear l. intros l IHl; apply Acc_intro; intros [g l'] H; inversion H as [ f' g' k k' g_prec_f Acc_l Acc_l' | f' k k' Sf' L H' Acc_l Acc_l' | f' k k' Sf' H' Acc_l Acc_l' ]; subst. apply IHf; trivial. absurd (Lex = Mul); [discriminate | apply trans_eq with (status Prec f); auto]. apply rpo_rest_prec_eq with f. apply prec_eq_sym; trivial. apply IHl; apply Rpo_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)