~/jendhub

law gen_cell

minebender-game@1.0.0.0 · proof_gen.bend:452

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

452law gen_cell:
453  for +z: G.Zone
454  for +p: T.Pos
455  for +st: G.GenState
456  for +lp: Nat
457  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
458  for lft: {st_left(st) == Nat.add(Bool.pick(Nat, G.gen.out(z, p), 0n, 1n), lp) : Nat}
459  GenStep(z, p, st, lp)

Uses (13)

Used by (1)