def opat

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

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/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

284def opat(+s: Bool, +P: Nat) -> {SF.of_pat(s, P) == FR.bits(s, P) : F.F64}:
285  Equal.trans(F.F64, SF.of_pat(s, P), FR.bits(s, Nat.add(C.low(52n, P), C.shift(52n, C.high(52n, P)))), FR.bits(s, P), FR.enc_bits(s, C.high(52n, P), C.low(52n, P)), Equal.cong(Nat, F.F64, t => FR.bits(s, t), Nat.add(C.low(52n, P), C.shift(52n, C.high(52n, P))), P, Equal.sym(Nat, P, Nat.add(C.low(52n, P), C.shift(52n, C.high(52n, P))), WW.low_high(52n, P))))