F64bits.xstep: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as F64bits
Lines 63-89 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&start_line=63&end_line=89

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/proofs/lib/lemmas/spec/numeric.bend as S
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/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

# flipping the top bit
def xstep(+q: Nat, +b: Bool, +t: Word(1n+q), +ih: {S.unsigned(1n+q, Word.xor(1n+q, t, WD.pw(1n+q, q))) == Nat.add(C.low(q, S.unsigned(1n+q, t)), C.shift(q, Nat.sub(1n, C.high(q, S.unsigned(1n+q, t))))) : Nat}) -> {S.unsigned(2n+q, Word.xor(2n+q, WCon{b, t}, WD.pw(2n+q, 1n+q))) == Nat.add(C.low(1n+q, S.unsigned(2n+q, WCon{b, t})), C.shift(1n+q, Nat.sub(1n, C.high(1n+q, S.unsigned(2n+q, WCon{b, t}))))) : Nat}:
  match b:
    case True{}:
      +T = S.unsigned(1n+q, t)
      +X0 = S.unsigned(1n+q, Word.xor(1n+q, t, WD.pw(1n+q, q)))
      +lq = C.low(q, T)
      +sq = C.shift(q, Nat.sub(1n, C.high(q, T)))
      +U0 = Nat.add(1n, Nat.double(T))
      +e1 = Equal.cong(Nat, Nat, z => 1n+Nat.double(z), X0, Nat.add(lq, sq), ih)
      +e2 = Equal.cong(Nat, Nat, z => 1n+z, Nat.double(Nat.add(lq, sq)), Nat.add(Nat.double(lq), Nat.double(sq)), NA.double_add(lq, sq))
      +r1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), C.bit(U0), 1n, WW.bit_dbl(1n, T))
      +r2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(1n, Nat.double(C.low(q, z))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, z))))), C.half(U0), T, WW.half_dbl(1n, T))
      +r = Equal.trans(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(1n, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(1n, Nat.double(lq)), Nat.double(sq)), r1, r2)
      Equal.trans(Nat, 1n+Nat.double(X0), 1n+Nat.double(Nat.add(lq, sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e1, Equal.trans(Nat, 1n+Nat.double(Nat.add(lq, sq)), Nat.add(Nat.add(1n, Nat.double(lq)), Nat.double(sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e2, Equal.sym(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(1n, Nat.double(lq)), Nat.double(sq)), r)))
    case False{}:
      +T = S.unsigned(1n+q, t)
      +X0 = S.unsigned(1n+q, Word.xor(1n+q, t, WD.pw(1n+q, q)))
      +lq = C.low(q, T)
      +sq = C.shift(q, Nat.sub(1n, C.high(q, T)))
      +U0 = Nat.add(0n, Nat.double(T))
      +e1 = Equal.cong(Nat, Nat, z => Nat.double(z), X0, Nat.add(lq, sq), ih)
      +e2 = NA.double_add(lq, sq)
      +r1 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(z, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), C.bit(U0), 0n, WW.bit_dbl(0n, T))
      +r2 = Equal.cong(Nat, Nat, z => Nat.add(Nat.add(0n, Nat.double(C.low(q, z))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, z))))), C.half(U0), T, WW.half_dbl(0n, T))
      +r = Equal.trans(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.add(0n, Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.double(lq), Nat.double(sq)), r1, r2)
      Equal.trans(Nat, Nat.double(X0), Nat.double(Nat.add(lq, sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e1, Equal.trans(Nat, Nat.double(Nat.add(lq, sq)), Nat.add(Nat.double(lq), Nat.double(sq)), Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), e2, Equal.sym(Nat, Nat.add(Nat.add(C.bit(U0), Nat.double(C.low(q, C.half(U0)))), Nat.double(C.shift(q, Nat.sub(1n, C.high(q, C.half(U0)))))), Nat.add(Nat.double(lq), Nat.double(sq)), r)))

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.xor
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=unsigned
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend&name=pw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=bit_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=half_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=bit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=half
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift