def ops_add

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:165

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as SI
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64

165def ops_add(+a: U32, +b: U32, +h: {I.u32_is(NM.AddOver{a, b}) == False{} : Bool}) -> SI.Ops.add(~U32, ~I.u32_op, ~I.u32_is, ~SG.u32_val, a, b, h):
166  +e = L.subst(Bool, c => {Nat.add(UD.v(U32.add(a, b)), WD.sc(32n, S.bit_value(c))) == Nat.add(UD.v(a), UD.v(b)) : Nat}, P64.carry32(a, b), False{}, carry_of(a, b, h), P64.add_cons(a, b))
167  Equal.trans(Nat, v(U32.add(a, b)), Nat.add(v(U32.add(a, b)), 0n), Nat.add(v(a), v(b)), Equal.sym(Nat, Nat.add(v(U32.add(a, b)), 0n), v(U32.add(a, b)), N.add_zero(v(U32.add(a, b)))), e)