law step_fb

lawful-fields@0.1.1.0 · proof_num.bend:370

import Base

370# After a digit, by the overflow test (b).
371law step_fb:
372  for +acc: U32
373  for +x: U32
374  for +M: Nat
375  for +b: Bool
376  for +hm: {Nat.pow(2n, 32n) == M : Nat}
377  for +hge: {U32.is_ge(x, 48) == True{} : Bool}
378  for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) == b : Bool}
379  Inv(b, NA(acc, x), Some{Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n))}, M)