def gen_row_count.k

minebender-game@1.0.0.0 · proof_gen.bend:496

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

496def gen_row_count.k(+z: G.Zone, +y: Nat, +t: List<&2, Nat>, +p: T.Pos, +st: G.GenState,
497  +cs: List<&2, T.Pos>,
498  step: GenStep(z, p, st, G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs))),
499  ih: ({Nat.is_le(st_need(G.gen.next(z, p, st)), st_left(G.gen.next(z, p, st))) == True{} : Bool} ->
500    {st_left(G.gen.next(z, p, st)) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, t), cs)) : Nat} ->
501    {Nat.add(L.row_mines(G.gen.row(z, y, t, G.gen.next(z, p, st))),
502       st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(G.gen.next(z, p, st)) : Nat} &
503    {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
504       st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
505    {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat})) ->
506  {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)))),
507     st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == st_need(st) : Nat} &
508  {Nat.is_le(st_need(G.gen.row_state(z, y, t, G.gen.next(z, p, st))),
509     st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st)))) == True{} : Bool} &
510  {st_left(G.gen.row_state(z, y, t, G.gen.next(z, p, st))) == G.gen.left(z, cs) : Nat}:
511  match step:
512    case (s1, rest):
513      match rest:
514        case (s2, s3):
515          gen_row_count.k2(z, y, t, p, st, cs, s1, ih(s2, s3))