def per1

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64next.bend:210

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/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

210# pat + 1 still fits 63 bits unless x is a NaN
211def per1(+x: F.F64) -> {Nat.add(SF.pat(x), 1n) == Nat.add(Nat.add(SF.frac(x), 1n), C.shift(52n, SF.efield(x))) : Nat}:
212  +Fr = SF.frac(x)
213  +S = C.shift(52n, SF.efield(x))
214  +ea = NA.add_assoc(Fr, S, 1n)
215  +ec = Equal.cong(Nat, Nat, t => Nat.add(Fr, t), Nat.add(S, 1n), Nat.add(1n, S), NA.add_comm(S, 1n))
216  +eb = Equal.sym(Nat, Nat.add(Nat.add(Fr, 1n), S), Nat.add(Fr, Nat.add(1n, S)), NA.add_assoc(Fr, 1n, S))
217  Equal.trans(Nat, Nat.add(SF.pat(x), 1n), Nat.add(Fr, Nat.add(S, 1n)), Nat.add(Nat.add(Fr, 1n), S), ea, Equal.trans(Nat, Nat.add(Fr, Nat.add(S, 1n)), Nat.add(Fr, Nat.add(1n, S)), Nat.add(Nat.add(Fr, 1n), S), ec, eb))