def when_or_eq

minebender-game@1.0.0.0 · proof_speed.bend:440

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S

440def when_or_eq(+g0a: Bool, +g0b: Bool, eg0: {g0a == g0b : Bool},
441  +d0a: Maybe<&2, T.Grid(Bool)>, +d0b: Maybe<&2, T.Grid(Bool)>, ed0: {d0a == d0b : Maybe<&2, T.Grid(Bool)>},
442  +g1a: Bool, +g1b: Bool, eg1: {g1a == g1b : Bool},
443  +d1a: Maybe<&2, T.Grid(Bool)>, +d1b: Maybe<&2, T.Grid(Bool)>, ed1: {d1a == d1b : Maybe<&2, T.Grid(Bool)>}) ->
444  {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
445    == S.dfs.or(S.dfs.when(g0b, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}:
446  %eg0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
447    == S.dfs.or(S.dfs.when(_, x => d0b), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
448  %ed0 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
449    == S.dfs.or(S.dfs.when(g0a, x => _), y => S.dfs.when(g1b, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
450  %eg1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
451    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(_, z => d1b)) : Maybe<&2, T.Grid(Bool)>}
452  %ed1 : {S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => d1a))
453    == S.dfs.or(S.dfs.when(g0a, x => d0a), y => S.dfs.when(g1a, z => _)) : Maybe<&2, T.Grid(Bool)>}
454  {==}