def contains_remove_other.go

minebender-game@1.0.0.0 · proof_grid.bend:258

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B

258def contains_remove_other.go(+e0: T.Pos, +t: List<&2, T.Pos>, +p: T.Pos, +q: T.Pos,
259  d: {B.same(p, q) == False{} : Bool}, +b: Bool, +e: {B.same(e0, p) == b : Bool},
260  ih: {B.contains(B.remove(t, p), q) == B.contains(t, q) : Bool}) ->
261  {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(B.same(e0, p))), q)
262    == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}:
263  match b:
264    case True{}:
265      %Equal.sym(Bool, B.same(e0, p), True{}, e) :
266        {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(_)), q)
267          == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}
268      %Equal.sym(T.Pos, e0, p, same_sound(e0, p, e)) :
269        {B.contains(B.remove(t, p), q) == Bool.or(B.same(_, q), B.contains(t, q)) : Bool}
270      %Equal.sym(Bool, B.same(p, q), False{}, d) :
271        {B.contains(B.remove(t, p), q) == Bool.or(_, B.contains(t, q)) : Bool}
272      ih
273    case False{}:
274      %Equal.sym(Bool, B.same(e0, p), False{}, e) :
275        {B.contains(List.filter.put(T.Pos, e0, B.remove(t, p), Bool.not(_)), q)
276          == Bool.or(B.same(e0, q), B.contains(t, q)) : Bool}
277      %ih : {Bool.or(B.same(e0, q), B.contains(B.remove(t, p), q))
278        == Bool.or(B.same(e0, q), _) : Bool}
279      {==}