ProofInv.inv_open.go: def of minebender-game@1.0.0.0 Import: import minebender-game@1.0.0.0/proof_inv.bend as ProofInv Lines 539-576 of minebender-game@1.0.0.0/proof_inv.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_inv.bend&start_line=539&end_line=576 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_base.bend as P import minebender-game@1.0.0.0/proof_copy.bend as PC import minebender-game@1.0.0.0/proof_lists.bend as PL import minebender-game@1.0.0.0/proof_cells.bend as PS import minebender-game@1.0.0.0/proof_walk.bend as PW import minebender-game@1.0.0.0/proof_flood.bend as PF def inv_open.go(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +shown: T.Grid(Bool), +flags: List<&2, T.Pos>, +status: T.Status, +sh: {B.shaped(Bool, w, h, shown) == True{} : Bool}, +won: {L.is_won(status) == G.all_safe(w, h, layout, shown) : Bool}, +cm: {calm(status, w, h, layout, shown) == True{} : Bool}, +cl: {closed(w, h, layout, shown) == True{} : Bool}, +p: T.Pos, +c: Bool, ce: {Bool.and(G.is_playing(status), G.unrevealed(w, h, shown, p)) == c : Bool}, +m: Bool, +me: {B.mine(layout, p) == m : Bool}) -> Inv(w, h, layout, G.open.go(c, m, G.Game{w, h, layout, shown, flags, status}, p)): match c m: case False{} _: ({==}, ({==}, ({==}, (sh, (won, (cm, cl)))))) case True{} True{}: +st = playing_is(status, P.and_true_l(G.is_playing(status), G.unrevealed(w, h, shown, p), ce)) +s2 = B.set_at(Bool, shown, p, True{}) +w0 = {%st : {L.is_won(_) == G.all_safe(w, h, layout, shown) : Bool}; won : {False{} == G.all_safe(w, h, layout, shown) : Bool}} ({==}, ({==}, ({==}, (PL.shaped_set(Bool, w, h, shown, p, True{}, sh), (Equal.trans(Bool, False{}, G.all_safe(w, h, layout, shown), G.all_safe(w, h, layout, s2), w0, Equal.sym(Bool, G.all_safe(w, h, layout, s2), G.all_safe(w, h, layout, shown), all_safe_set_mine(w, h, layout, shown, p, me))), ({==}, closed_explode(w, h, layout, shown, p, me, cl))))))) case True{} False{}: +st = playing_is(status, P.and_true_l(G.is_playing(status), G.unrevealed(w, h, shown, p), ce)) +start = {[G.Work{p, Nil{}}] : List<&2, G.Work>} +cf = B.count_false(shown) +hh = G.head_hidden(w, h, shown, start) +F = G.flood(cf, start, hh, w, h, layout, shown) +ns = {%st : {Bool.or(Bool.not(G.is_playing(_)), nsm(w, h, layout, shown)) == True{} : Bool}; cm : {nsm(w, h, layout, shown) == True{} : Bool}} +ok = {%Equal.sym(Bool, L.same(p, p), True{}, PW.lsame_refl(p)) : {Bool.and(_, True{}) == True{} : Bool}; {==} : {PF.works_ok(start, w, h, layout, p) == True{} : Bool}} +safe = {%PC.mine_eq(layout, p) : {_ == False{} : Bool}; me : {L.mine(layout, p) == False{} : Bool}} ({==}, ({==}, ({==}, (PF.flood_shaped(cf, start, hh, w, h, layout, shown, sh), (won_or_playing_won(G.all_safe(w, h, layout, F)), (%Equal.sym(Bool, nsm(w, h, layout, F), True{}, nsm_flood(cf, start, hh, w, h, layout, shown, p, safe, ok, ns)) : {Bool.or(Bool.not(G.is_playing(G.won_or_playing(G.all_safe(w, h, layout, F)))), _) == True{} : Bool}; PS.or_true_r(Bool.not(G.is_playing(G.won_or_playing(G.all_safe(w, h, layout, F))))), closed_flood(cf, start, hh, w, h, layout, shown, sh, cl, {==}, {==}))))))) Uses (45): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_won https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=mine https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=same https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=count_false https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=set_at https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=shaped https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game 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=all_safe https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=flood https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=head_hidden https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=is_playing https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=open.go https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=unrevealed https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=won_or_playing https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=and_true_l https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=or_true_r https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=mine_eq https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_flood.bend&name=flood_shaped 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_inv.bend&name=Inv https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=all_safe_set_mine https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=calm https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=closed https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=closed_explode https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=closed_flood https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=nsm https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=nsm_flood https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=playing_is https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=won_or_playing_won https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_lists.bend&name=shaped_set https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_walk.bend&name=lsame_refl 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 https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Status