;; GENERATED BY `fpconst`. DO NOT EDIT!!!
(spec (min_fp_value signed in out)
(provide
(=> (and (= in #x20) (= signed true) (= out #x08)) (= result #x00000000c3010000))
(=> (and (= in #x20) (= signed true) (= out #x10)) (= result #x00000000c7000100))
(=> (and (= in #x20) (= signed true) (= out #x20)) (= result #x00000000cf000000))
(=> (and (= in #x20) (= signed true) (= out #x40)) (= result #x00000000df000000))
(=> (and (= in #x20) (= signed false) (= out #x08)) (= result #x00000000bf800000))
(=> (and (= in #x20) (= signed false) (= out #x10)) (= result #x00000000bf800000))
(=> (and (= in #x20) (= signed false) (= out #x20)) (= result #x00000000bf800000))
(=> (and (= in #x20) (= signed false) (= out #x40)) (= result #x00000000bf800000))
(=> (and (= in #x40) (= signed true) (= out #x08)) (= result #xc060200000000000))
(=> (and (= in #x40) (= signed true) (= out #x10)) (= result #xc0e0002000000000))
(=> (and (= in #x40) (= signed true) (= out #x20)) (= result #xc1e0000000200000))
(=> (and (= in #x40) (= signed true) (= out #x40)) (= result #xc3e0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x08)) (= result #xbff0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x10)) (= result #xbff0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x20)) (= result #xbff0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x40)) (= result #xbff0000000000000))
)
(require (or
(and (= in #x20) (= signed true) (= out #x08))
(and (= in #x20) (= signed true) (= out #x10))
(and (= in #x20) (= signed true) (= out #x20))
(and (= in #x20) (= signed true) (= out #x40))
(and (= in #x20) (= signed false) (= out #x08))
(and (= in #x20) (= signed false) (= out #x10))
(and (= in #x20) (= signed false) (= out #x20))
(and (= in #x20) (= signed false) (= out #x40))
(and (= in #x40) (= signed true) (= out #x08))
(and (= in #x40) (= signed true) (= out #x10))
(and (= in #x40) (= signed true) (= out #x20))
(and (= in #x40) (= signed true) (= out #x40))
(and (= in #x40) (= signed false) (= out #x08))
(and (= in #x40) (= signed false) (= out #x10))
(and (= in #x40) (= signed false) (= out #x20))
(and (= in #x40) (= signed false) (= out #x40))
))
)
(spec (max_fp_value signed in out)
(provide
(=> (and (= in #x20) (= signed true) (= out #x08)) (= result #x0000000043000000))
(=> (and (= in #x20) (= signed true) (= out #x10)) (= result #x0000000047000000))
(=> (and (= in #x20) (= signed true) (= out #x20)) (= result #x000000004f000000))
(=> (and (= in #x20) (= signed true) (= out #x40)) (= result #x000000005f000000))
(=> (and (= in #x20) (= signed false) (= out #x08)) (= result #x0000000043800000))
(=> (and (= in #x20) (= signed false) (= out #x10)) (= result #x0000000047800000))
(=> (and (= in #x20) (= signed false) (= out #x20)) (= result #x000000004f800000))
(=> (and (= in #x20) (= signed false) (= out #x40)) (= result #x000000005f800000))
(=> (and (= in #x40) (= signed true) (= out #x08)) (= result #x4060000000000000))
(=> (and (= in #x40) (= signed true) (= out #x10)) (= result #x40e0000000000000))
(=> (and (= in #x40) (= signed true) (= out #x20)) (= result #x41e0000000000000))
(=> (and (= in #x40) (= signed true) (= out #x40)) (= result #x43e0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x08)) (= result #x4070000000000000))
(=> (and (= in #x40) (= signed false) (= out #x10)) (= result #x40f0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x20)) (= result #x41f0000000000000))
(=> (and (= in #x40) (= signed false) (= out #x40)) (= result #x43f0000000000000))
)
(require (or
(and (= in #x20) (= signed true) (= out #x08))
(and (= in #x20) (= signed true) (= out #x10))
(and (= in #x20) (= signed true) (= out #x20))
(and (= in #x20) (= signed true) (= out #x40))
(and (= in #x20) (= signed false) (= out #x08))
(and (= in #x20) (= signed false) (= out #x10))
(and (= in #x20) (= signed false) (= out #x20))
(and (= in #x20) (= signed false) (= out #x40))
(and (= in #x40) (= signed true) (= out #x08))
(and (= in #x40) (= signed true) (= out #x10))
(and (= in #x40) (= signed true) (= out #x20))
(and (= in #x40) (= signed true) (= out #x40))
(and (= in #x40) (= signed false) (= out #x08))
(and (= in #x40) (= signed false) (= out #x10))
(and (= in #x40) (= signed false) (= out #x20))
(and (= in #x40) (= signed false) (= out #x40))
))
)