1	import Base
2	import ../../lib/nat.bend as N
3	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
4	import ../natural/arith.bend as NR
5	
6	# Exponent bookkeeping for Div.value: the spec's quotient exponent plus the
7	# rounding cut is the implementation's biased exponent minus the offset.
8	
9	def dexp_z(+dp: Nat, +P: Nat, +u: Nat, +K: Nat, +sx: Nat, +sy: Nat, +hc: {Nat.add(dp, P) == 200n : Nat}, +hb: {Nat.add(62n, u) == Nat.add(sy, P) : Nat}, +hf: {Nat.add(u, K) == Nat.add(sx, 1022n) : Nat}) -> {Nat.add(sx, Nat.add(dp, 884n)) == Nat.add(sy, K) : Nat}:
10	  +a = Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Nat.add(200n, Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(Nat.add(dp, P), Nat.add(sx, Nat.add(u, 884n))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, u)), Nat.add(Nat.add(dp, Nat.add(sx, 884n)), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(P, u)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 884n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(dp, 884n), Nat.add(dp, 884n), Equal.trans(Nat, Nat.add(dp, 884n), Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, 884n), Equal.cong(Nat, Nat, z => Nat.add(z, 884n), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), 884n), Nat.add(dp, Nat.add(0n, 884n)), Nat.add(dp, 884n), NA.add_assoc(dp, 0n, 884n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.tra
11	  +b = Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Nat.add(sx, Nat.add(u, 1084n)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(62n, u), Nat.add(u, K)), Nat.add(Nat.add(62n, u), Nat.add(sx, 1022n)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(sy, P), Nat.add(u, K)), Nat.add(Nat.add(62n, u), Nat.add(u, K)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Nat.add(Nat.add(sy, P), Nat.add(u, K)), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Nat.add(K, Nat.add(P, Nat.add(sy, Nat.add(u, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, K), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, u)), Nat.add(Nat.add(K, Nat.add(sy, 0n)), Nat.add(P, Nat.add(u, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(P, u)), Nat.add(sy, K), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, K), Nat.add(Nat.add(sy, 0n), K), Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, K), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sy, 0n), z), K, Nat.add(K, 0n), Equal.sym(Nat, Nat.add(K, 0n), K, N.add_zero(K)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(K, 0n)), Nat.add(K, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(K, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(K, 0n))), Nat.add(sy, Nat.add(K, 0n)), NA.add_assoc(sy, 0n, Nat.add(K, 0n)), Equal.cong(Nat, Nat, z => Nat.add(sy, z), Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(K, 0n)), Nat.add(K, Nat.add(0n, 0n)), Nat.add(K, 0n), NA.add_swap(0n, K, 0n), {==}))), NA.add_swap(sy, K, 0n)))), Equ
12	  +c = Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Nat.add(Nat.add(P, u), Nat.add(sy, K)), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Nat.add(Nat.add(sx, Nat.add(dp, 884n)), Nat.add(P, u)), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(dp, Nat.add(sx, 884n))), Nat.add(P, Nat.add(dp, Nat.add(sx, Nat.add(u, 884n)))), Equal.trans(Nat, Nat.add(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(sx, Nat.add(dp, 884n))), Nat.add(Nat.add(P, Nat.add(u, 0n)), Nat.add(dp, Nat.add(sx, 884n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 884n))), Nat.add(P, u), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(u, 0n)), Equal.trans(Nat, Nat.add(P, u), Nat.add(Nat.add(P, 0n), u), Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, u), P, Nat.add(P, 0n), Equal.sym(Nat, Nat.add(P, 0n), P, N.add_zero(P))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, 0n), z), u, Nat.add(u, 0n), Equal.sym(Nat, Nat.add(u, 0n), u, N.add_zero(u)))), Equal.trans(Nat, Nat.add(Nat.add(P, 0n), Nat.add(u, 0n)), Nat.add(P, Nat.add(0n, Nat.add(u, 0n))), Nat.add(P, Nat.add(u, 0n)), NA.add_assoc(P, 0n, Nat.add(u, 0n)), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, 0n), Equal.trans(Nat, Nat.add(0n, Nat.add(u, 0n)), Nat.add(u, Nat.add(0n, 0n)), Nat.add(u, 0n), NA.add_swap(0n, u, 0n), {==}))))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(P, Nat.add(u, 0n)), z), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 884n)), Nat.add(dp, Nat.add(sx, 884n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 884n))
13	  NR.add_cancel(Nat.add(P, u), Nat.add(sx, Nat.add(dp, 884n)), Nat.add(sy, K), c)
14	
15	def dexp(+E: Nat, +XX: Nat, +XY: Nat, +dp: Nat, +P: Nat, +u: Nat, +K: Nat, +sx: Nat, +sy: Nat, +EA: Nat, +EB: Nat, +e: Nat, +ha: {Nat.add(E, Nat.add(XY, 201n)) == Nat.add(XX, 3000n) : Nat}, +hc: {Nat.add(dp, P) == 200n : Nat}, +hb: {Nat.add(62n, u) == Nat.add(sy, P) : Nat}, +hf: {Nat.add(u, K) == Nat.add(sx, 1022n) : Nat}, +hEAx: {Nat.add(EA, sx) == Nat.add(XX, 2171n) : Nat}, +hEBy: {Nat.add(EB, sy) == Nat.add(XY, 2171n) : Nat}, +hd: {Nat.add(e, EB) == Nat.add(EA, Nat.add(4096n, K)) : Nat}) -> {Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n) == e : Nat}:
16	  +z = dexp_z(dp, P, u, K, sx, sy, hc, hb, hf)
17	  +lz = Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Nat.add(XX, Nat.add(Nat.add(sy, K), 6267n)), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(Nat.add(sx, Nat.add(dp, 884n)), 6267n)), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Nat.add(XX, Nat.add(dp, Nat.add(sx, 7151n))), Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(XX, 0n), Nat.add(dp, Nat.add(sx, 7151n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(sx, Nat.add(dp, 7151n))), XX, Nat.add(XX, 0n), Equal.sym(Nat, Nat.add(XX, 0n), XX, N.add_zero(XX))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(XX, 0n), z), Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(dp, Nat.add(sx, 7151n)), Equal.trans(Nat, Nat.add(sx, Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Nat.add(Nat.add(sx, 0n), Nat.add(dp, 7151n)), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(dp, 7151n)), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sx, 0n), z), Nat.add(dp, 7151n), Nat.add(dp, 7151n), Equal.trans(Nat, Nat.add(dp, 7151n), Nat.add(Nat.add(dp, 0n), 7151n), Nat.add(dp, 7151n), Equal.cong(Nat, Nat, z => Nat.add(z, 7151n), dp, Nat.add(dp, 0n), Equal.sym(Nat, Nat.add(dp, 0n), dp, N.add_zero(dp))), Equal.trans(Nat, Nat.add(Nat.add(dp, 0n), 7151n), Nat.add(dp, Nat.add(0n, 7151n)), Nat.add(dp, 7151n), NA.add_assoc(dp, 0n, 7151n), {==})))), Equal.trans(Nat, Nat.add(Nat.add(
18	  +lh = Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Nat.add(Nat.add(XX, 3000n), Nat.add(sx, Nat.add(dp, 4151n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(E, Nat.add(XY, 201n)), Nat.add(sx, Nat.add(dp, 4151n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Nat.add(Nat.add(XY, 2171n), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Nat.add(Nat.add(EB, sy), Nat.add(E, Nat.add(sx, Nat.add(dp, 2181n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Nat.add(E, Nat.add(EB, Nat.add(dp, Nat.add(sx, Nat.add(sy, 2181n))))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(E, Nat.add(EB, Nat.add(dp, 2181n)))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(sy, sx), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.a
19	  +rh = Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Nat.add(Nat.add(XX, 2171n), Nat.add(sy, Nat.add(K, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Nat.add(Nat.add(EA, sx), Nat.add(sy, Nat.add(K, 4096n))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Nat.add(Nat.add(EA, Nat.add(4096n, K)), Nat.add(sy, sx)), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Nat.add(Nat.add(e, EB), Nat.add(sy, sx)), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(e, 0n))), Nat.add(EB, Nat.add(e, Nat.add(sx, Nat.add(sy, 0n)))), Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, e)), Nat.add(Nat.add(sx, Nat.add(sy, 0n)), Nat.add(EB, Nat.add(e, 0n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.add(EB, e)), Nat.add(sy, sx), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(sy, sx), Nat.add(Nat.add(sy, 0n), sx), Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Equal.cong(Nat, Nat, z => Nat.add(z, sx), sy, Nat.add(sy, 0n), Equal.sym(Nat, Nat.add(sy, 0n), sy, N.add_zero(sy))), Equal.cong(Nat, Nat, z => Nat.add(Nat.add(sy, 0n), z), sx, Nat.add(sx, 0n), Equal.sym(Nat, Nat.add(sx, 0n), sx, N.add_zero(sx)))), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(sx, 0n)), Nat.add(sx, Nat.add(sy, 0n)), Equal.trans(Nat, Nat.add(Nat.add(sy, 0n), Nat.add(sx, 0n)), Nat.add(sy, Nat.add(0n, Nat.add(sx, 0n))), Nat.add(s
20	  +all = Equal.trans(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n))), Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), lh, Equal.trans(Nat, Nat.add(XX, Nat.add(sx, Nat.add(dp, 7151n))), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), lz, Equal.sym(Nat, Nat.add(Nat.add(sy, sx), Nat.add(EB, e)), Nat.add(XX, Nat.add(sy, Nat.add(K, 6267n))), rh)))
21	  +c1 = NR.add_cancel(Nat.add(sy, sx), Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(EB, e), all)
22	  +c2 = Equal.trans(Nat, Nat.add(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n)), Nat.add(EB, e), Nat.add(EB, e), c1, {==})
23	  NR.add_cancel(EB, Nat.add(Nat.add(E, Nat.add(1n, dp)), 2180n), e, c1)