law ena

lawful-fields@0.1.1.0 · proof_num.bend:345

import Base

345# The new value when the test passes (no wrap).
346law ena:
347  for +acc: U32
348  for +x: U32
349  for +M: Nat
350  for +hm: {Nat.pow(2n, 32n) == M : Nat}
351  for +hge: {U32.is_ge(x, 48) == True{} : Bool}
352  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) == True{} : Bool}
353  {U32.to_nat(NA(acc, x)) == Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)) : Nat}