proposition: Lemma rpo_mul_trans : forall bb u t s, rpo_mul bb u t -> rpo_mul bb t s -> rpo_mul bb u s.
proof: Proof. intros. destruct H0 as [a lg ls lc l l' P' P ls_lt_alg]. destruct H 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 bb0 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 rpo_trans with (a''). trivial. 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)