def firsts_row.go

minebender-game@1.0.0.0 · proof_gen.bend:729

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/game.bend as G

729def firsts_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
730  +e: {Nat.is_eq(y, fy) == b : Bool}) ->
731  {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, cnt(fx, xs), 0n) : Nat}:
732  match xs:
733    case Nil{}:
734      match b:
735        case True{}:
736          {==}
737        case False{}:
738          {==}
739    case x <> t:
740      %Equal.sym(Bool, Nat.is_eq(y, fy), b, e) :
741        {Nat.add(Bool.pick(Nat, Bool.and(Nat.is_eq(x, fx), _), 1n, 0n), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, t)))
742          == Bool.pick(Nat, b, cnt(fx, x <> t), 0n) : Nat}
743      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.row_cells(y, t)), Bool.pick(Nat, b, cnt(fx, t), 0n),
744        firsts_row.go(fx, fy, y, t, b, e)) :
745        {Nat.add(Bool.pick(Nat, Bool.and(Nat.is_eq(x, fx), b), 1n, 0n), _)
746          == Bool.pick(Nat, b, cnt(fx, x <> t), 0n) : Nat}
747      firsts_row.end(Nat.is_eq(x, fx), b, cnt(fx, t))