law gen_rows_get

minebender-game@1.0.0.0 · proof_gen.bend:163

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

163law gen_rows_get:
164  for +z: G.Zone
165  for +w: Nat
166  for +ys: List<&2, Nat>
167  for +i: Nat
168  for +y: Nat
169  for +st: G.GenState
170  for e: {List.get(&2, Nat, ys, i) == Some{y} : Maybe<&2, Nat>}
171  exs st2: G.GenState
172  {List.get(&2, List<&2, Bool>, G.gen.rows(z, w, ys, st), i)
173    == Some{G.gen.row(z, y, List.range(w), st2)} : Maybe<&2, List<&2, Bool>>}