def half_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rint.bend:122

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/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/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/f64light.bend as FL

122# 2^(k-1) as a word
123def half_v(+j: Nat, +hb: {Nat.is_lt(1n+j, 64n) == True{} : Bool}) -> {SW.value(X.shl(WU.U64{1, 0}, Nat.sub(1n+j, 1n))) == C.shift(j, 1n) : Nat}:
124  +hj = N.lt_trans(j, 1n+j, 64n, N.lt_succ(j), hb)
125  +hl = N.lt_le(1n+j, 64n, hb)
126  +hj1 = L.subst(Nat, t => {Nat.is_le(t, 64n) == True{} : Bool}, 1n+j, Nat.add(j, 1n), Equal.sym(Nat, Nat.add(j, 1n), 1n+j, Equal.trans(Nat, Nat.add(j, 1n), 1n+Nat.add(j, 0n), 1n+j, N.add_succ(j, 0n), Equal.cong(Nat, Nat, t => 1n+t, Nat.add(j, 0n), j, N.add_zero(j)))), hl)
127  +e = FL.shl_v(WU.U64{1, 0}, j, 1n, hj, hj1, {==})
128  L.subst(Nat, t => {SW.value(X.shl(WU.U64{1, 0}, t)) == C.shift(j, 1n) : Nat}, j, Nat.sub(j, 0n), Equal.sym(Nat, Nat.sub(j, 0n), j, N.sub_zero(j)), e)