proposition: Lemma two_cases_rpo : forall bb a m n, rpo_mul_step bb n (a :: m) -> (exists a', exists n', equiv a a' /\ permut0 equiv n (a' :: n') /\ rpo_mul_step bb n' m) \/ (exists ls, (forall b, mem equiv b ls -> rpo bb b a) /\ permut0 equiv n (ls ++ m)).
proof: Proof. intros bb b m n M; inversion M as [a ls lc l l' P' P ls_lt_a]; subst. assert (b_mem_a_lc : mem equiv b (a :: lc)). rewrite <- (mem_permut0_mem equiv_equiv b P); left; reflexivity. simpl in b_mem_a_lc; destruct b_mem_a_lc as [b_eq_a | b_mem_lc]. right; exists ls; repeat split; trivial. intros c c_mem_ls; rewrite (equiv_rpo_equiv_1 _ b_eq_a). apply ls_lt_a; trivial. rewrite P'; rewrite <- permut_app1. rewrite <- permut0_cons in P; try (symmetry; trivial). apply equiv_equiv. symmetry;trivial. apply equiv_equiv. destruct (mem_split_set _ _ equiv_bool_ok _ _ b_mem_lc) as [b' [lc1 [lc2 [b_eq_b' [H _]]]]]; simpl in b_eq_b'; simpl in H. left; exists b'; exists (ls ++ (lc1 ++ lc2)); repeat split; trivial. rewrite P'; subst lc. rewrite ass_app; apply permut0_sym. apply equiv_equiv. rewrite <- permut0_cons_inside;[|apply equiv_equiv|reflexivity]. rewrite ass_app; reflexivity. apply (@List_mul_step bb a ls (lc1 ++ lc2)); try reflexivity. rewrite app_comm_cons. rewrite (@permut0_cons_inside _ _ equiv_equiv _ _ m (a :: lc1) lc2 b_eq_b'). rewrite P. simpl; subst lc; reflexivity. auto. 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)