law ena_add
lawful-fields@0.1.1.0 · proof_num.bend:329
import lawful-fields@0.1.1.0/proof_num.bend as ProofNum
import Base
329law ena_add:
330 for +acc: U32
331 for +x: U32
332 for +M: Nat
333 for +emul: {U32.to_nat(U32.mul(acc, 10)) == Nat.mul(U32.to_nat(acc), U32.to_nat(10)) : Nat}
334 for +ed: {U32.to_nat(U32.sub(x, 48)) == Nat.sub(U32.to_nat(x), 48n) : Nat}
335 for +hb: {Nat.is_lt(Nat.add(Nat.mul(U32.to_nat(acc), 10n), Nat.sub(U32.to_nat(x), 48n)), M) == True{} : Bool}
336 {Nat.is_lt(Nat.add(U32.to_nat(U32.mul(acc, 10)), U32.to_nat(U32.sub(x, 48))), M) == True{} : Bool}