law gen_row_first

minebender-game@1.0.0.0 · proof_gen.bend:106

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

106# A cell of a generated row that is in the zone has no mine.
107law gen_row_first:
108  for +z: G.Zone
109  for +y: Nat
110  for +xs: List<&2, Nat>
111  for +j: Nat
112  for +x: Nat
113  for +st: G.GenState
114  for e: {List.get(&2, Nat, xs, j) == Some{x} : Maybe<&2, Nat>}
115  for +s: {G.gen.out(z, T.Pos{x, y}) == True{} : Bool}
116  {List.get(&2, Bool, G.gen.row(z, y, xs, st), j) == Some{False{}} : Maybe<&2, Bool>}