law gen_rows_wide

minebender-game@1.0.0.0 · proof_gen.bend:48

import Base
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

48law gen_rows_wide:
49  for +z: G.Zone
50  for +w: Nat
51  for +ys: List<&2, Nat>
52  for +st: G.GenState
53  {L.rows_wide(Bool, w, G.gen.rows(z, w, ys, st)) == True{} : Bool}