Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
This file is part of the Flocq formalization of floating-point arithmetic in Coq: http://flocq.gforge.inria.fr/
Copyright (C) 2009-2018 Sylvie Boldo
Copyright (C) 2009-2018 Guillaume Melquiond
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Rounding to nearest, ties to even: existence, unicity...

Require Import Raux Defs Round_pred Generic_fmt Float_prop Ulp.

Notation ZnearestE := (Znearest (fun x => negb (Z.even x))).

Section Fcore_rnd_NE.

Variable beta : radix.

Notation bpow e := (bpow beta e).

Variable fexp : Z -> Z.

Context { valid_exp : Valid_exp fexp }.

Notation format := (generic_format beta fexp).
Notation canonical := (canonical beta fexp).

Definition NE_prop (_ : R) f :=
  exists g : float beta, f = F2R g /\ canonical g /\ Z.even (Fnum g) = true.

Definition Rnd_NE_pt :=
  Rnd_NG_pt format NE_prop.

Definition DN_UP_parity_pos_prop :=
  forall x xd xu,
  (0 < x)%R ->
  ~ format x ->
  canonical xd ->
  canonical xu ->
  F2R xd = round beta fexp Zfloor x ->
  F2R xu = round beta fexp Zceil x ->
  Z.even (Fnum xu) = negb (Z.even (Fnum xd)).

Definition DN_UP_parity_prop :=
  forall x xd xu,
  ~ format x ->
  canonical xd ->
  canonical xu ->
  F2R xd = round beta fexp Zfloor x ->
  F2R xu = round beta fexp Zceil x ->
  Z.even (Fnum xu) = negb (Z.even (Fnum xd)).

beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp

DN_UP_parity_pos_prop -> DN_UP_parity_prop
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp

DN_UP_parity_pos_prop -> DN_UP_parity_prop
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 < x)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:0%R = x
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
(* . *)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:0%R = x

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:0%R = x

format x
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:0%R = x

format 0
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
(* . *)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R

