def at_true_self.row

minebender-game@1.0.0.0 · proof_flood.bend:32

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
import minebender-game@1.0.0.0/proof_lists.bend as PL

32def at_true_self.row(+g: T.Grid(Bool), +x: Nat, +y: Nat, +b: Bool,
33  be: {Nat.is_lt(y, List.length(&2, List<&2, Bool>, g)) == b : Bool},
34  e: {B.at(Bool, False{}, g, T.Pos{x, y}) == True{} : Bool}) ->
35  {B.at(Bool, False{}, B.set_at(Bool, g, T.Pos{x, y}, True{}), T.Pos{x, y}) == True{} : Bool}:
36  match b:
37    case True{}:
38      +r = PL.row_of(Bool, g, y)
39      +r2 = List.set(&2, Bool, r, x, True{})
40      %Equal.sym(Maybe<&2, List<&2, Bool>>, List.get(&2, List<&2, Bool>, List.set(&2, List<&2, Bool>, g, y, r2), y),
41        Some{r2}, PL.get_set_eq(List<&2, Bool>, g, y, r2, be)) :
42        {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
43          == True{} : Bool}
44      at_true_self.col(r, x, Nat.is_lt(x, List.length(&2, Bool, r)), {==}, e)
45    case False{}:
46      Empty.absurd({B.at(Bool, False{}, B.set_at(Bool, g, T.Pos{x, y}, True{}), T.Pos{x, y}) == True{} : Bool},
47        P.false_ne_true(%P.get_out(List<&2, Bool>, g, y, be) :
48          {Maybe.default(&2, Bool, List.get(&2, Bool, Maybe.default(&2, List<&2, Bool>, _, Nil{}), x), False{})
49            == True{} : Bool}; e))