def at_set_ne.go

minebender-game@1.0.0.0 · proof_lists.bend:289

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/proof_base.bend as P

289def at_set_ne.go(-A: Data, +g: T.Grid(A), +x: Nat, +y: Nat, +qx: Nat, +qy: Nat, +v: A, +d: A,
290  ne: {B.same(T.Pos{x, y}, T.Pos{qx, qy}) == False{} : Bool}, +b: Bool,
291  +be: {Nat.is_eq(y, qy) == b : Bool}) ->
292  {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, qy}) == B.at(A, d, g, T.Pos{qx, qy}) : A}:
293  match b:
294    case False{}:
295      %Equal.sym(Maybe<&2, List<&2, A>>,
296        List.get(&2, List<&2, A>, List.set(&2, List<&2, A>, g, y, List.set(&2, A, row_of(A, g, y), x, v)), qy),
297        List.get(&2, List<&2, A>, g, qy),
298        get_set_ne(List<&2, A>, g, y, qy, List.set(&2, A, row_of(A, g, y), x, v), be)) :
299        {Maybe.default(&2, A, List.get(&2, A, Maybe.default(&2, List<&2, A>, _, Nil{}), qx), d)
300          == B.at(A, d, g, T.Pos{qx, qy}) : A}
301      {==}
302    case True{}:
303      +yq = P.eq_sound(y, qy, be)
304      %yq : {B.at(A, d, B.set_at(A, g, T.Pos{x, y}, v), T.Pos{qx, _}) == B.at(A, d, g, T.Pos{qx, _}) : A}
305      at_set_ne.row(A, g, x, y, qx, v, d,
306        {%P.and_true_r_id(Nat.is_eq(x, qx)) : {_ == False{} : Bool};
307          %be : {Bool.and(Nat.is_eq(x, qx), _) == False{} : Bool};
308          ne : {Nat.is_eq(x, qx) == False{} : Bool}},
309        Nat.is_lt(y, List.length(&2, List<&2, A>, g)), {==})