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 !