proposition: Lemma rpo_mul_trans_clos : inclusion _ rpo_mul_rest (clos_trans _ rpo_mul_rest_step).
proof: Proof. unfold inclusion; intros l' l H; inversion H; clear H; subst l0 l'0; generalize l' l a ls lc H0 H1 H2; clear l' l a ls lc H0 H1 H2; induction lg. intros l' l a ls lc H0 H1 H2; apply t_step; apply (List_mul_rest_step a ls lc); trivial; intros b In_b; elim (H2 b In_b); intros a' H'; elim H'; clear H'; intros In_a' lt_b; elim In_a'; clear In_a'; intro In_a'; [subst a'; trivial | contradiction ]. intros l' l a0 ls lc H0 H1 H2. assert (exists ls1, exists ls2, list_permut (map tt ls) (map tt (ls1 ++ ls2)) /\ (forall b, In b ls1 -> rpo_rest b a0) /\ (forall b, In b ls2 -> exists a', In a' ( a:: lg) /\ rpo_rest b a')). clear H0; induction ls. exists (nil : list SN_term); exists (nil : list SN_term); intuition. contradiction. contradiction. elim IHls. intros ls1 H; elim H; clear H; intros ls2 H; elim (H2 a1 (or_introl _ (refl_equal _))); intros a' H'; elim H'; clear H'; intros In_a' H'; elim In_a'; clear In_a'; intro In_a'. subst a'; exists (a1 :: ls1); exists ls2; intuition. rewrite <- app_comm_cons; simpl; apply context_list_permut_cons; trivial. elim H3; clear H3; intro H3. subst b; trivial. apply H; trivial. exists ls1; exists (a1 :: ls2); intuition. rewrite map_app; simpl; apply (list_permut_add_cons_inside); rewrite <- map_app; trivial. elim H3; clear H3; intro H3. subst b; exists a'; intuition. apply H4; trivial. intros; apply H2; trivial; right; trivial. elim H; clear H; intros ls1 H; elim H; clear H; intros ls2 H; apply t_trans with (a0 :: ls2 ++ lc). apply t_step; apply (List_mul_rest_step a0 ls1 (ls2 ++ lc)). apply list_permut_trans with (map tt (ls ++ lc)); trivial. rewrite app_assoc; do 2 rewrite map_app; apply context_list_permut_app2; intuition. apply list_permut_refl. intuition. apply (IHlg (a0 :: ls2 ++ lc) l a ls2 (a0 :: lc)). rewrite map_app; simpl; apply list_permut_add_cons_inside; rewrite map_app; apply list_permut_refl. apply list_permut_trans with (map tt (a0 :: (a :: lg) ++ lc)); trivial. do 2 rewrite app_comm_cons; generalize (a :: lg); intro l0. do 2 rewrite map_app; simpl; apply list_permut_add_cons_inside; apply list_permut_refl. intuition. Qed.
imports: Coq(List Relations Wellfounded Arith Wf_nat Lia) hydras(more_list list_permut dickson term)