def gen_row_count.k2
minebender-game@1.0.0.0 · proof_gen.bend:477
import minebender-game@1.0.0.0/proof_gen.bend as ProofGen
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/LAWS.bend as L
477def gen_row_count.k2(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
478 +cs: List<&2, T.Pos>,
479 s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
480 r: {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
481 st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
482 {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
483 st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
484 {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}) ->
485 {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)))),
486 st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
487 {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
488 st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
489 {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
490 match r:
491 case (r1, rest):
492 (gen_row_count.step(z, p, st,
493 L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
494 st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))), s1, r1), rest)