DFS in undirected graph - there is no edge from white vertex to black vertex

The graph is represented by a pair (vertices, successor)

• vertices : this constant is the set of graph vertices
• successor : this function gives for each vertex the set of vertices directly joinable from it

We show that in a undirected graph, the is no edge from a white vertex to a black vertex.
Fully automatic proof, with inductive definition of white paths.

module DfsUndirNoWhiteToBlack
  use import int.Int
  use import list.List
  use import list.Append
  use import list.Mem as L
  use import list.Elements as E
  use import init_graph.GraphSetSucc

  axiom undirected_graph:
    forall x y. edge x y -> edge y x

  predicate nbtw (b g: set vertex) =
    forall x x'. edge x x' -> mem x b -> mem x' (union b g)

  predicate nwtb (b g: set vertex) =
    forall x x'. edge x x' -> mem x' b -> mem x (union b g)

let rec dfs r g b
  variant {(cardinal vertices - cardinal g), (cardinal r)} =
  requires {subset r vertices }
  requires {subset b vertices }
  requires {subset g vertices }
  requires {inter b g == empty}
  ensures {subset result vertices }
  ensures {subset b result }
  ensures {inter result g == empty}
  ensures {subset (diff r g) result &&
           nbtw (diff result (union b g)) (union b g) &&
           nwtb (diff result (union b g)) (union b g)}
  if is_empty r then b else
  let x = choose r in
  let r' = remove x r in
  let v = union b g in
  if mem x v then dfs r' g b else
  let v' = dfs (successors x) (add x g) b in
  assert {diff (add x v') b == add x (diff v' b) };
  let v'' = dfs r' g (add x v') in
  assert {diff v'' b == union (diff v'' (add x v')) (diff (add x v') b) };
  v''
end