proposition: Lemma WF_cycles : WF (chain R).
proof: Proof. set (n := length DP). apply WF_iter with (S n). intro. assert (Hwf' : WF (succ @ succ_eq#)). apply absorb_WF_modulo_r; hyp. gen (Hwf' x). induction 1. apply SN_intro; intros. apply H0. ded (iter_chain_chain_dps H1). do 3 destruct H2. assert (length x1 > 0). lia. ded (last_intro H4). do 3 destruct H5. clear H4. rewrite H5 in H3. ded (chain_dps_path_dp_graph H3). set (l' := x0 :: x2 ++ x3 :: nil). assert (exists z, occur z l' >= 2). unfold l'. eapply long_path_occur. apply restricted_dp_graph. apply H4. rewrite H6, H2. unfold n. lia. assert (exists l, exists a, exists m, l' = l ++ a :: m /\ succ (lhs a) (rhs a)). destruct H7. set (p := occur x4 l' - 2). assert (occur x4 l' = S (S p)). unfold p. lia. ded (occur_S eq_dec H8). do 3 destruct H9. destruct H10. clear H8. rewrite H9. ded (occur_S eq_dec H11). do 3 destruct H8. destruct H12. clear H11. clear H13. clear p. rewrite H8. rewrite H8 in H9. clear H8. clear H10. assert (cycle dp_graph x4 x7). unfold cycle. eapply sub_path. unfold l' in H9. apply H9. exact H4. ded (cycle_min_intro eq_dec H8). decomp H10. assert (length l' = n+2). unfold l'. simpl. rewrite <- H5. lia. rewrite H9 in H10. change (length (x5++(x4::x7)++x4::x8) = n+2) in H10. rewrite H11 in H10. repeat (rewrite length_app in H10; simpl in H10). unfold n in H10. assert (h : length x11 < length DP). unfold cycle_min in H14. destruct H14. assert (length (x10::x11) <= length DP). apply nodup_incl_length. apply eq_dec. exact H14. apply incl_appr_incl with (x10::nil). simpl. eapply restricted_path_incl. apply restricted_dp_graph. exact H13. simpl in H15. lia. clear H10. ded (Hcycle h H14). do 2 destruct H10. ded (in_elim H10). do 2 destruct H15. exists (x5++x9++x14). exists x13. exists (x15++x12++x4::x8). intuition. rewrite !app_ass. trans (x5++(x4::x7)++x4::x8). refl. rewrite H11, app_ass. trans (x5++x9++(x10::x11)++x12++x4::x8). simpl. rewrite app_ass. refl. rewrite H15, app_ass. refl. do 4 destruct H8. unfold l' in H8. ded (chain_dps_app' H8 H3). do 2 destruct H10. assert (succ_eq# x x7). destruct H10. subst x7. intuition. eapply incl_elim. eapply compat_chain_dps. apply H10. assert ((succ @ succ_eq#) x7 y). destruct x6; simpl in H11. ded (compat_chain_dp_strict H9 H11). exists y. intuition. do 2 destruct H11. exists x8. split. eapply incl_elim. apply (compat_chain_dp_strict H9). exact H11. eapply incl_elim. eapply compat_chain_dps. apply H13. do 2 destruct H13. exists x8. intuition. eapply incl_elim with (R := succ_eq# @ succ). apply absorbs_left_rtc. intuition. exists x7. intuition. Qed.
imports: Coq(Lia) CoLoR(LogicUtil ATrs ListUtil RelUtil RelSub Path ARelation SN ListOccur ListNodup AShift VecUtil ASubstitution Iter Cycle)