fact: Fixpoint bfs (fuel : nat) (w : list (state * move)) (settled : state_fmap) (sufficient : state) (round : nat) : (state_fmap * nat) + (list (state * move) * state_fmap) := match fuel with | O => inr (w, settled) | S p => match bfs_aux w nil sufficient settled with | (nil, s) => inl (s, round) | (w, s) => bfs p w s sufficient (round + 1) end end.
imports: mathcomp(all_ssreflect) ZArith QArith List String OrderedType OrderedTypeEx FMapAVL