proposition: Lemma compose_empty : forall i j, RT_ODPG i j -> hd_red_Mod_SCC' j @ hd_red_Mod_SCC' i << empty.
proof: Proof. intros. unfold inclusion. intros x y H0. destruct H0 as [z]. destruct H0. assert (~ODPGquo' j i). unfold RT in *. destruct topo_sortable_Rquo'. simpl in *. intuition. ded (l (nats_decr_lt dim)). clear l. set (RTbis := fun x y : nat => x0 (nats_decr_lt dim) x y = true) in *. change (RTbis i j) in H. assert (RTbis j i). destruct H3. intuition. apply H5. ded (@Rquo_restricted hyps M HM j i). split; try split; try tauto; destruct H2; try tauto. unfold irreflexive in *. intuition. destruct H3; intuition. apply (H7 i). eapply H5; ehyp. assert (ODPGquo' j i). unfold Rquo'. intuition. unfold Rquo in *. unfold hd_red_Mod_SCC' in *. destruct H0 as [x']. destruct H0. destruct H1 as [z']. destruct H1. destruct H3 as [t1]. destruct H3 as [r1]. destruct H3 as [s1]. exists (mkRule t1 r1); split; try tauto. destruct H4 as [t2]. destruct H4 as [r2]. destruct H4 as [s2]. exists (mkRule t2 r2); split; try tauto. apply over_DPG. eapply hd_red_Mod_rule2_hd_rules_graph; intuition. unfold hd_red_Mod_rule. split. assert (SCC' (mkRule t1 r1) (mkRule t1 r1)). rewrite (SCC'_tag_exact hyps HM). split; try tauto. congruence. destruct H7. tauto. exists s1. subst x'. split; simpl; auto; eauto. intuition. split. assert (SCC' (mkRule t2 r2) (mkRule t2 r2)). rewrite (SCC'_tag_exact hyps HM). split; try tauto. congruence. destruct H7; tauto. exists s2. subst z. split; simpl; auto; eauto. congruence. subst j. unfold RT in *. destruct topo_sortable_Rquo'. simpl in *. ded (l (nats_decr_lt dim)). clear l. destruct H3. intuition. unfold irreflexive in H6. ded (H6 i). auto. tauto. Qed.
imports: Coq(Permutation Multiset Setoid PermutSetoid) CoLoR(SCCTopoOrdering AGraph ATrs RelUtil RelSub BoundNat AdjMat LogicUtil NatUtil SCC SCC_dec ListExtras SN VecUtil GDomainBij OptUtil Union SortUtil ListNodup ListPermutation)