def big_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64isq.bend:148

import Base
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/src/math/natural.bend as M

148def big_v(+l: U32, +h: U32, +r0: U32) -> {SW.value(X.isqrt_big(WU.U64{l, h}, r0)) == M.isqrt(SW.value(WU.U64{l, h})) : Nat}:
149  +ei = Equal.cong(U32, Nat, z => v(z), X.isqrt64_fix(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))))), up64g(1n+v(U32.sub(4294967295, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))), WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))), up64_okg(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))), 4294967295), 4294967295), impl_up64(1n+v(U32.sub(4294967295, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))), WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))), X.up64_ok(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))))
150  Equal.trans(Nat, SW.value(WU.U64{X.isqrt64_fix(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))))), 0}), v(X.isqrt64_fix(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))), M.isqrt(SW.value(WU.U64{l, h})), val0(X.isqrt64_fix(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))), Equal.trans(Nat, v(X.isqrt64_fix(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))), v(up64g(1n+v(U32.sub(4294967295, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))))), WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))), up64_okg(WU.U64{l, h}, X.down64(1n+v(X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0})))), WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))), X.sq_over(WU.U64{l, h}, X.q_clamp(X.half(X.add(X.fst_q(X.div32(WU.U64{l, h}, r0)), WU.U64{r0, 0}))))), 4294967295), 4294967295)), M.isqrt(SW.value(WU.U64{l, h})), ei, big_g(1n, {==}, l, h, r0, 4294967295, {==})))