def gen_row_count.step
minebender-game@1.0.0.0 · proof_gen.bend:466
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/proof_base.bend as P
466def gen_row_count.step(+z: G.Zone, +p: T.Pos, +st: G.GenState, +rm: Nat, +nf: Nat,
467 s1: {Nat.add(one(G.gen.bit(z, p, st)), st_need(G.gen.next(z, p, st))) == st_need(st) : Nat},
468 r1: {Nat.add(rm, nf) == st_need(G.gen.next(z, p, st)) : Nat}) ->
469 {Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf) == st_need(st) : Nat}:
470 %Equal.sym(Nat, Nat.add(Nat.add(one(G.gen.bit(z, p, st)), rm), nf),
471 Nat.add(one(G.gen.bit(z, p, st)), Nat.add(rm, nf)),
472 P.add_assoc(one(G.gen.bit(z, p, st)), rm, nf)) : {_ == st_need(st) : Nat}
473 %Equal.sym(Nat, Nat.add(rm, nf), st_need(G.gen.next(z, p, st)), r1) :
474 {Nat.add(one(G.gen.bit(z, p, st)), _) == st_need(st) : Nat}
475 s1