def loop_none.cov

minebender-game@1.0.0.0 · proof_solver.bend:2349

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

2349def loop_none.cov(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2350  +part: T.Grid(Maybe<&2, Bool>), +w: Nat, +h: Nat, +n: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>,
2351  +val: {all_valid(S.Ctx{w, h, n, rows, its}, found) == True{} : Bool},
2352  +shP: {B.shaped(Maybe<&2, Bool>, w, h, part) == True{} : Bool}, on0: {B.on_board(w, h, c0) == True{} : Bool},
2353  +c: T.Pos, mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2354  +b: Bool, be: {S.covered(found, c0) == b : Bool},
2355  e: {S.loop.if(b, u => S.loop(t, found, todo, part, S.Ctx{w, h, n, rows, its}),
2356      v => S.loop.found(S.search(c0, todo, part, S.Ctx{w, h, n, rows, its}), c0,
2357        l => S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}))) == None{} : Maybe<&2, T.Pos>},
2358  ihf: {S.loop(t, found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
2359    {B.contains(t, c) == True{} : Bool} -> Witness(S.Ctx{w, h, n, rows, its}, c),
2360  ihn: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, S.Ctx{w, h, n, rows, its}) == None{} : Maybe<&2, T.Pos>} ->
2361    {all_valid(S.Ctx{w, h, n, rows, its}, l <> found) == True{} : Bool} -> {B.contains(t, c) == True{} : Bool} ->
2362    Witness(S.Ctx{w, h, n, rows, its}, c)) ->
2363  Witness(S.Ctx{w, h, n, rows, its}, c):
2364  match b:
2365    case True{}:
2366      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2367      loop_none.pick2(ctx, c0, t, c, found, mr, be, val, mt => ihf(e, mt))
2368    case False{}:
2369      +ctx = {S.Ctx{w, h, n, rows, its} : S.Ctx}
2370      loop_none.found(c0, t, found, todo, part, w, h, n, rows, its, val, shP, on0, c, mr,
2371        loop_found_none(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx), e), ihn)