~/jendhub

law step_dg

lawful-fields@0.1.1.0 · proof_num.bend:391

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

391# After byte x, from value a, by the digit test (dg).
392law step_dg:
393  for +acc: U32
394  for +x: U32
395  for +M: Nat
396  for +q: Nat
397  for +dg: Bool
398  for +hdg: {DG(x) == dg : Bool}
399  for +hm: {Nat.pow(2n, 32n) == M : Nat}
400  for +hcq: {U32.to_nat(429496729) == q : Nat}
401  for +hq: {Nat.add(Nat.mul(q, 10n), 6n) == M : Nat}
402  Inv(Bool.and(dg, FT(acc, x)), NA(acc, x), F.dec.push(Some{U32.to_nat(acc)}, F.digit.if(x, dg)), M)

Uses (29)

Used by (1)