def at_true_self.col

minebender-game@1.0.0.0 · proof_flood.bend:18

import Base
import minebender-game@1.0.0.0/proof_base.bend as P
import minebender-game@1.0.0.0/proof_lists.bend as PL

18def at_true_self.col(+r: List<&2, Bool>, +x: Nat, +b: Bool,
19  be: {Nat.is_lt(x, List.length(&2, Bool, r)) == b : Bool},
20  e: {Maybe.default(&2, Bool, List.get(&2, Bool, r, x), False{}) == True{} : Bool}) ->
21  {Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool}:
22  match b:
23    case True{}:
24      %Equal.sym(Maybe<&2, Bool>, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), Some{True{}},
25        PL.get_set_eq(Bool, r, x, True{}, be)) : {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}
26      {==}
27    case False{}:
28      Empty.absurd({Maybe.default(&2, Bool, List.get(&2, Bool, List.set(&2, Bool, r, x, True{}), x), False{}) == True{} : Bool},
29        P.false_ne_true(%P.get_out(Bool, r, x, be) :
30          {Maybe.default(&2, Bool, _, False{}) == True{} : Bool}; e))