search

sharmaeklavya2 / theoremdep-source

Source files for TheoremDep - a theorem dependency tracker
https://sharmaeklavya2.github.io/theoremdep/
19 stars 1 forks source link

DFS: White-path theorem: possibly wrong statement #3

Closed zzJinux closed 6 months ago

zzJinux commented 6 months ago

https://sharmaeklavya2.github.io/theoremdep/nodes/graph-theory/dfs/white-path-theorem.html

$v$ is not a descendant of $u \implies u$ was already non-white when visit(w) was called. Therefore, $s(v) < s(w)$.

I couldn't get it why $s(v) < s(w)$ holds. Since $w$ is the predecessor of $v$ in the white path, it seems that $s(v) > s(w)$ is the case. Please let me know if I'm wrong. Besides the $s(v) < s(w)$, I also couldn't understand how “ $v$ is not a descendant of $u \implies u$ was already non-white when visit(w) was called ” holds.

sharmaeklavya2 commented 6 months ago

Thanks for reporting this issue! I couldn't understand what I had written, so I rewrote the proof. Let me know if you still have issues with the proof.