def add_low

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:58

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as P64
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

58def add_low(+x: U32, +y: U32) -> {SG.u32_val(U32.add(x, y)) == C.low(32n, Nat.add(SG.u32_val(x), SG.u32_val(y))) : Nat}:
59  +c = WA.bv(P64.carry32(x, y))
60  +e = Equal.cong(Nat, Nat, t => C.low(32n, t), Nat.add(SG.u32_val(x), SG.u32_val(y)), Nat.add(SG.u32_val(U32.add(x, y)), C.shift(32n, c)), Equal.sym(Nat, Nat.add(SG.u32_val(U32.add(x, y)), C.shift(32n, c)), Nat.add(SG.u32_val(x), SG.u32_val(y)), WA.acons(x, y)))
61  Equal.sym(Nat, C.low(32n, Nat.add(SG.u32_val(x), SG.u32_val(y))), SG.u32_val(U32.add(x, y)), Equal.trans(Nat, C.low(32n, Nat.add(SG.u32_val(x), SG.u32_val(y))), C.low(32n, Nat.add(SG.u32_val(U32.add(x, y)), C.shift(32n, c))), SG.u32_val(U32.add(x, y)), e, WW.low_u(32n, SG.u32_val(U32.add(x, y)), c, LW.vb(U32.add(x, y)))))