law gen_opening_

minebender-game@1.0.0.0 · proof_gen.bend:327

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

327# With room, no cell next to the first click gets a mine.
328law gen_opening_:
329  for +w: Nat
330  for +h: Nat
331  for +n: Nat
332  for +first: T.Pos
333  for +rs: List<&2, U32>
334  for +room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
335  for +q: T.Pos
336  for +near: {L.within_one(first, q) == True{} : Bool}
337  {L.mine(G.place_mines(w, h, n, first, rs), q) == False{} : Bool}