law count_false_set.go

minebender-game@1.0.0.0 · proof_lists.bend:486

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

486law count_false_set.go:
487  for +g: T.Grid(Bool)
488  for +y: Nat
489  for +r: List<&2, Bool>
490  for +r2: List<&2, Bool>
491  for e: {List.get(&2, List<&2, Bool>, g, y) == Some{r} : Maybe<&2, List<&2, Bool>>}
492  for rf: {B.row_false(r) == 1n+B.row_false(r2) : Nat}
493  {B.count_false(g) == 1n+B.count_false(List.set(&2, List<&2, Bool>, g, y, r2)) : Nat}