def count_false_zero.go

minebender-game@1.0.0.0 · proof_lists.bend:548

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

548def count_false_zero.go(+w: Nat, +h: Nat, +g: T.Grid(Bool), +x: Nat, +y: Nat,
549  +sh: {B.shaped(Bool, w, h, g) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
550  z: {B.count_false(g) == 0n : Nat}, +b: Bool, e: {B.at(Bool, False{}, g, T.Pos{x, y}) == b : Bool}) ->
551  {B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool}:
552  match b:
553    case True{}:
554      e
555    case False{}:
556      Empty.absurd({B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool},
557        P.succ_ne_zero(B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})),
558          Equal.trans(Nat, 1n+B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})), B.count_false(g), 0n,
559            Equal.sym(Nat, B.count_false(g), 1n+B.count_false(B.set_at(Bool, g, T.Pos{x, y}, True{})),
560              count_false_set(w, h, g, x, y, sh, on, e)), z)))