def exp_amt0

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:50

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

50# the exponent field of the implementation: 1033 - clz = 970 + j
51def exp_amt0(+j: Nat, +hj: {Nat.is_le(j, 52n) == True{} : Bool}) -> {Nat.sub(1033n, Nat.sub(63n, j)) == Nat.add(970n, j) : Nat}:
52  +r = Nat.sub(52n, j)
53  +e1 = N.sub_add(52n, j, hj)
54  +e3 = Equal.trans(Nat, Nat.add(r, Nat.add(970n, j)), Nat.add(Nat.add(970n, j), r), 1022n, N.add_comm(r, Nat.add(970n, j)), Equal.cong(Nat, Nat, z => Nat.add(970n, z), Nat.add(j, r), 52n, e1))
55  %Equal.sym(Nat, Nat.sub(63n, j), Nat.add(11n, r), sub63(j, hj)) : {Nat.sub(1033n, _) == Nat.add(970n, j) : Nat}
56  %e3 : {Nat.sub(_, r) == Nat.add(970n, j) : Nat}
57  N.add_sub_cancel(r, Nat.add(970n, j))