proposition: Lemma rpo_subst : forall bb s t, rpo bb s t -> forall sigma, rpo bb (apply_subst sigma s) (apply_subst sigma t).
proof: Proof. intro bb. cut (forall p, match p with (s,t) => rpo bb s t -> forall sigma, rpo bb (apply_subst sigma s) (apply_subst sigma t) end). intros H s t s_lt_t sigma; apply (H (s,t)); trivial. intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s t] IH s_lt_t sigma. inversion s_lt_t as [ f l s' t' t'_mem_l R' | f g l l' R' R'' | f g l l' f_lex g_lex f_eq_g L Rlex R' H2 H3 | f g l l' f_mul g_mul f_eq_g Rmul R' H2 ]; subst. simpl; apply Subterm with (apply_subst sigma t'). destruct (mem_split_set _ _ equiv_bool_ok _ _ t'_mem_l) as [t'' [l1 [l2 [t'_eq_t'' [H _]]]]]; simpl in t'_eq_t''; simpl in H; subst l. rewrite map_app; rewrite <- mem_or_app. right; left; apply equiv_subst; trivial. inversion R' as [ s' R'' | s' t'' R'' ]; subst. apply Equiv; apply equiv_subst; trivial. apply Lt; apply (IH (s,t')); trivial. apply size2_lex2_mem; trivial. simpl; apply Top_gt; trivial. intros s' s'_mem_l'_sigma; destruct (mem_split_set _ _ equiv_bool_ok _ _ s'_mem_l'_sigma) as [s'' [l1 [l2 [s'_eq_s'' [H _]]]]]; simpl in s'_eq_s''; simpl in H. rewrite (equiv_rpo_equiv_2 _ s'_eq_s''). assert (s''_in_l'_sigma : In s'' (map (apply_subst sigma) l')). rewrite H; apply in_or_app; right; left; trivial. rewrite in_map_iff in s''_in_l'_sigma. destruct s''_in_l'_sigma as [u [s_eq_u_sigma u_in_l']]. subst s''; replace (Term f (map (apply_subst sigma) l)) with (apply_subst sigma (Term f l)); trivial. apply (IH (u, Term f l)). apply size2_lex1; trivial. apply rpo_trans with (Term g l'); trivial. apply Subterm with u. apply in_impl_mem; trivial. exact Eq. apply Equiv; apply Eq. simpl; apply Top_eq_lex; trivial. do 2 rewrite length_map; assumption. generalize l Rlex IH; clear l s_lt_t Rlex R' IH L; induction l' as [ | s' l' ]; intros l Rlex IH; inversion Rlex as [s'' t' k k' s'_lt_t' L | s'' t' k k' s'_eq_t' k_lt_k' | ]; subst; simpl. apply List_nil. apply List_gt. apply (IH (s',t')); trivial. apply size2_lex1; left; trivial. apply List_eq. apply equiv_subst; trivial. apply IHl'; trivial. intros [s t] S s_lt_t tau; apply (IH (s,t)); trivial. apply o_size2_trans with (Term f l', Term f k'); trivial. apply size2_lex1_bis. intros s' s'_mem_l'_sigma; destruct (mem_split_set _ _ equiv_bool_ok _ _ s'_mem_l'_sigma) as [s'' [l1 [l2 [s'_eq_s'' [H _]]]]]; simpl in s'_eq_s''; simpl in H. rewrite (equiv_rpo_equiv_2 _ s'_eq_s''). assert (s''_in_l'_sigma : In s'' (map (apply_subst sigma) l')). rewrite H; apply in_or_app; right; left; trivial. rewrite in_map_iff in s''_in_l'_sigma. destruct s''_in_l'_sigma as [u [s_eq_u_sigma u_in_l']]. subst s''; replace (Term f (map (apply_subst sigma) l)) with (apply_subst sigma (Term f l)); trivial. apply (IH (u, Term g l)). apply size2_lex1; trivial. apply rpo_trans with (Term f l'); trivial. apply Subterm with u. apply in_impl_mem; trivial. exact Eq. apply Equiv; apply Eq. simpl; apply Top_eq_mul; trivial; inversion Rmul as [ a lg ls lc l0 k0 Pk Pl ls_lt_alg]; subst. apply (@List_mul bb (apply_subst sigma a) (map (apply_subst sigma) lg) (map (apply_subst sigma) ls) (map (apply_subst sigma) lc)). rewrite <- map_app; apply permut_map with equiv; trivial. intros b b' _ _ b_eq_b'; apply equiv_subst; trivial. rewrite <- map_app. refine (@permut_map term term term term equiv equiv (apply_subst sigma) _ _ (a :: lg ++ lc) _ _); trivial. intros b b' b_in_l _ b_eq_b'; apply equiv_subst; trivial. intros b b_mem_ls_sigma; destruct (mem_split_set _ _ equiv_bool_ok _ _ b_mem_ls_sigma) as [b' [ls1 [ls2 [b_eq_b' [H _]]]]]; simpl in b_eq_b'; simpl in H. assert (b'_in_ls_sigma : In b' (map (apply_subst sigma) ls)). rewrite H; apply in_or_app; right; left; trivial. rewrite in_map_iff in b'_in_ls_sigma. destruct b'_in_ls_sigma as [b'' [b''_sigma_eq_b' b''_in_ls]]. destruct (ls_lt_alg b'') as [a' [a'_mem_alg b''_lt_a']]. apply in_impl_mem; trivial. exact Eq. destruct (mem_split_set _ _ equiv_bool_ok _ _ a'_mem_alg) as [a'' [alg' [alg'' [a'_eq_a'' [H' _]]]]]; simpl in a'_eq_a''; simpl in H'. exists (apply_subst sigma a''); split; trivial. apply in_impl_mem. exact Eq. rewrite (in_map_iff (apply_subst sigma) (a :: lg)). exists a''; split; trivial. rewrite H'; apply in_or_app; right; left; trivial. rewrite (equiv_rpo_equiv_2 _ b_eq_b'). subst b'; apply (IH (b'',a'')). apply size2_lex1_mem. rewrite Pk; rewrite <- mem_or_app; left; apply in_impl_mem; trivial. exact Eq. rewrite <- (equiv_rpo_equiv_1 _ a'_eq_a''); 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)