law gen_row_count

minebender-game@1.0.0.0 · proof_gen.bend:518

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

518law gen_row_count:
519  for +z: G.Zone
520  for +y: Nat
521  for +xs: List<&2, Nat>
522  for +st: G.GenState
523  for +cs: List<&2, T.Pos>
524  for inv: {Nat.is_le(st_need(st), st_left(st)) == True{} : Bool}
525  for lft: {st_left(st) == G.gen.left(z, List.append(&2, T.Pos, B.row_cells(y, xs), cs)) : Nat}
526  {Nat.add(L.row_mines(G.gen.row(z, y, xs, st)), st_need(G.gen.row_state(z, y, xs, st)))
527    == st_need(st) : Nat} &
528  {Nat.is_le(st_need(G.gen.row_state(z, y, xs, st)), st_left(G.gen.row_state(z, y, xs, st)))
529    == True{} : Bool} &
530  {st_left(G.gen.row_state(z, y, xs, st)) == G.gen.left(z, cs) : Nat}