proposition: Lemma rpo_mul_rest_trans_clos : forall bb, inclusion _ (rpo_mul_rest bb) (clos_trans _ (rpo_mul_step_rest bb)).
proof: Proof. intro bb; unfold inclusion; intros l' l H; inversion H as [k k' Acc_l Acc_l' H' H1 H2 ]; subst. inversion H' as [a lg ls lc k k' P' P ls_lt_alg]; subst. generalize l' l a ls lc P' P ls_lt_alg Acc_l Acc_l'; clear l' l a ls lc P' P ls_lt_alg H Acc_l Acc_l' H'; induction lg as [ | g lg]; intros l' l a ls lc P' P ls_lt_alg Acc_l Acc_l'. apply t_step; apply Rpo_mul_step_rest; trivial; apply (@List_mul_step bb a ls lc); trivial. intros b b_in_ls; destruct (ls_lt_alg b b_in_ls) as [a' [[a'_eq_a | a'_in_nil] b_lt_a']]. rewrite <- (equiv_rpo_equiv_1 _ a'_eq_a); trivial. contradiction. assert (H: exists ls1, exists ls2, permut0 equiv ls (ls1 ++ ls2) /\ (forall b, mem equiv b ls1 -> rpo bb b g) /\ (forall b, mem equiv b ls2 -> exists a', mem equiv a' (a :: lg) /\ rpo bb b a')). clear P'; induction ls as [ | s ls]. exists (nil : list term); exists (nil : list term); intuition. reflexivity. destruct IHls as [ls1 [ls2 [P' [ls1_lt_g ls2_lt_alg]]]]. intros b b_in_ls; apply ls_lt_alg; right; trivial. destruct (ls_lt_alg s) as [a' [[a'_eq_a | [a'_eq_g | a'_in_lg]] b_lt_a']]. left; reflexivity. exists ls1; exists (s :: ls2); repeat split; trivial. rewrite <- permut0_cons_inside; trivial. apply equiv_equiv. reflexivity. intros b [b_eq_s | b_in_ls2]. exists a; split. left; reflexivity. rewrite (equiv_rpo_equiv_2 _ b_eq_s). rewrite <- (equiv_rpo_equiv_1 _ a'_eq_a); trivial. apply ls2_lt_alg; trivial. exists (s :: ls1); exists ls2; repeat split; trivial. simpl; rewrite <- permut0_cons; trivial. apply equiv_equiv. reflexivity. intros b [b_eq_s | b_in_ls1]. rewrite (equiv_rpo_equiv_2 _ b_eq_s). rewrite <- (equiv_rpo_equiv_1 _ a'_eq_g); trivial. apply ls1_lt_g; trivial. exists ls1; exists (s :: ls2); repeat split; trivial. rewrite <- permut0_cons_inside; trivial. apply equiv_equiv. reflexivity. intros b [b_eq_s | b_in_ls2]. exists a'; split. right; trivial. rewrite (equiv_rpo_equiv_2 _ b_eq_s); trivial. apply ls2_lt_alg; trivial. destruct H as [ls1 [ls2 [Pls [ls1_lt_g ls2_lt_alg]]]]. apply t_trans with (g :: ls2 ++ lc). apply t_step; apply Rpo_mul_step_rest; trivial. simpl; intros s [g_eq_s | s_mem_ls2lc]. apply Acc_l. rewrite P; right; left; trivial. apply Acc_l'. rewrite P'; rewrite <- mem_or_app. rewrite <- mem_or_app in s_mem_ls2lc. destruct s_mem_ls2lc as [s_mem_ls2 | s_mem_lc]. left; rewrite Pls; rewrite <- mem_or_app; right; trivial. right; trivial. apply (@List_mul_step bb g ls1 (ls2 ++ lc)); reflexivity || auto. rewrite P'; rewrite Pls; rewrite ass_app; reflexivity || auto. apply (IHlg (g :: ls2 ++ lc) l a ls2 (g :: lc)); trivial. rewrite <- permut0_cons_inside; try reflexivity. apply equiv_equiv. rewrite P. rewrite <- permut0_cons;[|apply equiv_equiv|reflexivity]. simpl; rewrite <- permut0_cons_inside;[reflexivity|apply equiv_equiv|reflexivity]. simpl; intros s [g_eq_s | s_mem_ls2lc]. apply Acc_l. rewrite P; right; left; trivial. apply Acc_l'. rewrite P'; rewrite <- mem_or_app. rewrite <- mem_or_app in s_mem_ls2lc. destruct s_mem_ls2lc as [s_mem_ls2 | s_mem_lc]. left; rewrite Pls; rewrite <- mem_or_app; right; trivial. right; 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)