def addv2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addc.bend:68

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

68def addv2(+fa: WU.U64, +fb: WU.U64, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(fa) == Fa : Nat}, +hfb: {SW.value(fb) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}) -> {SW.value(X.add(fa, fb)) == Nat.add(Fa, Fb) : Nat}:
69  a1 = WA.add_value(fa, fb)
70  +f53 = FR.fits_add1(52n, Fa, Fb, hFa, hFb)
71  Equal.trans(Nat, SW.value(X.add(fa, fb)), C.low(64n, Nat.add(SW.value(fa), SW.value(fb))), Nat.add(Fa, Fb), a1, Equal.trans(Nat, C.low(64n, Nat.add(SW.value(fa), SW.value(fb))), C.low(64n, Nat.add(Fa, Fb)), Nat.add(Fa, Fb), Equal.cong(Nat, Nat, z => C.low(64n, z), Nat.add(SW.value(fa), SW.value(fb)), Nat.add(Fa, Fb), Equal.trans(Nat, Nat.add(SW.value(fa), SW.value(fb)), Nat.add(Fa, SW.value(fb)), Nat.add(Fa, Fb), Equal.cong(Nat, Nat, z => Nat.add(z, SW.value(fb)), SW.value(fa), Fa, hfa), Equal.cong(Nat, Nat, z => Nat.add(Fa, z), SW.value(fb), Fb, hfb))), WW.low_fit(64n, Nat.add(Fa, Fb), SH.fits_mono(53n, 64n, Nat.add(Fa, Fb), {==}, f53))))