law gen_left_firsts

minebender-game@1.0.0.0 · proof_gen.bend:617

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

617# Every cell is either a candidate or in the zone.
618law gen_left_firsts:
619  for +z: G.Zone
620  for +ps: List<&2, T.Pos>
621  {Nat.add(G.gen.left(z, ps), outs(z, ps)) == List.length(&2, T.Pos, ps) : Nat}