law gen_inv_one

minebender-game@1.0.0.0 · proof_gen.bend:1145

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

1145# With just the first click kept free, there are w*h - 1 candidates, so
1146# n < w*h mines fit among them.
1147law gen_inv_one:
1148  for +w: Nat
1149  for +h: Nat
1150  for +n: Nat
1151  for +fx: Nat
1152  for +fy: Nat
1153  for +on: {L.on_board(w, h, T.Pos{fx, fy}) == True{} : Bool}
1154  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1155  {Nat.is_le(n, G.gen.left(G.Zone{T.Pos{fx, fy}, False{}}, B.cells(w, h))) == True{} : Bool}