ProofGen.gen_row_count.k: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
Lines 496-515 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=496&end_line=515

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
import minebender-game@1.0.0.0/LAWS.bend as L

def gen_row_count.k(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
  +cs: List<&2, T.Pos>,
  step: GenStep(z, p, st, G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs))),
  ih: ({Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} ->
    {st_left(G.gen.next(z, p, st)) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs)) : Nat} ->
    {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
       st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
    {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
       st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
    {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat})) ->
  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st)))),
     st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
  {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
     st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
  {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
  match step:
    case (s1, rest):
      match rest:
        case (s2, s3):
          gen_row_count.k2(z, y, t, p, st, cs, s1, ih(s2, s3))

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=row_mines
  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=GenState
  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/game.bend&name=gen.bit
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.left
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.next
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.row
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=gen.row_state
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=GenStep
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=gen_row_count.k2
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=one
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=st_left
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_gen.bend&name=st_need
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos