law gen_rows_count
minebender-game@1.0.0.0 · proof_gen.bend:567
import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
import Base
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
567law gen_rows_count:
568 for +z: G.Zone
569 for +w: Nat
570 for +ys: List<&2, Nat>
571 for +st: G.GenState
572 for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
573 for lft: {st_left(st) == G.gen.left(z, B.cells.go(w, ys)) : Nat}
574 {L.total_mines(G.gen.rows(z, w, ys, st)) == st_need(st) : Nat}