(0 < - x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R

(- - x < - 0)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
xd, xu:float beta
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed:Z
xu:float beta
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical xu
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even (Fnum xu) = negb (Z.even (Fnum {| Fnum := md; Fexp := ed |}))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even (Fnum {| Fnum := mu; Fexp := eu |}) = negb (Z.even (Fnum {| Fnum := md; Fexp := ed |}))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even mu = negb (Z.even md)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

negb (negb (Z.even mu)) = negb (Z.even md)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

negb (Z.even mu) = Z.even md
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even md = negb (Z.even mu)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even (- md) = negb (Z.even (- mu))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

Z.even (Fnum {| Fnum := - md; Fexp := ed |}) = negb (Z.even (Fnum {| Fnum := - mu; Fexp := eu |}))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

~ format (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - mu; Fexp := eu |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - md; Fexp := ed |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
H:format (- x)

False
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - mu; Fexp := eu |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - md; Fexp := ed |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
H:format (- x)

format x
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - mu; Fexp := eu |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - md; Fexp := ed |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
H:format (- x)

format (- - x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - mu; Fexp := eu |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - md; Fexp := ed |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

canonical {| Fnum := - mu; Fexp := eu |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
canonical {| Fnum := - md; Fexp := ed |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

canonical {| Fnum := - md; Fexp := ed |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

F2R {| Fnum := - mu; Fexp := eu |} = round beta fexp Zfloor (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

(- F2R {| Fnum := mu; Fexp := eu |})%R = (- round beta fexp Zceil x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R
F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

F2R {| Fnum := - md; Fexp := ed |} = round beta fexp Zceil (- x)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
Hpos:DN_UP_parity_pos_prop
x:R
md, ed, mu, eu:Z
Hfx:~ format x
Hd:canonical {| Fnum := md; Fexp := ed |}
Hu:canonical {| Fnum := mu; Fexp := eu |}
Hxd:F2R {| Fnum := md; Fexp := ed |} = round beta fexp Zfloor x
Hxu:F2R {| Fnum := mu; Fexp := eu |} = round beta fexp Zceil x
Hx:(0 > x)%R
Hx':(0 < - x)%R

(- F2R {| Fnum := md; Fexp := ed |})%R = (- round beta fexp Zfloor x)%R
now apply f_equal. Qed. Class Exists_NE := exists_NE : Z.even beta = false \/ forall e, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e). Context { exists_NE_ : Exists_NE }.
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE

DN_UP_parity_pos_prop
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE

DN_UP_parity_pos_prop
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:x <> 0%R -> (bpow (ex - 1) <= Rabs x < bpow ex)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R

(bpow (ex - 1) <= Rabs x < bpow ex)%R -> Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa, Hex:(bpow (ex - 1) <= Rabs x < bpow ex)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
(* small x *)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z

Fnum xd = 0%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z

F2R {| Fnum := Fnum xd; Fexp := Fexp xd |} = 0%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z

F2R xd = R0
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z

round beta fexp Zfloor x = R0
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

canonical {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
F2R xu = F2R {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

(fexp ex + 1)%Z = mag beta (F2R {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |})
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
F2R xu = F2R {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

(fexp ex + 1)%Z = mag beta (F2R {| Fnum := 1; Fexp := fexp ex |})
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
F2R xu = F2R {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
F2R xu = F2R {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

F2R xu = F2R {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

F2R xu = F2R {| Fnum := 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

F2R xu = bpow (fexp ex)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

bpow (fexp ex) = F2R xu
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

bpow (fexp ex) = round beta fexp Zceil x
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

round beta fexp Zceil x = bpow (fexp ex)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z

(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}

Z.even (Fnum {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}) = negb (Z.even 0)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}

Z.even (Fnum {| Fnum := beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}) = negb (Z.even 0)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}

Z.even (beta ^ (fexp ex - fexp (fexp ex + 1))) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:Z.even beta = false

Z.even (beta ^ (fexp ex - fexp (fexp ex + 1))) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)
Z.even (beta ^ (fexp ex - fexp (fexp ex + 1))) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:Z.even beta = false

(0 <= fexp ex - fexp (fexp ex + 1))%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)
Z.even (beta ^ (fexp ex - fexp (fexp ex + 1))) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:Z.even beta = false

(fexp (fexp ex + 1) <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)
Z.even (beta ^ (fexp ex - fexp (fexp ex + 1))) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)

Z.even (beta ^ (fexp ex - fexp (fexp ex + 1))) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)

Z.even (beta ^ (fexp ex - fexp ex)) = false
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)
(ex <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(ex <= fexp ex)%Z
Hd3:Fnum xd = 0%Z
Hu3:xu = {| Fnum := 1 * beta ^ (fexp ex - fexp (fexp ex + 1)); Fexp := fexp (fexp ex + 1) |}
H:forall e : Z, ((fexp e < e)%Z -> (fexp (e + 1) < e)%Z) /\ ((e <= fexp e)%Z -> fexp (fexp e + 1) = fexp e)

(ex <= fexp ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
(* large x *)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(bpow (ex - 1) <= F2R xd < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(bpow (ex - 1) <= round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(bpow (ex - 1) <= round beta fexp Zfloor x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

format (bpow (ex - 1))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(bpow (ex - 1) <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(fexp (ex - 1 + 1) <= ex - 1)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(bpow (ex - 1) <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(fexp ex <= ex - 1)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(bpow (ex - 1) <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(bpow (ex - 1) <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(round beta fexp Zfloor x < bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(round beta fexp Zfloor x <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(0 <= F2R xd)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(0 <= round beta fexp Zfloor x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

format 0
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z

(0 <= x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z

F2R xu = (F2R xd + ulp beta fexp x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z

round beta fexp Zceil x = (round beta fexp Zfloor x + ulp beta fexp x)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex < F2R xu)%R

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
(* - xu > bpow ex *)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex < F2R xu)%R

(F2R xu <= bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex < F2R xu)%R

(round beta fexp Zceil x <= bpow ex)%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
(* - xu = bpow ex *)
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

canonical {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
F2R xu = F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

(ex + 1)%Z = mag beta (F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |})
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
F2R xu = F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

(ex + 1)%Z = mag beta (F2R {| Fnum := 1; Fexp := ex |})
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
(fexp (ex + 1) <= ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
F2R xu = F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

(fexp (ex + 1) <= ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
F2R xu = F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

F2R xu = F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

bpow ex = F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

F2R {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |} = bpow ex
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

F2R {| Fnum := 1; Fexp := ex |} = bpow ex
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
(fexp (ex + 1) <= ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu

(fexp (ex + 1) <= ex)%Z
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Hd3:xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

F2R xd = F2R {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
H:F2R xd = F2R {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Hd3:xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

(IZR (Fnum xd) * bpow (Fexp xd))%R = (IZR (Fnum {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}) * bpow (Fexp {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
H:F2R xd = F2R {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Hd3:xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

(IZR (Fnum xd) * bpow (Fexp xd))%R = (IZR (beta ^ (ex - fexp ex) - 1) * bpow (fexp ex))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
H:F2R xd = F2R {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Hd3:xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

(IZR (Fnum xd) * bpow (Fexp xd))%R = ((IZR (beta ^ (ex - fexp ex)) - 1) * bpow (fexp ex))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
H:F2R xd = F2R {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}
Hd3:xd = {| Fnum := beta ^ (ex - fexp ex) - 1; Fexp := fexp ex |}
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:(bpow ex > F2R xu)%R
Z.even (Fnum xu) = negb (Z.even (Fnum xd))
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta
H0x:(0 < x)%R
Hfx:~ format x
Hd:canonical xd
Hu:canonical xu
Hxd:F2R xd = round beta fexp Zfloor x
Hxu:F2R xu = round beta fexp Zceil x
ex:Z
Hexa:(bpow (ex - 1) <= Rabs x < bpow ex)%R
Hex:(bpow (ex - 1) <= x < bpow ex)%R
Hxe:(fexp ex < ex)%Z
Hd4:(bpow (ex - 1) <= Rabs (F2R xd) < bpow ex)%R
Hxe2:(fexp (ex + 1) <= ex)%Z
Hud:F2R xu = (F2R xd + ulp beta fexp x)%R
Hu2:bpow ex = F2R xu
Hu3:xu = {| Fnum := 1 * beta ^ (ex - fexp (ex + 1)); Fexp := fexp (ex + 1) |}

(IZR (Fnum xd) * bpow (Fexp xd))%R = ((IZR (beta ^ (ex - fexp ex)) + - (1)) * bpow (fexp ex))%R
beta:radix
fexp:Z -> Z
valid_exp:Valid_exp fexp
exists_NE_:Exists_NE
x:R
xd, xu:float beta