def addrr

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:563

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/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
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/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

563def addrr(+r: WU.U64, +Rv: Nat, +er: {SW.value(r) == Rv : Nat}, +hf: {C.fits(53n, Rv) == True{} : Bool}) -> {SW.value(X.add(r, r)) == Nat.add(Rv, Rv) : Nat}:
564  +f64 = SH.fits_mono(54n, 64n, Nat.add(Rv, Rv), {==}, FR.fits_add1(53n, Rv, Rv, hf, hf))
565  e1 = WA.add_value(r, r)
566  +e2 = Equal.cong(Nat, Nat, t => C.low(64n, Nat.add(t, t)), SW.value(r), Rv, er)
567  Equal.trans(Nat, SW.value(X.add(r, r)), C.low(64n, Nat.add(SW.value(r), SW.value(r))), Nat.add(Rv, Rv), e1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(r), SW.value(r))), C.low(64n, Nat.add(Rv, Rv)), Nat.add(Rv, Rv), e2, WW.low_fit(64n, Nat.add(Rv, Rv), f64)))