def order_split.self

minebender-game@1.0.0.0 · proof_solver.bend:1952

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

1952def order_split.self(+c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
1953  cq: {B.same(c, q) == True{} : Bool}, +hr: Bool, hre: {S.has_rel(S.Todo{c, rel}) == hr : Bool}) ->
1954  {Bool.or(tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.nears(rest), hr), q),
1955    tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.fars(rest), Bool.not(hr)), q)) == True{} : Bool}:
1956  match hr:
1957    case True{}:
1958      or_l(tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.nears(rest), True{}), q),
1959        tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.fars(rest), False{}), q),
1960        tput_self(True{}, c, rel, S.nears(rest), q, {==}, cq))
1961    case False{}:
1962      or_r(tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.nears(rest), False{}), q),
1963        tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, S.fars(rest), True{}), q),
1964        tput_self(True{}, c, rel, S.fars(rest), q, {==}, cq))