def bits_g

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64misc.bend:63

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
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/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC

63def bits_g(+l: U32, +h: U32) -> {Nat.add(v(l), C.shift(32n, v(h))) == Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, SF.b2n(SF.sign(F.Bits{l, h})))) : Nat}:
64  +H = v(h)
65  +Lo = C.low(31n, H)
66  +Hh = C.high(31n, H)
67  +e1 = Equal.cong(Nat, Nat, t => Nat.add(v(l), C.shift(32n, t)), H, Nat.add(Lo, C.shift(31n, Hh)), WW.low_high(31n, H))
68  +e2 = Equal.cong(Nat, Nat, t => Nat.add(v(l), t), C.shift(32n, Nat.add(Lo, C.shift(31n, Hh))), Nat.add(C.shift(32n, Lo), C.shift(32n, C.shift(31n, Hh))), WW.shift_add(32n, Lo, C.shift(31n, Hh)))
69  +e3 = Equal.cong(Nat, Nat, t => Nat.add(v(l), Nat.add(C.shift(32n, Lo), t)), C.shift(32n, C.shift(31n, Hh)), C.shift(63n, Hh), Equal.sym(Nat, C.shift(63n, Hh), C.shift(32n, C.shift(31n, Hh)), WW.shift_comp(32n, 31n, Hh)))
70  +e4 = Equal.sym(Nat, Nat.add(Nat.add(v(l), C.shift(32n, Lo)), C.shift(63n, Hh)), Nat.add(v(l), Nat.add(C.shift(32n, Lo), C.shift(63n, Hh))), NA.add_assoc(v(l), C.shift(32n, Lo), C.shift(63n, Hh)))
71  +e5 = Equal.cong(Nat, Nat, t => Nat.add(t, C.shift(63n, Hh)), Nat.add(v(l), C.shift(32n, Lo)), SF.pat(F.Bits{l, h}), FC.magQ(l, h))
72  +e6 = Equal.cong(Nat, Nat, t => Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, t)), Hh, SF.b2n(SF.sign(F.Bits{l, h})), FB.bit_c(Hh, FB.half0(h)))
73  +a1 = Nat.add(v(l), C.shift(32n, Nat.add(Lo, C.shift(31n, Hh))))
74  +a2 = Nat.add(v(l), Nat.add(C.shift(32n, Lo), C.shift(32n, C.shift(31n, Hh))))
75  +a3 = Nat.add(v(l), Nat.add(C.shift(32n, Lo), C.shift(63n, Hh)))
76  +a4 = Nat.add(Nat.add(v(l), C.shift(32n, Lo)), C.shift(63n, Hh))
77  +a5 = Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, Hh))
78  +a6 = Nat.add(SF.pat(F.Bits{l, h}), C.shift(63n, SF.b2n(SF.sign(F.Bits{l, h}))))
79  Equal.trans(Nat, Nat.add(v(l), C.shift(32n, H)), a1, a6, e1, Equal.trans(Nat, a1, a2, a6, e2, Equal.trans(Nat, a2, a3, a6, e3, Equal.trans(Nat, a3, a4, a6, e4, Equal.trans(Nat, a4, a5, a6, e5, e6)))))