// A graph is a set of edges, each from a source node to a destination node.
type Node = int
type Edge = (Node, Node)
type Graph = set<Edge>

// The set of nodes of a graph is all the nodes appearing in edges.
function Nodes(g: Graph): set<Node> {
  (set edge | edge in g :: edge.0) + (set edge | edge in g :: edge.1)
}

// Definition of *reachability* of one node from another:
ghost predicate Reachable(g: Graph, src: Node, dst: Node) {
  // There exists a path connecting the source and destination.
  exists path: seq<Node> ::
    && |path| >= 1           // The path is nonempty.
    && path[0] == src        // It starts at the right place...
    && path[|path|-1] == dst // ... and finishes at the right place.
    // And it only includes edges that actually appear in the graph:
    && (forall i :: 0 <= i < |path|-1 ==> (path[i], path[i+1]) in g)
}

// Is that definition the same as this one?
ghost predicate ReachableNoDup(g: Graph, src: Node, dst: Node) {
  // There exists a path that meets the same requirements as above...
  exists path: seq<Node> ::
    && |path| >= 1
    && path[0] == src
    && path[|path|-1] == dst
    && (forall i :: 0 <= i < |path|-1 ==> (path[i], path[i+1]) in g)
    // ... *and* it has no duplicates.
    && (forall i, j :: 0 <= i < j < |path| ==> path[i] != path[j])
}

// Yes. Prove the equivalence of those definitions...
lemma ReachableNoDupEquiv(g: Graph, src: Node, dst: Node)
  ensures ReachableNoDup(g, src, dst) == Reachable(g, src, dst)
{
  
}

// ... perhaps with the help of a lemma where you show, given a path that satisfies the
// requirements of Reachable, how you can excise any loops to satisfy ReachableNoDup.