No. B may belong to several different valid routes. A path-local set prevents repeats within one route and is undone on return. A global set is appropriate for ordinary reachability, where exploring the same vertex again adds no new reachable vertices.

def reachable(graph, start):
    seen = {start}
    stack = [start]
    while stack:
        node = stack.pop()
        for neighbor in graph.get(node, []):
            if neighbor not in seen:
                seen.add(neighbor)
                stack.append(neighbor)
    return seen

graph = {"A": ["B"], "B": ["A", "C"], "C": []}
assert reachable(graph, "A") == {"A", "B", "C"}

This iterative depth-first reachability search uses a last-in-first-out stack and global discovery. It handles cycles and takes O(V+E) time and O(V) extra space. For precise recursive DFS entry/exit ordering, use recursion or stack frames that also track the next neighbor; the simple stack above only promises reachability.

Directed cycle detection needs to distinguish an active ancestor from a completed vertex. Use unseen, active, and finished states. An edge to an active ancestor signals a cycle; an edge to an already finished vertex may just represent shared work.

Undirected cycle detection has another wrinkle: the edge back to the parent is normal. A simple undirected graph traversal must distinguish that parent edge from another previously discovered neighbor.

Analogy limit: a footprint on a map does not tell you whether the visit belongs to the current route, a completed route, or another unfinished branch. Your data structure must encode the distinction the proof uses.

Yes, for a fixed graph where future legal moves depend only on the vertex. Revisiting a fully explored vertex cannot reveal additional reachable destinations.