ProofSpeed.dfs2_eq.node: def of minebender-game@1.0.0.0 Import: import minebender-game@1.0.0.0/proof_speed.bend as ProofSpeed Lines 456-504 of minebender-game@1.0.0.0/proof_speed.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_speed.bend&start_line=456&end_line=504 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/solver.bend as S def dfs2_eq.node(+x: Nat, +y: Nat, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +t: Nat, +f: Nat, +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool}, +et: {S.part_true(part) == t : Nat}, +ef: {S.part_none(part) == f : Nat}, +fr: Bool, fre: {S.is_none(S.look(part, T.Pos{x, y})) == fr : Bool}, ks: {S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}) == S.dfs(rest, part, S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}, k0: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == t : Nat} -> {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == Nat.sub(f, 1n) : Nat} -> {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its}) == S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}, k1: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == 1n+t : Nat} -> {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == Nat.sub(f, 1n) : Nat} -> {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), 1n+t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its}) == S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), S.Ctx{w, h, n, rows, its}) : Maybe<&2, T.Grid(Bool)>}) -> {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}), v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel)), x0 => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})), y0 => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel)), z0 => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), 1n+t, Nat.sub(f, 1n), S.Ctx{w, h, n, rows, its})))) == S.dfs.free(fr, u => S.dfs(rest, part, S.Ctx{w, h, n, rows, its}), v => S.dfs.or(S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel, n), x0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its})), y0 => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel, n), z0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), S.Ctx{w, h, n, rows, its})))) : Maybe<&2, T.Grid(Bool)>}: match fr: case False{}: ks case True{}: +q = {T.Pos{x, y} : T.Pos} +p0 = B.set_at(Maybe<&2, Bool>, part, q, Some{False{}}) +p1 = B.set_at(Maybe<&2, Bool>, part, q, Some{True{}}) +lk = none_of(S.look(part, q), fre) +e0f = one_less(S.part_none(part), S.part_none(p0), f, ef, none_set(w, h, part, x, y, False{}, sh, on, lk)) +e1f = one_less(S.part_none(part), S.part_none(p1), f, ef, none_set(w, h, part, x, y, True{}, sh, on, lk)) +e0t = Equal.trans(Nat, S.part_true(p0), S.part_true(part), t, true_set_f(w, h, part, x, y, sh, on, lk), et) +e1t = {%et : {S.part_true(p1) == 1n+_ : Nat}; true_set_t(w, h, part, x, y, sh, on, lk) : {S.part_true(p1) == 1n+t : Nat}} +eg0 = {%e0t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool}; %e0f : {Bool.and(S.between(S.part_true(p0), _, n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool}; {==} : {Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool}} +eg1 = {%e1t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool}; %e1f : {Bool.and(S.between(S.part_true(p1), _, n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool}; {==} : {Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool}} +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx} when_or_eq(Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)), S.open_ok(p0, rel, n), eg0, S.dfs2(rest, p0, t, Nat.sub(f, 1n), ctx), S.dfs(rest, p0, ctx), k0(e0t, e0f), Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)), S.open_ok(p1, rel, n), eg1, S.dfs2(rest, p1, 1n+t, Nat.sub(f, 1n), ctx), S.dfs(rest, p1, ctx), k1(e1t, e1f)) Uses (34): 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=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=Maybe https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=on_board 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/proof_speed.bend&name=none_of https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_speed.bend&name=none_set https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_speed.bend&name=one_less https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_speed.bend&name=true_set_f https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_speed.bend&name=true_set_t https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_speed.bend&name=when_or_eq https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Ctx https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Item https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=Todo https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=between https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.free https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.or https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs.when https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=dfs2 https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=is_none https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=items_open https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=look https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=open_ok https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=part_none https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=part_true 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=Seen