# 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 :

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

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

3. 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 !