I wrote the following algorithm based on BFS. The algorithm detects if a given undirected connected graph contains a cycle. If he contains a cycle, he prints it out. I'm pretty sure it works well, but I do not really know how to prove it right.

Here is the pseudocode:

```
Let s be the root
set parent(s)=s and parent(v)=null for all other v
create queue q ;
enqueue(s,q);
cycle=false;
while (!isEmpty(q) && !cycle) {
u=front(q);
for every edge (u,v) incident to u {
if (parent(v)!=null){
parent(v)=u;
enqueue(v);
}
else if (parent(u)!=v){
cycle=true;
keep the edge (u,v)
}
dequeue(q);
if (cycle){
print edge (u,v)
while (parent(u)!=parent(v))&& (parent(v)!=u)&&(parent(u)!=v){
print edge (u,parent(u)) and edge (v,parent(v))
u=parent(u);
v=parent(v);
}
if (parent(u)==parent(v))
print edge (u,parent(u)) and edge (v,parent(v))
else
print edge (u,v)
}
/**************************************************/
/**************************************************/
```

I worked on the proof, but I can not get it.

First, I want to prove that the algorithm detects a cycle if G contains it.

My idea is the following:

Let us be the root of the FSO. We know that G contains a cycle, so there is a node, so there are two different paths from s to such a node. Let u be the first node to fulfill this.

Since this BFS visits all nodes and examines each edge once, and also marks all visited nodes as visited, it reaches a step in which it visits the node u a second time and then finds the cycle.

Then I want to prove that, in the positive case, the edges that are printed form a cycle, but I really stick with it.