ProofGen.firsts_rows.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 749-766 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=749&end_line=766

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 firsts_rows.go(+fx: Nat, +fy: Nat, +w: Nat, +y: Nat, +t: List<&2, Nat>,
  c1: {cnt(fx, List.range(w)) == 1n : Nat},
  ih: {outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)) == cnt(fy, t) : Nat}) ->
  {outs(G.Zone{T.Pos{fx, fy}, False{}}, List.append(&2, T.Pos, B.row_cells(y, List.range(w)), B.cells.go(w, t)))
    == cnt(fy, y <> t) : Nat}:
  +row = B.row_cells(y, List.range(w))
  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, List.append(&2, T.Pos, row, B.cells.go(w, t))),
    Nat.add(outs(G.Zone{T.Pos{fx, fy}, False{}}, row), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t))),
    firsts_append(G.Zone{T.Pos{fx, fy}, False{}}, row, B.cells.go(w, t))) : {_ == cnt(fy, y <> t) : Nat}
  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, row), Bool.pick(Nat, Nat.is_eq(y, fy), cnt(fx, List.range(w)), 0n),
    firsts_row.go(fx, fy, y, List.range(w), Nat.is_eq(y, fy), {==})) :
    {Nat.add(_, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t))) == cnt(fy, y <> t) : Nat}
  %Equal.sym(Nat, cnt(fx, List.range(w)), 1n, c1) :
    {Nat.add(Bool.pick(Nat, Nat.is_eq(y, fy), _, 0n), outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)))
      == cnt(fy, y <> t) : Nat}
  %Equal.sym(Nat, outs(G.Zone{T.Pos{fx, fy}, False{}}, B.cells.go(w, t)), cnt(fy, t), ih) :
    {Nat.add(Bool.pick(Nat, Nat.is_eq(y, fy), 1n, 0n), _) == cnt(fy, y <> t) : Nat}
  {==}

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.range
  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=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=cells.go
  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=cnt
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=firsts_append
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=firsts_row.go
  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