CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.Strongly Connected Components (SCC) of a graph seen as a relation
- Leo Ducas, 2007-08-06
Definition of SCC seen as a relation : are x and y in the same SCC ?
Lemma SCC_trans : forall x y z, SCC x y -> SCC y z -> SCC x z.
Lemma SCC_sym : forall x y, SCC x y -> SCC y x.
Lemma cycle_in_SCC : forall x l, cycle R x l -> forall y, In y l -> SCC x y.
Lemma SCC_in_cycle : forall x y, SCC x y -> exists l, cycle R x l /\ In y l.
Lemma cycle_in_SCC_bound : forall x l, cycle R x l -> SCC x x.
Variables R1 R2 : relation A.
Lemma SCC_incl : R1 << R2 -> SCC R1 << SCC R2.