def dfs2_some_keep.node

minebender-game@1.0.0.0 · proof_solver.bend:1316

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

1316def dfs2_some_keep.node(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +part: T.Grid(Maybe<&2, Bool>),
1317  +t: Nat, +f: Nat, +ctx: S.Ctx, +l: T.Grid(Bool), +q: T.Pos, +bq: Bool, +fr: Bool, +fre: {S.is_none(S.look(part, c)) == fr : Bool},
1318  e: {S.dfs.free(fr, u => S.dfs2(rest, part, t, f, ctx),
1319      v => S.dfs.or(S.dfs.when(Bool.and(S.between(t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel)),
1320        x => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx)),
1321      y => S.dfs.when(Bool.and(S.between(1n+t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel)),
1322        z => S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx)))) == Some{l} : Maybe<&2, T.Grid(Bool)>},
1323  +lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
1324  kp: {S.dfs2(rest, part, t, f, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} -> {B.mine(l, q) == bq : Bool},
1325  k0: {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1326    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool},
1327  k1: {S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>} ->
1328    {S.look(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), q) == Some{bq} : Maybe<&2, Bool>} -> {B.mine(l, q) == bq : Bool}) ->
1329  {B.mine(l, q) == bq : Bool}:
1330  match fr:
1331    case False{}:
1332      kp(e)
1333    case True{}:
1334      +d0 = S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), t, Nat.sub(f, 1n), ctx)
1335      +d1 = S.dfs2(rest, B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), 1n+t, Nat.sub(f, 1n), ctx)
1336      dfs_some_keep.br(l, q, bq, d0, d1,
1337        dfs_branch_some(Bool.and(S.between(t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{False{}}), rel)),
1338          Bool.and(S.between(1n+t, Nat.sub(f, 1n), S.ctx_n(ctx)), S.items_open(B.set_at(Maybe<&2, Bool>, part, c, Some{True{}}), rel)), d0, d1, l, e),
1339        e0 => k0(e0, set_keep(part, c, q, Some{False{}}, bq, fre, lq, B.same(c, q), {==})),
1340        e1 => k1(e1, set_keep(part, c, q, Some{True{}}, bq, fre, lq, B.same(c, q), {==})))