proposition: Lemma wf_rpo_mul_rest : forall bb, well_founded (rpo_mul_rest bb).
proof: Proof. intro bb; apply wf_incl with (clos_trans _ (rpo_mul_step_rest bb)). unfold inclusion; apply rpo_mul_rest_trans_clos. apply wf_clos_trans. unfold well_founded; intro l; induction l as [ | s l]. apply Acc_intro; intros m H; inversion H as [l l' Acc_l Acc_l' H']; subst; inversion H' as [a ls lc l l' P P']; subst. assert (L := permut_length P'); discriminate. assert (Acc (rpo bb) s -> Acc (rpo_mul_step_rest bb) (s :: l)). intro Acc_s; generalize l IHl; clear l IHl; pattern s; apply Acc_ind with term (rpo bb); trivial; clear s Acc_s. intros s Acc_s IHs l Acc_l; pattern l; apply Acc_ind with (list term) (rpo_mul_step_rest bb); trivial; clear l Acc_l. intros l Acc_l IHl; apply Acc_intro. intros l' H; inversion H as [s_k k' Acc_s_l Acc_l' H']; subst. destruct (@two_cases_rpo bb s l l' H') as [[s' [n' [s_eq_s' [P H'']]]] | [ls [ls_lt_s P]]]. apply (@list_permut_map_acc bb (s :: n')). rewrite P; rewrite <- permut0_cons; reflexivity || apply equiv_equiv || auto. symmetry;assumption. apply Acc_intro; intros l'' l''_lt_s'_n; apply Acc_inv with (s :: n'). apply IHl; apply Rpo_mul_step_rest; trivial. intros; apply Acc_s_l; right; trivial. intros s'' s''_in_n'; apply Acc_l'; rewrite (mem_permut0_mem equiv_equiv s'' P); right; trivial. trivial. apply (@list_permut_map_acc bb (ls ++ l)). apply permut0_sym; trivial. apply equiv_equiv. clear P; induction ls as [ | b ls]. simpl; apply Acc_intro; trivial. simpl; apply IHs. apply ls_lt_s; left; reflexivity. apply IHls; intros; apply ls_lt_s; right; trivial. apply Acc_intro. intros l' H'. apply Acc_inv with (s :: l); trivial. inversion H' as [k k' Acc_s_l Acc_l']; subst; apply H; apply Acc_s_l; left; reflexivity. 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)