Finding invariant when detecting a cycle Let consider a connected graph $G = (V, E)$ which is not oriented. One way to detect a cycle in such a graph is :


Create an array : seen of size $\mid V \mid$ with seen[i] = false for all $i$

Perform a DFS (or BFS) starting at the node $0$.

When we see a node $i$ : we have two cases : if seen[i] = false then seen[i] = true else we found a cycle.



One idea to prove the correction of this algorithm is saying the following : if the algorithm return true it means there two  nodes $x$ and $y$ such that when we looked at $y$ we have : seen[y] = false and seen[x] = true thus there is a cycle namely the cycle which begin at $x$ and use the only path that connect $x$ and $y$ in the DFS tree and then use the edge $(y,x)$.
The problem is that this is not really rigourous and I am really lokking for an invariant that we help me do the correction of this algorithm rigourously.
So is there any invariant I can use here ?
Thank you very much  !
Assuming we execute line 3 when you first visit a node, and assuming you are working with directed graphs, this algorithm is incorrect (consider what happens with a cross edge discovered by DFS).

Alternatively, assuming you are working with undirected graphs:

The missing part of your argument is the "thus" part; why does the existence of two such nodes imply the existence of a cycle?

To work out the proof, I suggest categorizing what types of edges can exist in the search tree for an undirected graph: tree edges? forward edges? back edges/ cross edges?  Then, categorize what type of edge caused you to visit x when seen[x] was true.  What does that mean the search tree has to look like?