law gen_inv

minebender-game@1.0.0.0 · proof_gen.bend:1202

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

1202# Whichever zone the board keeps free, the n mines fit outside it.
1203law gen_inv:
1204  for +w: Nat
1205  for +h: Nat
1206  for +n: Nat
1207  for +first: T.Pos
1208  for +on: {L.on_board(w, h, first) == True{} : Bool}
1209  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1210  {Nat.is_le(n, G.gen.left(zone(w, h, n, first), B.cells(w, h))) == True{} : Bool}