ProofGen.wide_row.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 1037-1055 of minebender-game@1.0.0.0/proof_gen.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_gen.bend&start_line=1037&end_line=1055

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

def wide_row.go(+fx: Nat, +fy: Nat, +y: Nat, +xs: List<&2, Nat>, +b: Bool,
  +e: {nr(fy, y) == b : Bool}) ->
  {outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, xs)) == Bool.pick(Nat, b, ncnt(fx, xs), 0n) : Nat}:
  match xs:
    case Nil{}:
      match b:
        case True{}:
          {==}
        case False{}:
          {==}
    case x <> t:
      %Equal.sym(Bool, nr(fy, y), b, e) :
        {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)))
          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
      %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, True{}}, B.row_cells(y, t)), Bool.pick(Nat, b, ncnt(fx, t), 0n),
        wide_row.go(fx, fy, y, t, b, e)) :
        {Nat.add(Bool.pick(Nat, Bool.and(nr(fx, x), b), 1n, 0n), _)
          == Bool.pick(Nat, b, ncnt(fx, x <> t), 0n) : Nat}
      firsts_row.end(nr(fx, x), b, ncnt(fx, t))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=row_cells
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Zone
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=firsts_row.end
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=ncnt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=nr
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=outs
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos