def gen_rows_count.k
minebender-game@1.0.0.0 · proof_gen.bend:544
import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
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
544def gen_rows_count.k(+z: G.Zone, +w: Nat, +y: Nat, +t: List<&2, Nat>, +st: G.GenState,
545 r: {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
546 st_need(G.gen.row_state(z, y, List.range(w), st))) == st_need(st) : Nat} &
547 {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
548 st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} &
549 {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat},
550 ih: {Nat.is_le(st_need(G.gen.row_state(z, y, List.range(w), st)),
551 st_left(G.gen.row_state(z, y, List.range(w), st))) == True{} : Bool} ->
552 {st_left(G.gen.row_state(z, y, List.range(w), st)) == G.gen.left(z, B.cells.go(w, t)) : Nat} ->
553 {L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st)))
554 == st_need(G.gen.row_state(z, y, List.range(w), st)) : Nat}) ->
555 {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)),
556 L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))))
557 == st_need(st) : Nat}:
558 match r:
559 case (r1, rest):
560 match rest:
561 case (r2, r3):
562 %Equal.sym(Nat, L.total_mines(G.gen.rows(z, w, t, G.gen.row_state(z, y, List.range(w), st))),
563 st_need(G.gen.row_state(z, y, List.range(w), st)), ih(r2, r3)) :
564 {Nat.add(L.row_mines(G.gen.row(z, y, List.range(w), st)), _) == st_need(st) : Nat}
565 r1