def works_ok_push

minebender-game@1.0.0.0 · proof_flood.bend:565

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
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_copy.bend as PC
import minebender-game@1.0.0.0/proof_cells.bend as PS

565def works_ok_push(+z: Bool, +c: T.Pos, +back: List<&2, T.Pos>, +rest: List<&2, G.Work>, +w: Nat, +h: Nat,
566  +layout: T.Grid(Bool), +p0: T.Pos, ze: {B.zero(w, h, layout, c) == z : Bool},
567  okc: {L.zero_walk(List.reverse(&2, T.Pos, back), w, h, layout, p0, c) == True{} : Bool},
568  okr: {works_ok(rest, w, h, layout, p0) == True{} : Bool}) ->
569  {works_ok(G.push(z, B.neighbours(w, h, c), back, rest), w, h, layout, p0) == True{} : Bool}:
570  match z:
571    case True{}:
572      works_ok_append(G.works(B.neighbours(w, h, c), back), rest, w, h, layout, p0,
573        works_ok_works(B.neighbours(w, h, c), back, c, w, h, layout, p0, okc,
574          %PC.zero_eq(w, h, layout, c) : {_ == True{} : Bool}; ze,
575          PS.neighbours_all(w, h, c)), okr)
576    case False{}:
577      okr