def GenStep

minebender-game@1.0.0.0 · proof_gen.bend:364

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

364# What one cell does to the state: the mines placed plus the mines still
365# needed stay the same, need <= left stays true, and left counts down for
366# every cell outside the zone.
367def GenStep(+z: G.Zone, +p: T.Pos, +st: G.GenState, +lp: Nat) -> Type:
368  {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat} &
369  {Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} &
370  {st_left(G.gen.next(z, p, st)) == lp : Nat}