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

import Base
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_rows_count.k(+z: G.Zone, +w: Nat, +y: Nat, +t: List<&2, Nat>, +st: G.GenState,
  r: {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
       st_need(G.gen.row_state(z, y, List.range(w), st))) == st_need(st) : Nat} &
    {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
       st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} &
    {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat},
  ih: {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
       st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} ->
    {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat} ->
    {L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st)))
      == st_need(G.gen.row_state(z, y, List.range(w), st)) : Nat}) ->
  {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
     L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))))
    == st_need(st) : Nat}:
  match r:
    case (r1, rest):
      match rest:
        case (r2, r3):
          %Equal.sym(Nat, L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))),
            st_need(G.gen.row_state(z, y, List.range(w), st)), ih(r2, r3)) :
            {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)), _) == st_need(st) : Nat}
          r1

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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_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/LAWS.bend&name=total_mines
  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/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.left
  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/game.bend&name=gen.rows
  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