proposition: Lemma SCC_effective_exact : forall M (H : M = SCC_mat_effective) x y, SCC R x y <-> SCC_effective H x y.
proof: Proof. split; intros; unfold SCC_effective in *; unfold SCC_mat_effective in *; rewrite <- (dom_change_SCC eq_dec restriction Dom_nodup x y) in *; unfold rel_on_dom in *; destruct (find_first (eq x) (eq_dec x) Dom); auto with *; destruct (find_first (eq y) (eq_dec y) Dom); auto with *; subst; rewrite GoM_SCC in *. assert (rel_on_nat Dom R << GoM (MoG dim (rel_on_nat Dom R) (rel_on_nat_dec Dom R R_dec))). unfold inclusion; intros; rewrite GoM_MoG; intros. trivial. ded (rel_on_nat_is_restricted _ _ _ _ H1). do 2 rewrite <- In_nats_decr_lt in H2; trivial. ded (SCC_incl H); auto. assert (GoM (MoG dim (rel_on_nat Dom R) (rel_on_nat_dec Dom R R_dec)) << rel_on_nat Dom R). unfold inclusion; intros. rewrite GoM_MoG in H; intros; auto. ded (rel_on_nat_is_restricted _ _ _ _ H1). do 2 rewrite <- In_nats_decr_lt in H2; trivial. ded (SCC_incl H). auto. Qed.
imports: CoLoR(GDomainBij AdjMat RelSub ListExtras RelUtil LogicUtil BoundNat SCC ListNodup)