law cells_on.go

minebender-game@1.0.0.0 · proof_cells.bend:387

import Base
import minebender-game@1.0.0.0/board.bend as B

387law cells_on.go:
388  for +w: Nat
389  for +h: Nat
390  for +ys: List<&2, Nat>
391  for +yh: {alln(ys, h) == True{} : Bool}
392  {allp(~WH, ~onb, WH{w, h}, B.cells.go(w, ys)) == True{} : Bool}