proposition: Lemma WF_hd_red_Mod_SCC_fast_trivial : forall i (Hi : i < dim), SCC_list_fast Hi = nil -> WF (hd_red_Mod_SCC' i).
proof: Proof. intros i Hi; intros. set (L := SCC'_list i). assert (L = SCC'_list i); auto. destruct L. apply WF_chain_SCC_trivial. auto. destruct L. destruct (ODPG_dec h h). assert (R [i] =Some h). assert (In h (SCC'_list i)). rewrite <- H0; simpl; auto. rewrite SCC'_list_exact in H1. gen H1; intro. unfold SCCTopoOrdering.SCC'_tag in H1. simpl in *. ded (find_first_exact _ _ _ H1). do 2 destruct H3. rewrite (SCC'_tag_exact hyps HM) in H4. intuition. cut (x=h). intro; subst x; auto. rewrite H5, <- SCC'_list_exact, <- H0 in H2; simpl in *. intuition. cut (M[[i,i]] = true). intros. unfold mat_unbound in H2. destruct (le_gt_dec dim i); try discr. unfold Peano.gt in *; assert (g=Hi). apply lt_unique. subst g. ded (incl_SCC_list_fast Hi H2). rewrite H, <- H0 in *. unfold incl in H3. ded (H3 h). simpl in *. tauto. assert (SCC ODPG h h). split; apply t_step; auto. rewrite (SCC_effective_exact hyps HM) in H2. unfold SCC_effective in H2. simpl in *. unfold rel_on_dom in H2. ded (restriction o); intuition. ded (eq_In_find_first rule_eq_dec H4). do 2 destruct H3. ded(@nodup_unique rule R h R_nodup _ _ H1 H6). subst x. rewrite H3 in H2. intuition. eapply red_Mod_SCC_trivial_singl; eauto. ded (nodup_SCC'_list i). rewrite <-H0 in H1; simpl in H1; intuition. clear H1 H4 H5. assert(In h (SCC'_list i)); assert(In h0 (SCC'_list i)); try rewrite <- H0; simpl;auto. rewrite SCC'_list_exact in *. rewrite <- H2 in H1. assert (SCC' h h0). rewrite (SCC'_tag_exact hyps HM); auto. split; congruence. destruct H4. destruct H4. assert False; auto. tauto. rewrite H2 in H1. unfold SCCTopoOrdering.SCC'_tag in *. ded (In_find_first2 H2). ded (In_find_first2 H1). do 2 destruct H6. do 2 destruct H7. simpl in *. assert (x=x0). congruence. subst x0. assert (SCC ODPG x x). destruct(rule_eq_dec x h). subst h. eapply SCC_trans. apply H4. apply SCC_sym. apply H4. do 2 destruct H9; try subst x; try tauto. simpl in *. eapply SCC_trans. apply SCC_sym. apply H9. apply H9. cut (M[[i,i]]=true). intros. unfold mat_unbound in H11. destruct (le_gt_dec dim i). cut False; try tauto; lia. unfold Peano.gt in *. assert (g=Hi). apply lt_unique. subst g. ded (incl_SCC_list_fast Hi H11). rewrite H, <- H0 in *. unfold incl in H12. ded (H12 h). simpl in *. tauto. rewrite (SCC_effective_exact hyps HM) in H10. unfold SCC_effective in H10. simpl in *. unfold rel_on_dom in H10. assert (In x R). eapply exists_element_at_in. exists i; auto. ded (eq_In_find_first rule_eq_dec H11). do 2 destruct H12. ded (nodup_unique R_nodup H13 H6). subst x0. rewrite H12 in H10. intuition. 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)