anchor.diff:          && Seq.forall (fun { InEdge.Command = c } -> isNop c) yToX
   
       /// <summary>
  +    ///     Plumbs a function over various properties of a graph and
  +    ///     node into the format expected by <c>onNodes</c>.
  +    /// </summary>
  +    /// <param name="f">
  +    ///     The function, which takes:
  +    ///     the name of the node to look at for optimising;
  +    ///     the view of the node;
  +    ///     the out-edges of the node;
  +    ///     the in-edges of the node;
  +    ///     the graph to optimise;
  +    ///     and the list of edges removed from the node so far, to append
  +    ///     to if this optimisation removes nodes.
  +    ///
  +    ///     It should return the list of edges removed, the optimised
  +    ///     graph, and an Option containing the node name if the node has
  +    ///     not been removed.
  +    /// </param>
  +    /// <returns>
  +    ///     A new function, which takes and returns the edge-graph-node
  +    ///     triple <c>onNodes</c> expects.
  +    /// </returns>
  +    let expandNodeIn f =
  +        function
  +        | (rs, g, None) -> (rs, g, None)
  +        | (rs, g, Some n) ->
  +            match Map.tryFind n g.Contents with
  +            | Some (nV, outs, ins) -> f n nV outs ins g rs
  +            | None -> (rs, g, Some n)
  +
  +    /// <summary>
       ///     Given a node, tries to unify every other node that is
       ///     equivalent and connected, but only by no-op commands, into it.
  +    /// </summary>
  +    /// <param name="_arg1">
  +    ///     A triple of:
  +    ///     the list of edges already removed, which is appended to in the
  +    ///     result;
  +    ///     the graph to optimise (perhaps);
  +    ///     an Option containing the name of the node to optimise.
  +    /// </param>
  +    /// <returns>
  +    ///     A triple containing the list of node names removed, a graph,
  +    ///     and the input node Option.
  +    ///     The graph is equivalent to <paramref name="g" />, but with some
  +    ///     nodes merged into the named node if they are
  +    ///     equivalent and connected only by no-op commands.
  +    /// </returns>
  +    let collapseNops =
  +        expandNodeIn <|
  +            fun nName nView outEdges inEdges g removed ->
  +                let outNodes = outEdges
  +                               |> Set.toSeq
  +                               |> Seq.map (fun { Dest = d } -> d)
  +                let inNodes = inEdges
  +                              |> Set.toSeq
  +                              |> Seq.map (fun { Src = s } -> s)
  +
  +                Seq.append outNodes inNodes
  +                // Then, find out which ones are nop-connected.
  +                |> Seq.filter (nopConnected g nName)
  +                (* If we found any nodes, then unify them.
  +                 * We also have to wipe out the edges between both nodes.
  +                 *)
  +                |> Seq.fold (fun (xs, gg) xName ->
  +                                gg
  +                                |> rmEdgesBetween nName xName
  +                                |> rmEdgesBetween xName nName
  +                                |> unify nName xName
  +                                |> mkPair (xName :: xs))
  +                            (removed, g)
  +                |> fun (removed', g') -> (removed', g', Some nName)
  +
  +    /// <summary>
  +    ///     Safely stitches the names of two edges together.
  +    /// </summary>
  +    /// <param name="_arg1">
  +    ///     The first edge, heading in.
  +    /// </param>
  +    /// <param name="_arg2">
  +    ///     The second edge, heading out.
  +    /// </param>
  +    /// <returns>
  +    ///     A name for any edge replacing both above edges.
  +    /// </returns>
  +    let glueNames { InEdge.Name = a } { OutEdge.Name = b } =
  +        String.concat "__" [ a ; b ]
  +
  +
  +    /// <summary>
  +    ///     Removes a node if it is an ITE-guarded view.
  +    ///
  +    ///     <para>
  +    ///         An ITE-guarded view is a view with one in-edge,
  +    ///         two guarded funcs which negate each other, and two
  +    ///         out-edges, each assuming one of the guards.
  +    ///     </para>
       /// </summary>
       /// <param name="_arg1">
       ///     A triple of:
  
positive.code:     ///     node optimisation <paramref name="opt" /> performed as many times
      ///     as possible.
      /// </returns>
      let rec liftNodeOptimisation opt graph =
          // TODO(CaptainHayashi): do a proper depth-first search instead.
  
          let (xs, newGraph, _) =
  
negative.code:     ///     an Option containing the name of the node to optimise.
      /// </param>
      /// <returns>
      ///     A triple containing the list of edge names removed, an
      ///     optimised graph, and an Option containing the node name if it was
      ///     not removed.
      /// </returns>
      let collapseITEs =
          expandNodeIn <|
              fun nName nView outEdges inEdges g removed ->
                  match nView with
                  | ITEGuards ({ Cond = xc }, { Cond = yc }) ->
                      // Are there only two out edges, and only one in edges?
                      if (Set.count outEdges = 2 && Set.count inEdges = 1)
                      then
                          let oE, iE = Set.toList outEdges, Set.toList inEdges
                          let outA, outB = oE.[0], oE.[1]
                          let inA : InEdge = iE.[0]
  
                          (* Translate xc and yc to pre-state, to match the
                             commands. *)
                          let xcPre = (liftMarker Before always).BSub xc
                          let ycPre = (liftMarker Before always).BSub yc
  
                          // Are the out edges assumes over xc and yc?
                          match (outA.Command, outB.Command) with
                          | ([ { Name = aN ; Params = [ BExpr aP ] } ],
                             [ { Name = bN ; Params = [ BExpr bP ] } ])
                              when (aN = "Assume" && bN = "Assume"
                                    && equivHolds <|
                                           orEquiv
                                               (andEquiv (equiv aP xcPre)
                                                         (equiv bP ycPre))
                                               (andEquiv (equiv aP ycPre)
                                                         (equiv bP xcPre))) ->
                              let removed' =
                                  outA.Name :: outB.Name :: inA.Name :: removed
  
                              let aCmd = inA.Command @ outA.Command
  
                              g
                              // Remove the existing edges first.
                              |> rmEdgesBetween inA.Src nName
                              |> rmEdgesBetween nName outA.Dest
                              |> rmEdgesBetween nName outB.Dest
                              // Then, remove the node.
                              |> rmNode nName
                              // Then, add the new edges.
                              |> mkEdgeBetween (glueNames inA outA)
                                               inA.Src
                                               outA.Dest
                                               (inA.Command @ outA.Command)
                              |> mkEdgeBetween (glueNames inA outB)
                                               inA.Src
                                               outB.Dest
                                               (inA.Command @ outB.Command)
                              |> (fun g' -> removed', g', None)
                          | _ -> (removed, g, Some nName)
                      else (removed, g, Some nName)
                  | _ -> (removed, g, Some nName)
  
  
      /// <summary>
      ///     Performs a node-wise optimisation on every node in the graph.
  