def gen_cell.need

minebender-game@1.0.0.0 · proof_gen.bend:399

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

399def gen_cell.need(+z: G.Zone, +p: T.Pos, +need: Nat, +lp: Nat, +rs: List<&2, U32>,
400  inv: {Nat.is_le(need, 1n+lp) == True{} : Bool}) ->
401  {Nat.add(one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))),
402     Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs))))) == need : Nat} &
403  {Nat.is_le(Nat.sub(need, one(Bool.and(Nat.is_lt(0n, need), G.gen.pick(need, 1n+lp, rs)))),
404     Nat.sub(1n+lp, 1n)) == True{} : Bool} &
405  {Nat.sub(1n+lp, 1n) == lp : Nat}:
406  match need:
407    case 0n:
408      %Equal.sym(Nat, Nat.sub(lp, 0n), lp, P.sub_zero(lp)) :
409        {0n == 0n : Nat} & {Nat.is_le(0n, _) == True{} : Bool} & {_ == lp : Nat}
410      ({==}, (P.le_zero_l(lp), {==}))
411    case 1n+m:
412      gen_take(z, p, m, lp, rs, inv, G.gen.pick(1n+m, 1n+lp, rs), {==})