proposition: Lemma equiv_rpo_equiv_1 : forall bb t t', equiv t t' -> (forall s, rpo bb s t <-> rpo bb s t').
proof: Proof. intro bb. assert (H : forall p, match p with (s,t) => forall t', equiv t t' -> rpo bb s t -> rpo bb s t' end). intro p; pattern p; refine (well_founded_ind wf_size2 _ _ _); clear p. intros [s t] IH t' t_eq_t' s_lt_t. inversion t_eq_t' as [ t'' | f g'' l1 l2 Statf Statg eq_f_g H | f g'' l1 l2 Statf Statg eq_f_g P]; subst. trivial. inversion s_lt_t as [g l t'' t' t'_mem_l t''_le_t' | g g' l l' g_prec_f l'_lt_t | g g''' l l' Stat_g Statg''' eq_g_g''' L l'_lt_ll1 l'_lt_t | g g''' l l' Stat_g Statg''' eq_g_g''' l'_lt_ll1 ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. rewrite <- (mem_mem t' H); trivial. apply Equiv; trivial. rewrite <- (mem_mem t' H); trivial. apply Lt; trivial. apply Top_gt; trivial. apply prec_eq_prec1 with f. trivial. trivial. intros s' s'_mem_l'. apply (IH (s',(Term f l1))); trivial. apply size2_lex1_mem; trivial. apply l'_lt_t; trivial. apply Top_eq_lex; trivial. apply prec_eq_transitive with f; trivial. rewrite <- (equiv_list_lex_same_length H); assumption. clear t_eq_t' l'_lt_t s_lt_t L. revert l2 l' l'_lt_ll1 IH H. induction l1 as [ | t1 l1]; intros l2 l' l'_lt_l1 IH l1_eq_l2; inversion l'_lt_l1 as [ s t1' l'' l1' s_lt_t1' L_eq | t1' t1'' l'' l1' t1'_eq_t1'' l''_lt_l1' | s l'']; subst; inversion l1_eq_l2 as [ | t1'' t2 l1' l2' t1''_eq_t2 l1_eq_l2']; subst. simpl; apply List_gt. apply (IH (s,t1)); trivial. apply size2_lex1; left; trivial. apply List_eq. transitivity t1; trivial. apply IHl1; trivial. intros y H; apply IH. refine (o_size2_trans _ _ _ H _). apply size2_lex1_bis. apply List_nil. intros s' s'_mem_l'. apply (IH (s', Term f l1)); trivial. apply size2_lex1_mem; trivial. apply l'_lt_t; trivial. rewrite Statf in Statg'''; discriminate. inversion s_lt_t as [g l t'' t' t'_mem_l t''_le_t' | g g' l l' g_prec_f l'_lt_t | g g''' l l' Stat_g Statg''' eq_g_g''' L l'_lt_ll1 l'_lt_t | g g''' l l' Stat_g Statg''' eq_g_g''' l'_lt_ll1 ]; subst. destruct t''_le_t' as [t'' t' t''_eq_t' | t'' t' t''_lt_t']; apply Subterm with t'; trivial. rewrite <- (mem_permut0_mem equiv_equiv t' P); trivial. apply Equiv; trivial. rewrite <- (mem_permut0_mem equiv_equiv t' P); trivial. apply Lt; trivial. apply Top_gt; trivial. apply prec_eq_prec1 with f. trivial. trivial. intros s' s'_mem_l2. apply (IH (s', Term f l1)); trivial. apply size2_lex1_mem; trivial. apply l'_lt_t; trivial. rewrite Statf in Statg'''; discriminate. apply Top_eq_mul; trivial. apply prec_eq_transitive with f. trivial. trivial. inversion l'_lt_ll1 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 equiv_equiv) with l1. apply (permut0_sym equiv_equiv). trivial. exact Q2. 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)