Lemma: Enthaelt ein Graph einen Zyklus, so entsteht bei der Tiefensuche eine Rueckwaertskante. Beweis: Sei der Zyklus a->b->c->d->a und sei a der Knoten im Zyklus mit der kleinsten Entdeckungszeit. Wenn also dann a entdeckt wird, so sind b,c,d alle noch weiss und werden ausgehend von a entdeckt. Bei der Bearbeitung der Kante d->a ist dann a noch grau und diese Kante ist somit eine Rueckwaertskante. [] Die Umkehrung gilt natuerlich auch, denn eine Rueckwaertskante weist nach Definition einen Zyklus aus. Lemma[Korrektheit des Algorithmus zur topologischen Sortierung]: Ist G=(V,E) azyklisch und u->v eine Kante, so gilt f[u]>f[v]. Beweis: Gilt d[u] < d[v] (Entdeckungszeit), so wird v von u aus entdeckt und eher abgefertigt. Es folgt f[u]>f[v]. Gilt d[v] < d[u], so kann u nicht Nachfahre von v sein, denn sonst waere u->v eine Rueckwaertskante im Widerspruch zum vorhergehenden Lemma. Das aber bedeutet, dass v erst ganz abgefertigt wird, bevor ueberhaupt u entdeckt wird (Klammerungseigenschaft!), somit auch hier f[u] > f[v]. [] Es gilt sogar die folgende Verallgemeinerung: Lemma: Falls b ->* a so folgt f[b] > f[a] oder a ->* b. Beweis: Falls d[b]* a, so folgt a ->* b. Beweis: Falls d[b]* a. Im zweiten Fall hat man aber a->*b. Ist umgekehrt d[a]*b. [] Satz: Der Algorithmus zur Berechnung der SCC ist korrekt. Beweis: Entdeckungs- und Abfertigungszeiten beziehen sich immer auf die erste DFS. Bei der zweiten DFS im transponierten Graphen interessieren nur die Baeume, die ja die SCCs ausweisen, nicht aber die Zeitstempel. Auch beziehen sich Notationen wie a->b und a->*b immer auf den Graphen G, nicht auf seine Transposition. Sind a,b stark zusammenhaengend, also a->*b und b->*a so koennen wir oBdA annehmen, dass bei der zweiten Tiefensuche a vor b entdeckt wird. Dann aber kommt b in denselben Baum wie a. Ist umgekehrt b Nachfahre von a im DFS-Wald der zweiten Tiefensuche, so folgt zum einen b->*a, da ja b von a aus im transponierten Graphen erreicht wird. Andererseits muss b beim ersten Besuch von a noch weiss gewesen sein, sonst koennte es ja nicht Nachfahre werden, was insbesondere bedeutet, dass b im Hauptalgorithmus nach a betrachtet wird, also f[b]*b wie verlangt. []