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

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/proof_base.bend as P

def gen_row_count.step(+z: G.Zone, +p: T.Pos, +st: G.GenState, +rm: Nat, +nf: Nat,
  s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
  r1: {Nat.add(rm, nf) == st_need(G.gen.next(z, p, st)) : Nat}) ->
  {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf) == st_need(st) : Nat}:
  %Equal.sym(Nat, Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf),
    Nat.add(one(G.gen.bit(z, p, st)), Nat.add(rm, nf)),
    P.add_assoc(one(G.gen.bit(z, p, st)), rm, nf)) : {_ == st_need(st) : Nat}
  %Equal.sym(Nat, Nat.add(rm, nf), st_need(G.gen.next(z, p, st)), r1) :
    {Nat.add(one(G.gen.bit(z, p, st)), _) == st_need(st) : Nat}
  s1

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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/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.next
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=add_assoc
  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_need
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos