Lemma 4
If r is the first root from which dfs returns, then r has no exit
Proof:
- Suppose x is an exit
- let z be root of x’s SCC
- r not reachable from z, else in same SCC
- #z ? #x (z ancestor of x; Lemma 2)
- #x ? #r (x is an exit from r)
- #z ? #r, no z ? r path, so return from z first
- Contradiction