def order_split.cell

minebender-game@1.0.0.0 · proof_solver.bend:1978

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

1978def order_split.cell(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
1979  r: Or({B.same(c, q) == True{} : Bool}, {tcontains(rest, q) == True{} : Bool}),
1980  ih: {tcontains(rest, q) == True{} : Bool} ->
1981    {Bool.or(tcontains(S.nears(rest), q), tcontains(S.fars(rest), q)) == True{} : Bool}) ->
1982  {Bool.or(tcontains(S.nears(S.Todo{c, rel} <> rest), q), tcontains(S.fars(S.Todo{c, rel} <> rest), q)) == True{} : Bool}:
1983  match r:
1984    case Inl{cq}:
1985      order_split.self(c, rel, rest, q, cq, S.has_rel(S.Todo{c, rel}), {==})
1986    case Inr{m}:
1987      order_split.rest(S.Todo{c, rel}, rest, q, S.has_rel(S.Todo{c, rel}),
1988        or_cases(tcontains(S.nears(rest), q), tcontains(S.fars(rest), q), ih(m)))