proposition: Lemma rpo_mul_remove_equiv_aux : forall bb l l' s s', (forall t, mem equiv t (s :: l) -> rpo bb t t -> False) -> equiv s s' -> rpo_mul bb (s :: l) (s' :: l') -> rpo_mul bb l l'.
proof: Proof. intros bb l l' s s' Antirefl s_eq_s' sl_lt_s'l'; inversion sl_lt_s'l' as [a lg ls lc k' k P P' ls_lt_alg]; subst. assert (s_mem_ls_lc : mem equiv s (ls ++ lc)). rewrite <- (mem_permut0_mem equiv_equiv s P); left; reflexivity. rewrite <- mem_or_app in s_mem_ls_lc. destruct s_mem_ls_lc as [s_mem_ls | s_mem_lc]. assert (s'_mem_alg_lc : mem equiv s' (a :: lg ++ lc)). rewrite <- (mem_permut0_mem equiv_equiv s' P'); left; reflexivity. rewrite app_comm_cons in s'_mem_alg_lc. rewrite <- mem_or_app in s'_mem_alg_lc. destruct s'_mem_alg_lc as [s'_mem_alg | s'_mem_lc]. destruct lg as [ | g lg]. assert (s'_eq_a : equiv s' a). destruct s'_mem_alg; trivial; contradiction. destruct (ls_lt_alg _ s_mem_ls) as [a' [[a_eq_a' | a'_mem_nil] b_lt_a']]. apply False_rect. apply (Antirefl s). left; reflexivity. rewrite (equiv_rpo_equiv_1 _ s_eq_s'). rewrite (equiv_rpo_equiv_1 _ s'_eq_a). rewrite <- (equiv_rpo_equiv_1 _ a_eq_a'); trivial. contradiction. destruct (mem_split_set _ _ equiv_bool_ok _ _ s'_mem_alg) as [u' [alg' [alg'' [s'_eq_u' [H _]]]]]; simpl in s'_eq_u'; simpl in H; subst. assert (P'' : permut0 equiv l' ((alg' ++ alg'') ++ lc)). rewrite app_comm_cons in P'; rewrite H in P'. rewrite <- ass_app in P'; simpl in P'. rewrite <- ass_app; rewrite <- permut0_cons_inside in P'; trivial. apply equiv_equiv. destruct (mem_split_set _ _ equiv_bool_ok _ _ s_mem_ls) as [u [ls' [ls'' [s_eq_u [H' _]]]]]; simpl in s_eq_u; simpl in H'; subst. assert (ls'ls''_lt_alg'alg'' : forall b, mem equiv b (ls' ++ ls'') -> exists a', mem equiv a' (alg' ++ alg'') /\ rpo bb b a'). intros b b_in_ls'ls''; destruct (ls_lt_alg b) as [a' [a'_mem_aglg b_lt_a']]. apply mem_insert; trivial. rewrite H in a'_mem_aglg. rewrite <- mem_or_app in a'_mem_aglg. destruct a'_mem_aglg as [a'_mem_alg' | [u'_eq_a' | a'_mem_alg'']]. exists a'; split; trivial. rewrite <- mem_or_app; left; trivial. destruct (ls_lt_alg a') as [a'' [a''_mem_aglg a'_lt_a'']]. rewrite <- mem_or_app; right; left. transitivity u'; trivial. transitivity s; trivial. symmetry. transitivity s'; trivial. exists a''; split. apply diff_mem_remove with u'. intro a''_eq_u'. destruct (mem_split_set _ _ equiv_bool_ok u (s :: l)) as [u'' [l1 [l2 [u_eq_u'' [H' _]]]]]. left; symmetry; trivial. simpl in u_eq_u''; simpl in H'. apply (Antirefl u''). rewrite (mem_permut0_mem equiv_equiv u'' P). rewrite <- mem_or_app; left. rewrite <- mem_or_app; right; left; symmetry; trivial. assert (u''_eq_u' : equiv u'' u'). transitivity s'; trivial. transitivity s; trivial. transitivity u. symmetry; trivial. symmetry; trivial. rewrite (equiv_rpo_equiv_2 _ u''_eq_u'). rewrite <- (equiv_rpo_equiv_2 _ u'_eq_a'). rewrite (equiv_rpo_equiv_1 _ u''_eq_u'). rewrite <- (equiv_rpo_equiv_1 _ a''_eq_u'); trivial. rewrite <- H; trivial. apply rpo_trans with a'; trivial. exists a'; split; trivial. rewrite <- mem_or_app; right; trivial. assert (L : length (alg' ++ alg'') = S (length lg)). assert (L' := f_equal (fun l => length l) H). simpl in L'; rewrite length_app in L'; simpl in L'. rewrite Nat.add_comm in L'; simpl in L'; rewrite Nat.add_comm in L'. rewrite <- length_app in L'; injection L'; intro L''; symmetry; assumption. destruct (alg' ++ alg'') as [ | a' lg']. discriminate. apply (@List_mul bb a' lg' (ls' ++ ls'') lc); trivial. rewrite <- ass_app in P; simpl in P. rewrite <- permut0_cons_inside in P; trivial;[|apply equiv_equiv]. rewrite <- ass_app; trivial. destruct (mem_split_set _ _ equiv_bool_ok _ _ s'_mem_lc) as [s'' [lc' [lc'' [s_eq_s'' [H _]]]]]. simpl in s_eq_s''; simpl in H. apply (@List_mul bb a lg ls (lc' ++ lc'')); trivial. rewrite H in P. rewrite ass_app in P. rewrite <- permut0_cons_inside in P. rewrite ass_app; trivial. apply equiv_equiv. transitivity s'; trivial. rewrite H in P'. rewrite app_comm_cons in P'. rewrite ass_app in P'. rewrite <- permut0_cons_inside in P'; trivial. rewrite app_comm_cons; rewrite ass_app; trivial. apply equiv_equiv. destruct (mem_split_set _ _ equiv_bool_ok _ _ s_mem_lc) as [s'' [lc' [lc'' [s_eq_s'' [H _]]]]]. simpl in s_eq_s''; simpl in H. apply (@List_mul bb a lg ls (lc' ++ lc'')); trivial. rewrite H in P. rewrite ass_app in P. rewrite <- permut0_cons_inside in P; trivial. rewrite ass_app; trivial. apply equiv_equiv. rewrite H in P'. rewrite app_comm_cons in P'. rewrite ass_app in P'. rewrite <- permut0_cons_inside in P'. rewrite app_comm_cons; rewrite ass_app; trivial. apply equiv_equiv. transitivity s; trivial. symmetry; 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)