law inv_step
lawful-fields@0.1.1.0 · proof_num.bend:417
import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
import Base
import lawful-fields@0.1.1.0/defs.bend as F
417law inv_step:
418 for +ok: Bool
419 for +acc: U32
420 for +m: Maybe<&2, Nat>
421 for +x: U32
422 for +M: Nat
423 for +q: Nat
424 for +hm: {Nat.pow(2n, 32n) == M : Nat}
425 for +hcq: {U32.to_nat(429496729) == q : Nat}
426 for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
427 for +hi: Inv(ok, acc, m, M)
428 Inv(Bool.and(ok, Bool.and(DG(x), FT(acc, x))), NA(acc, x), F.dec.push(m, F.digit(x)), M)