law flood_zero

minebender-game@1.0.0.0 · proof_flood.bend:460

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/game.bend as G

460law flood_zero:
461  for +n: Nat
462  for +work: List<&2, G.Work>
463  for +hd: Bool
464  for +w: Nat
465  for +h: Nat
466  for +layout: T.Grid(Bool)
467  for +shown: T.Grid(Bool)
468  for +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}
469  for +cnt: {n == B.count_false(shown) : Nat}
470  for +he: {G.head_hidden(w, h, shown, work) == hd : Bool}
471  for +q: T.Pos
472  for +before: {B.at(Bool, False{}, shown, q) == False{} : Bool}
473  for +after: {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), q) == True{} : Bool}
474  for +z: {B.zero(w, h, layout, q) == True{} : Bool}
475  for +r: T.Pos
476  for +rm: {B.contains(B.neighbours(w, h, q), r) == True{} : Bool}
477  {B.at(Bool, False{}, G.flood(n, work, hd, w, h, layout, shown), r) == True{} : Bool}