def ame0

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

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/f64.bend as SF
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/f64.bend as F
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/lib/nat.bend as N
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/math/typed/w64sh.bend as SH
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

100# addMags, both subnormal: pack(s, 0, fa + fb)
101def ame0(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +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}) -> {F.pack(s, 0n, X.add(fa, fb)) == SF.round(s, Nat.add(Fa, Fb), 1926n) : F.F64}:
102  +ev = addv2(fa, fb, Fa, Fb, hfa, hfb, hFa, hFb)
103  +f53 = FR.fits_add1(52n, Fa, Fb, hFa, hFb)
104  +hn = L.subst(Nat, z => {C.fits(63n, Nat.add(z, C.shift(52n, 0n))) == True{} : Bool}, Nat.add(Fa, Fb), SW.value(X.add(fa, fb)), Equal.sym(Nat, SW.value(X.add(fa, fb)), Nat.add(Fa, Fb), ev), L.subst(Nat, z => {C.fits(63n, z) == True{} : Bool}, Nat.add(Fa, Fb), Nat.add(Nat.add(Fa, Fb), 0n), Equal.sym(Nat, Nat.add(Nat.add(Fa, Fb), 0n), Nat.add(Fa, Fb), N.add_zero(Nat.add(Fa, Fb))), SH.fits_mono(53n, 63n, Nat.add(Fa, Fb), {==}, f53)))
105  +i1 = FR.pack_v(s, 0n, {==}, X.add(fa, fb), hn)
106  +i2 = Equal.cong(Nat, F.F64, z => FR.bits(s, Nat.add(z, C.shift(52n, 0n))), SW.value(X.add(fa, fb)), Nat.add(Fa, Fb), ev)
107  Equal.trans(F.F64, F.pack(s, 0n, X.add(fa, fb)), FR.bits(s, Nat.add(Nat.add(Fa, Fb), C.shift(52n, 0n))), SF.round(s, Nat.add(Fa, Fb), 1926n), Equal.trans(F.F64, F.pack(s, 0n, X.add(fa, fb)), FR.bits(s, Nat.add(SW.value(X.add(fa, fb)), C.shift(52n, 0n))), FR.bits(s, Nat.add(Nat.add(Fa, Fb), C.shift(52n, 0n))), i1, i2), Equal.sym(F.F64, SF.round(s, Nat.add(Fa, Fb), 1926n), FR.bits(s, Nat.add(Nat.add(Fa, Fb), C.shift(52n, 0n))), r1926(one, h1, s, Nat.add(Fa, Fb), f53, 1926n, {==}, Nat.is_eq(Nat.add(Fa, Fb), 0n), {==})))