ProofFlood.works_ok_push: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_flood.bend as ProofFlood
Lines 565-577 of minebender-game@1.0.0.0/proof_flood.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_flood.bend&start_line=565&end_line=577

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

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

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=zero_walk
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=neighbours
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=zero
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Work
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=push
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=works
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=neighbours_all
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=zero_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=works_ok
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=works_ok_append
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=works_ok_works
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos