law gen_first_safe_

minebender-game@1.0.0.0 · proof_gen.bend:294

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

294law gen_first_safe_:
295  for +w: Nat
296  for +h: Nat
297  for +n: Nat
298  for +first: T.Pos
299  for +rs: List<&2, U32>
300  {L.mine(G.place_mines(w, h, n, first, rs), first) == False{} : Bool}