proposition: Lemma wf_rpo_lex_rest : forall bb bb', well_founded (rpo_lex_rest bb bb').
proof: Proof. intro bb; unfold well_founded; induction bb. intros bb' l; revert bb'; pattern l; apply list_rec2; clear l. induction n as [ | n]; intros [ | a l] L bb'. apply Acc_intro; intros k H; inversion H as [k' k'' L' Acc_k Acc_k' H' H1 H2]; clear H; subst; inversion H'. inversion L. apply Acc_intro; intros k H; inversion H as [k' k'' L' Acc_k Acc_k' H' H1 H2]; clear H; subst; inversion H'. apply Acc_intro; intros k H; inversion H as [k' k'' L' Acc_k Acc_k' H' H1 H2]; subst. assert (Acc_a : Acc (rpo bb') a). apply Acc_k; left; apply Eq. assert (Acc_l' : forall s : term, mem equiv s l -> Acc (rpo bb') s). intros; apply Acc_k; right; assumption. apply Acc_inv with (a :: l); [idtac | assumption]. clear k H L' Acc_k' H'. clear -IHn Acc_a L Acc_l'. simpl in L; generalize (le_S_n _ _ L); clear L; intro L. revert l L Acc_l'; induction Acc_a as [a Acc_a IHa]; intros l L Acc_l. assert (Acc_l' := IHn _ L bb'). induction Acc_l' as [l Acc_l' IHl]. apply Acc_intro; intros l' H; inversion H as [ k k' L' Acc_al Acc_l'' H' H1 H2]; clear H; subst. destruct L' as [L' | [L1 L2]]; [idtac | inversion L2]. inversion H' as [u s' k' k'' u_lt_s | s' s'' k' k'' s'_eq_s k'_lt_l H1 H2 | u k']; clear H'; subst. apply IHa; trivial. injection L'; clear L'; intro L'; rewrite <- L'; assumption. intros; apply Acc_l''; right; assumption. apply Acc_intro. intros k'' H'; apply Acc_inv with (a :: k'). apply IHl. constructor; trivial. left; injection L'; intro; assumption. intros; apply Acc_l''; right; assumption. injection L'; clear L'; intro L'; rewrite <- L'; assumption. intros; apply Acc_l''; right; assumption. inversion H' as [k1 k1' L'' Acc_l1 Acc_l1' H1' H1 H2]; subst. constructor; trivial. simpl; intros s [s_eq_a | s_in_k']; [idtac | apply Acc_l1; right; assumption]. apply Acc_intro; intros; apply Acc_inv with a. apply Acc_intro; apply Acc_a; trivial. rewrite <- (equiv_rpo_equiv_1 _ s_eq_a); trivial. inversion H1' as [u s'' k1' k1'' u_lt_s | s1' s'' k1' k1'' s'_eq_s1 k'_lt_l1 H1 H2 | u k1']; clear H1'; subst. constructor 1; trivial. rewrite <- (equiv_rpo_equiv_1 _ s'_eq_s); trivial. constructor 2; trivial. transitivity s'; trivial. constructor 3. apply Acc_intro; intros l' H; inversion H as [ k k' L'' Acc_l1 Acc_l1' H' H1 H2]; clear H; subst. inversion H'. intros bb' l. apply Acc_intro; intros k H; inversion H as [k' k'' L' Acc_k Acc_k' H' H1 H2]; subst. destruct l as [ | a l]. inversion H'. apply Acc_inv with (a :: l); [idtac | assumption]. clear -IHbb Acc_k. assert (Acc_a : Acc (rpo bb') a). apply Acc_k; left; apply Eq. assert (Acc_l : forall s : term, mem equiv s l -> Acc (rpo bb') s). intros; apply Acc_k; right; assumption. revert Acc_l; clear Acc_k. revert l; induction Acc_a as [a Acc_a IHa]; intros l. pattern l; apply (well_founded_ind (IHbb bb')); clear l; intros l IHl Acc_l. apply Acc_intro; intros l' H; inversion H as [ k k' L Acc_al Acc_l' H' H1 H2]; clear H; subst. inversion H' as [u s' k' k'' u_lt_s | s' s'' k' k'' s'_eq_s k'_lt_l H1 H2 | u k']; clear H'; subst. apply IHa; trivial. intros; apply Acc_l'; right; assumption. apply Acc_intro. intros k'' H'; apply Acc_inv with (a :: k'). apply IHl; constructor. destruct L as [L | [L1 L2]]. left; injection L; intro; assumption. right; split; apply le_S_n; assumption. intros; apply Acc_al; right; assumption. intros; apply Acc_l'; right; assumption. assumption. apply Acc_inv; apply Acc_l'; right; assumption. inversion H' as [ k1 k1' L' Acc_l1 Acc_l1' H1' H1 H2]; subst. constructor; trivial. simpl; intros s [s_eq_a | s_in_k']; [idtac | apply Acc_l1; right; assumption]. apply Acc_intro; intros; apply Acc_inv with a. apply Acc_intro; apply Acc_a; trivial. rewrite <- (equiv_rpo_equiv_1 _ s_eq_a); trivial. inversion H1' as [u s'' k1' k1'' u_lt_s | s1' s'' k1' k1'' s'_eq_s1 k'_lt_l1 H1 H2 | u k1']; clear H1'; subst. constructor 1; trivial. rewrite <- (equiv_rpo_equiv_1 _ s'_eq_s); trivial. constructor 2; trivial. transitivity s'; trivial. constructor 3. apply Acc_intro; intros l' H; inversion H as [ k k' L' Acc_l1 Acc_l1' H' H1 H2]; clear H; subst. inversion H'. 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)