proposition: Lemma two_cases_rpo : forall a m n, rpo_mul_rest_step n (a :: m) -> (exists n', list_permut (map tt n) (map tt (a :: n')) /\ rpo_mul_rest_step n' m) \/ (exists k, (forall b, In b k -> rpo_rest b a) /\ list_permut (map tt n) (map tt (k ++ m))).
proof: Proof. intros a m n M; inversion_clear M; destruct a; destruct a0; elim (eq_term_dec tt0 tt1). intro; subst tt1; right; exists ls; intuition; apply list_permut_trans with (map tt (ls ++ lc)); trivial; do 2 rewrite map_app; apply context_list_permut_app1; apply remove_context_list_permut_cons with tt0; apply list_permut_sym; trivial. intro a_diff_a0; left; elim (In_dec eq_term_dec tt1 (map tt m)); intro In_a0. generalize (split_list_app_cons eq_term_dec _ _ In_a0); clear In_a0; destruct (split_list eq_term_dec (map tt m) tt1). intro; assert (forall s, In s l -> Acc rpo s). intros s In_s; apply in_sn_sn with m; rewrite H2; apply in_or_app; left; trivial. assert (forall s, In s l0 -> Acc rpo s). intros s In_s; apply in_sn_sn with m; rewrite H2; apply in_or_app; do 2 right; trivial. exists ((build_list_of_SN_terms l H3) ++ ls ++ (build_list_of_SN_terms l0 H4)); intuition. apply list_permut_trans with (map tt (ls ++ lc)) ; trivial; apply remove_context_list_permut_cons with tt1; apply list_permut_trans with ((map tt ls) ++ tt1 :: (map tt lc)). apply list_permut_add_cons_inside; rewrite map_app; apply list_permut_refl. apply list_permut_trans with (map tt ls ++ (tt0 :: l ++ tt1 :: l0)). apply context_list_permut_app1; apply list_permut_sym; rewrite <- H2; trivial. rewrite app_comm_cons; rewrite <- app_ass; apply list_permut_sym; apply list_permut_add_cons_inside; rewrite app_ass; rewrite <- app_comm_cons; simpl; apply list_permut_add_cons_inside; do 2 rewrite map_app; do 2 rewrite projection_list_of_SN_terms; do 2 rewrite <- app_ass; apply context_list_permut_app2; apply list_permut_app_app. apply (List_mul_rest_step (mk_sn tt1 sn1) ls (build_list_of_SN_terms l H3 ++ build_list_of_SN_terms l0 H4)); intuition. do 2 rewrite ass_app; do 4 rewrite map_app; apply context_list_permut_app2; apply list_permut_app_app. rewrite H2; simpl; rewrite map_app; do 2 rewrite projection_list_of_SN_terms; apply list_permut_sym; apply list_permut_add_cons_inside; apply list_permut_refl. absurd (In tt1 (map tt (mk_sn tt0 sn0 :: m))). unfold not; intro H2; elim H2; clear H2; intro H2. apply a_diff_a0; trivial. apply In_a0; trivial. refine (in_permut_in tt1 _ (list_permut_sym H0)); left; trivial. Qed.
imports: List more_list list_permut dickson Relations Wellfounded Arith Wf_nat term