proposition: Lemma rpo_trans : forall bb u t s, rpo bb u t -> rpo bb t s -> rpo bb u s.
proof: Proof. intros bb u t s; cut (forall triple : term * (term * term), match triple with | (s,(t,u)) => rpo bb t s -> rpo bb u t -> rpo bb u s end). intros H u_lt_t t_lt_s; apply (H (s,(t,u))); trivial. clear s t u; intro triple; pattern triple; refine (well_founded_ind wf_size3 _ _ triple); clear triple. intros [[v | f l] [t u]] IH. intros t_lt_v; inversion t_lt_v. intros t_lt_fl u_lt_t; inversion t_lt_fl as [ f'' l' s' t' t'_in_l' t_le_t' | f'' f' k'' l' f'_prec_f H'' | f'' g'' k'' l' Sf Sg f''_eq_g'' L l'_lt_l H H1 H2 | f'' g'' k'' l' Sf Sg f''_eq_g'' l'_lt_l ]; subst. apply Subterm with t'; trivial; apply Lt; inversion t_le_t' as [t'' t''' t_eq_t' | t'' t''' t_lt_t']; subst. rewrite <- (equiv_rpo_equiv_1 _ t_eq_t'); trivial. apply (IH (t',(t,u))); trivial. apply size3_lex1_mem; trivial. inversion u_lt_t as [ f'' l'' s' t' t'_in_l' u_le_t' | g'' f'' k'' l'' f''_prec_f'' H''' | g'' g' k'' l'' Sf' Sf'' g''_eq_g' L l''_lt_l' H H1 H2 | g'' g' k'' l'' Sf' Sf'' g''_eq_g' l''_lt_l' ]; subst. inversion u_le_t' as [t'' t''' u_eq_t' | t'' t''' u_lt_t']; subst. rewrite (equiv_rpo_equiv_2 _ u_eq_t'); trivial; apply H''; trivial. apply (IH (Term f l,(t',u))); trivial. apply size3_lex2_mem; trivial. apply H''; trivial. apply Top_gt. apply prec_transitive with f'; trivial. intros u u_in_l''; apply (IH (Term f l, (Term f' l', u))); trivial. apply size3_lex3_mem; trivial. apply H'''; trivial. apply Top_gt. apply prec_eq_prec2 with f'. trivial. apply prec_eq_sym. trivial. intros u u_in_l''; apply (IH (Term f l, (Term f' l', u))); trivial. apply size3_lex3_mem; trivial. apply H; trivial. apply Top_gt. apply prec_eq_prec2 with f'. trivial. apply prec_eq_sym. trivial. intros u u_in_l''. apply (IH (Term f l, (Term f' l', u))); trivial. apply size3_lex3_mem; trivial. apply rpo_subterm_mem with g'' l''; trivial. inversion u_lt_t as [ f''' l'' s' t' t'_in_l' u_le_t' | g'' f''' k'' l'' f''_prec_f' H''' | g'' f''' k'' l'' Sf' Sg' f_eq_g' L' l''_lt_l' H' H1 H2 | g'' f''' k'' l'' Sf' Sg' f_eq_g' l''_lt_l' ]; subst. inversion u_le_t' as [t'' t''' u_eq_t' | t'' t''' u_lt_t']; subst. rewrite (equiv_rpo_equiv_2 _ u_eq_t'). apply rpo_subterm_mem with f'' l'; trivial. apply (IH (Term f l, (t', u))); trivial. apply size3_lex2_mem; trivial. apply H; trivial. apply Top_gt. apply prec_eq_prec1 with f''; trivial. intros u u_in_l''. apply (IH (Term f l, (Term f'' l', u))). apply size3_lex3_mem. trivial. trivial. apply H'''. trivial. apply Top_eq_lex; trivial. apply prec_eq_transitive with f''. trivial. trivial. destruct L as [L | [L1 L2]]. rewrite L; assumption. destruct L' as [L' | [L1' L2']]. rewrite <- L'; right; split; assumption. right; split; assumption. generalize l' l'' l'_lt_l l''_lt_l' IH; clear l' l'' l'_lt_l l''_lt_l' IH H H' t_lt_fl u_lt_t L L'; induction l as [ | s l]; intros l' l'' l'_lt_l l''_lt_l' IH. inversion l'_lt_l. inversion l'_lt_l as [ t s' k' k t_lt_s | t s' k' k t_eq_s k'_lt_k | t k]; inversion l''_lt_l' as [ u t' k'' h' u_lt_t | u t' k'' h' u_eq_t k''_lt_k' | u k1]. subst; injection H3; intros; subst; apply List_gt. apply (IH (s,(t,u))); trivial. apply size3_lex1; left; trivial. subst; injection H3; intros; subst; apply List_gt. rewrite (equiv_rpo_equiv_2 _ u_eq_t); trivial. apply List_nil. subst; injection H3; intros; subst; apply List_gt. rewrite <- (equiv_rpo_equiv_1 _ t_eq_s); trivial. subst; injection H3; intros; subst; apply List_eq. transitivity t; trivial. apply IHl with k'; trivial. intros; apply IH; apply o_size3_trans with (Term f l, (Term f k', Term f k'')); trivial. apply size3_lex1_bis. apply List_nil. subst; discriminate H3. subst; discriminate H3. subst; discriminate H3. intros u u_in_l''. apply (IH (Term f l, (Term f'' l', u))); trivial. apply size3_lex3_mem. trivial. apply H'; trivial. rewrite Sf in Sg'; discriminate. inversion u_lt_t as [ f''' l'' s' t' t'_in_l' u_le_t' | g'' f''' k'' l'' f''_prec_f' H''' | g'' f''' k'' l'' Sf' Sf''' Seq_g''_f''' L l''_lt_l' H H1 H2 | g'' f''' k'' l'' Sf' Sf''' Seq_g''_f''' l''_lt_l' ]; subst. inversion u_le_t' as [t'' t''' u_eq_t' | t'' t''' u_lt_t']; subst. rewrite (equiv_rpo_equiv_2 _ u_eq_t'). apply rpo_subterm_mem with f'' l'; trivial. apply (IH (Term f l, (t', u))); trivial. apply size3_lex2_mem; trivial. apply rpo_subterm_mem with f'' l'; trivial. apply Top_gt; trivial. apply prec_eq_prec1 with f''. trivial. trivial. intros u u_in_l''; apply (IH (Term f l, (Term f'' l', u))); trivial. apply size3_lex3_mem; trivial. apply H'''; trivial. rewrite Sf in Sf'''; discriminate. apply Top_eq_mul; trivial. apply prec_eq_transitive with f''. trivial. trivial. destruct l'_lt_l as [a lg ls lc l l' P' P ls_lt_alg]. destruct l''_lt_l' as [a' lg' ls' lc' l' l'' Q' Q ls'_lt_alg']. rewrite P' in Q; rewrite app_comm_cons in Q. destruct (@ac_syntactic _ _ equiv_equiv _ equiv_bool_ok _ _ _ _ Q) as [k1 [k2 [k3 [k4 [P1 [P2 [P3 P4]]]]]]]. apply (@List_mul bb a (lg ++ k2) (ls' ++ k3) k1). rewrite Q'. rewrite <- ass_app. rewrite <- permut_app1. rewrite list_permut0_app_app; trivial. apply equiv_equiv. apply equiv_equiv. rewrite P. rewrite <- permut0_cons;[|apply equiv_equiv|reflexivity]. rewrite <- ass_app. rewrite <- permut_app1. rewrite list_permut0_app_app; trivial. apply equiv_equiv. apply equiv_equiv. intros b b_mem_ls'_k3; rewrite <- mem_or_app in b_mem_ls'_k3. destruct b_mem_ls'_k3 as [b_mem_ls' | b_mem_k3]. destruct (ls'_lt_alg' _ b_mem_ls') as [a'' [a''_in_a'lg' b_lt_a'']]. rewrite (mem_permut0_mem equiv_equiv a'' P4) in a''_in_a'lg'. rewrite <- mem_or_app in a''_in_a'lg'. destruct a''_in_a'lg' as [a''_mem_k2 | a''_mem_k4]. exists a''; split; trivial. rewrite app_comm_cons; rewrite <- mem_or_app; right; trivial. destruct (ls_lt_alg a'') as [a3 [a3_in_alg a''_lt_a3]]. rewrite (mem_permut0_mem equiv_equiv a'' P2). rewrite <- mem_or_app; right; trivial. exists a3; split. rewrite app_comm_cons; rewrite <- mem_or_app; left; trivial. apply (IH (a3,(a'',b))); trivial. apply size3_lex1_mem. rewrite (mem_permut0_mem equiv_equiv a3 P). rewrite app_comm_cons; rewrite <- mem_or_app; left; trivial. destruct (ls_lt_alg b) as [a'' [a''_in_alg b_lt_a'']]. rewrite (mem_permut0_mem equiv_equiv b P2); rewrite <- mem_or_app; left; trivial. exists a''; split; trivial. rewrite app_comm_cons; rewrite <- mem_or_app; left; 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)