def wide_row.go

minebender-game@1.0.0.0 · proof_gen.bend:1037

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

1037def wide_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
1038  +e: {nr(fy, y) == b : Bool}) ->
1039  {outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, ncnt(fx, xs), 0n) : Nat}:
1040  match xs:
1041    case Nil{}:
1042      match b:
1043        case True{}:
1044          {==}
1045        case False{}:
1046          {==}
1047    case x <> t:
1048      %Equal.sym(Bool, nr(fy, y), b, e) :
1049        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), _), 1n, 0n), outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)))
1050          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
1051      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)), Bool.pick(Nat, b, ncnt(fx, t), 0n),
1052        wide_row.go(fx, fy, y, t, b, e)) :
1053        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), b), 1n, 0n), _)
1054          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
1055      firsts_row.end(nr(fx, x), b, ncnt(fx, t))