title: how to prove that BFS directed-graph traversal algorithm is terminable?
body: <p>how to prove that BFS directed-graph traversal algorithm is <strong>terminable</strong>?
  (I copy the pseudocode from <a href="http://en.wikipedia.org/wiki/Breadth-first_search" rel="nofollow">here</a> )
  Input: A graph G and a root v of G</p>
  
  <pre><code>  procedure BFS(G,v):
        create a queue Q
        enqueue v onto Q
        mark v
        while Q is not empty:
            t ← Q.dequeue()
            if t is what we are looking for:
                return t
            for all edges e in G.incidentEdges(t) do
               o ← G.opposite(t,e)
               if o is not marked:
                    mark o
                    enqueue o onto Q
  </code></pre>