proposition: Lemma equiv_rpo_equiv_2 : forall bb t t', equiv t t' -> (forall s, rpo bb t s <-> rpo bb t' s).
proof: Proof. intro bb. assert (H : forall p, match p with (s,t) => forall t', equiv t t' -> rpo bb t s -> rpo bb t' s end). intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s t] IH t' t_eq_t' t_lt_s. inversion t_eq_t' as [ t'' | g g' l1 l2 Stat Statg' g_eq_g' l1_eq_l2 | g g' l1 l2 Stat Statg' g_eq_g' P]; subst. trivial. inversion t_lt_s as [f l t'' t' t'_mem_l t''_le_t' | f f' l l' g_prec_f l'_lt_s | f' f l l' Stat_g Stat' f_stat_g L ll1_lt_l ll_lt_s | f' f l l' Stat_g Stat' f_stat_g ll1_lt_l ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. apply Equiv. transitivity t''; trivial. symmetry; trivial. apply Lt. apply (IH (t',t'')); trivial. apply size2_lex1_mem; trivial. apply Top_gt; trivial. apply prec_eq_prec2 with g; trivial. intros s' s'_mem_l2. apply l'_lt_s. rewrite (@mem_mem s' l1 l2); trivial. apply Top_eq_lex; trivial. apply prec_eq_transitive with g. apply prec_eq_sym. trivial. trivial. rewrite <- (equiv_list_lex_same_length l1_eq_l2); assumption. clear t_eq_t' ll_lt_s t_lt_s L; revert l2 l l1_eq_l2 ll1_lt_l IH. induction l1 as [ | t1 l1]; intros l2 l l1_eq_l2 l1_lt_l IH; inversion l1_lt_l as [ t1' s l1' l' t1'_lt_s L_eq | t1' s l1' l'' t1'_eq_s l1'_lt_l'' | s l']; subst; inversion l1_eq_l2 as [ | t1'' t2 l1' l2' t1''_eq_t2 l1_eq_l2']; subst. apply List_nil. simpl; apply List_gt. apply (IH (s,t1)); trivial. apply size2_lex1; left; trivial. simpl; apply List_eq. transitivity t1; trivial. symmetry; trivial. apply IHl1; trivial. intros y H; apply IH. refine (o_size2_trans _ _ _ H _). apply size2_lex1_bis. intros s' s'_in_l2; apply ll_lt_s. rewrite (@mem_mem s' l1 l2); trivial. rewrite Stat in Stat_g; discriminate. inversion t_lt_s as [f l t'' t' t'_mem_l t''_le_t' | f f' l l' g_prec_f l'_lt_s | f' f l l' Stat_g Stat' f_stat_g L ll1_lt_l ll_lt_s | f' f l l' Stat_g Stat' f_stat_g ll1_lt_l ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. apply Equiv. transitivity t''; trivial. symmetry; trivial. apply Lt. apply (IH (t',t'')); trivial. apply size2_lex1_mem; trivial. apply Top_gt; trivial. apply prec_eq_prec2 with g; trivial. intros s' s'_mem_l2; apply l'_lt_s. rewrite (mem_permut0_mem equiv_equiv s' P); trivial. rewrite Stat in Stat_g; discriminate. apply Top_eq_mul; trivial. apply prec_eq_transitive with g. apply prec_eq_sym; trivial. trivial. inversion ll1_lt_l as [a lg ls lc l' l'' Q1 Q2 ls_lt_alg]; subst. apply (@List_mul bb a lg ls lc); trivial. apply permut0_trans with l1. exact equiv_equiv. apply (permut0_sym equiv_equiv). assumption. assumption. intros t t' t_eq_t' s; split. apply (H (s,t)); trivial. apply (H (s,t')); trivial. symmetry; assumption. 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)