law gen_count_

minebender-game@1.0.0.0 · proof_gen.bend:1217

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

1217law gen_count_:
1218  for +w: Nat
1219  for +h: Nat
1220  for +n: Nat
1221  for +first: T.Pos
1222  for +rs: List<&2, U32>
1223  for on: {L.on_board(w, h, first) == True{} : Bool}
1224  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
1225  {L.total_mines(G.place_mines(w, h, n, first, rs)) == n : Nat}