def dfs2_eq.node

minebender-game@1.0.0.0 · proof_speed.bend:456

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

456def dfs2_eq.node(+x: Nat, +y: Nat, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
457  +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +t: Nat, +f: Nat,
458  +sh: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, +on: {B.on_board(w, h, T.Pos{x, y}) == True{} : Bool},
459  +et: {S.part_true(part) == t : Nat}, +ef: {S.part_none(part) == f : Nat},
460  +fr: Bool, fre: {S.is_none(S.look(part, T.Pos{x, y})) == fr : Bool},
461  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)>},
462  k0: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == t : Nat} ->
463    {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}})) == Nat.sub(f, 1n) : Nat} ->
464    {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})
465      == 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)>},
466  k1: {S.part_true(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == 1n+t : Nat} ->
467    {S.part_none(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}})) == Nat.sub(f, 1n) : Nat} ->
468    {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})
469      == 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)>}) ->
470  {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, S.Ctx{w, h, n, rows, its}),
471      v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), n),
472          S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), rel)),
473        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})),
474      y0 => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), n),
475          S.items_open(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel)),
476        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}))))
477    == S.dfs.free(fr, u => S.dfs(rest, part, S.Ctx{w, h, n, rows, its}),
478      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),
479        x0 => S.dfs(rest, B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{False{}}), S.Ctx{w, h, n, rows, its})),
480      y0 => S.dfs.when(S.open_ok(B.set_at(Maybe<&2, Bool>, part, T.Pos{x, y}, Some{True{}}), rel, n),
481        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)>}:
482  match fr:
483    case False{}:
484      ks
485    case True{}:
486      +q = {T.Pos{x, y} : T.Pos}
487      +p0 = B.set_at(Maybe<&2, Bool>, part, q, Some{False{}})
488      +p1 = B.set_at(Maybe<&2, Bool>, part, q, Some{True{}})
489      +lk = none_of(S.look(part, q), fre)
490      +e0f = one_less(S.part_none(part), S.part_none(p0), f, ef, none_set(w, h, part, x, y, False{}, sh, on, lk))
491      +e1f = one_less(S.part_none(part), S.part_none(p1), f, ef, none_set(w, h, part, x, y, True{}, sh, on, lk))
492      +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)
493      +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}}
494      +eg0 = {%e0t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool};
495        %e0f : {Bool.and(S.between(S.part_true(p0), _, n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool};
496        {==} : {Bool.and(S.between(t, Nat.sub(f, 1n), n), S.items_open(p0, rel)) == S.open_ok(p0, rel, n) : Bool}}
497      +eg1 = {%e1t : {Bool.and(S.between(_, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool};
498        %e1f : {Bool.and(S.between(S.part_true(p1), _, n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool};
499        {==} : {Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)) == S.open_ok(p1, rel, n) : Bool}}
500      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
501      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,
502        S.dfs2(rest, p0, t, Nat.sub(f, 1n), ctx), S.dfs(rest, p0, ctx), k0(e0t, e0f),
503        Bool.and(S.between(1n+t, Nat.sub(f, 1n), n), S.items_open(p1, rel)), S.open_ok(p1, rel, n), eg1,
504        S.dfs2(rest, p1, 1n+t, Nat.sub(f, 1n), ctx), S.dfs(rest, p1, ctx), k1(e1t, e1f))