diff --git a/.ocamlformat b/.ocamlformat
index 8fa71c162ea3feebcc61fc98509325cc21d2c39f..d4d1b6a3629ffc0c4e4db95826f2257466a7e5d2 100644
--- a/.ocamlformat
+++ b/.ocamlformat
@@ -1 +1,4 @@
version=0.19.0
+exp-grouping=preserve
+if-then-else=keyword-first
+max-indent=2
diff --git a/config/provers_autodetection.conf b/config/caisar.conf
similarity index 100%
rename from config/provers_autodetection.conf
rename to config/caisar.conf
diff --git a/config/dune b/config/dune
index 1aabdf75ad87b38d9be62f9e82b4d5859a2f7a81..2599259423220dce7e9bed4a2f48208a45d25fc7 100644
--- a/config/dune
+++ b/config/dune
@@ -1,4 +1,4 @@
(install
(section (site (caisar config)))
- (files provers_autodetection.conf)
+ (files caisar.conf)
(package caisar))
diff --git a/dune-project b/dune-project
index 610e405cc8bb2069908819f343798e4d909bb84b..7f51a78afd27666dcab27405f5cba6215f63bfcb 100644
--- a/dune-project
+++ b/dune-project
@@ -27,7 +27,10 @@
(ppx_deriving_yojson (>= 3.6.1))
(csv (>= 2.4))
)
- (sites (share stdlib)(share config))
+ (sites
+ (share stdlib)
+ (share config)
+ )
)
(package
diff --git a/lib/nnet/dune b/lib/nnet/dune
index fb2c5ec74be4294d311033bf92eed89bf913e5da..c6303823209277875d7941fc93eb07b3fd69a643 100644
--- a/lib/nnet/dune
+++ b/lib/nnet/dune
@@ -1,5 +1,5 @@
(library
- (name nnet)
+ (name nnet)
(public_name nnet)
(libraries base csv)
(synopsis "NNet parser"))
diff --git a/lib/nnet/nnet.ml b/lib/nnet/nnet.ml
index 8b626b36d2000e4ad99f078616ce80c0d70d9523..3ef39126ee3d41b1568e7063189fdd1f1f2d54f9 100644
--- a/lib/nnet/nnet.ml
+++ b/lib/nnet/nnet.ml
@@ -42,24 +42,24 @@ let skip_nnet_header filename in_channel =
try
while true do
let line = Stdlib.input_line in_channel in
- if not (Str.string_match (Str.regexp "//") line 0) then
- raise End_of_header
+ if not (Str.string_match (Str.regexp "//") line 0)
+ then raise End_of_header
else pos_in := Stdlib.pos_in in_channel
done;
assert false
with
| End_of_header ->
- (* At this point we have read one line past the header part: seek back. *)
- Stdlib.seek_in in_channel !pos_in;
- Ok ()
+ (* At this point we have read one line past the header part: seek back. *)
+ Stdlib.seek_in in_channel !pos_in;
+ Ok ()
| End_of_file ->
- Error (Format.sprintf "NNet model not found in file `%s'." filename)
+ Error (Format.sprintf "NNet model not found in file `%s'." filename)
(* Retrieve number of layers, inputs, outputs and maximum layer size. *)
let handle_nnet_basic_info in_channel =
match handle_nnet_line ~f:Int.of_string in_channel with
| [ n_layers; n_inputs; n_outputs; max_layer_size ] ->
- Ok (n_layers, n_inputs, n_outputs, max_layer_size)
+ Ok (n_layers, n_inputs, n_outputs, max_layer_size)
| _ -> nnet_format_error "second"
| exception End_of_file -> nnet_format_error "second"
@@ -67,7 +67,8 @@ let handle_nnet_basic_info in_channel =
let handle_nnet_layer_sizes n_layers in_channel =
try
let layer_sizes = handle_nnet_line ~f:Int.of_string in_channel in
- if List.length layer_sizes = n_layers + 1 then Ok layer_sizes
+ if List.length layer_sizes = n_layers + 1
+ then Ok layer_sizes
else nnet_format_error "third"
with End_of_file -> nnet_format_error "third"
@@ -82,7 +83,8 @@ let handle_nnet_unused_flag in_channel =
let handle_nnet_min_input_values n_inputs in_channel =
try
let min_input_values = handle_nnet_line ~f:Float.of_string in_channel in
- if List.length min_input_values = n_inputs then Ok min_input_values
+ if List.length min_input_values = n_inputs
+ then Ok min_input_values
else nnet_format_error "fifth"
with End_of_file -> nnet_format_error "fifth"
@@ -90,7 +92,8 @@ let handle_nnet_min_input_values n_inputs in_channel =
let handle_nnet_max_input_values n_inputs in_channel =
try
let max_input_values = handle_nnet_line ~f:Float.of_string in_channel in
- if List.length max_input_values = n_inputs then Ok max_input_values
+ if List.length max_input_values = n_inputs
+ then Ok max_input_values
else nnet_format_error "sixth"
with End_of_file -> nnet_format_error "sixth"
@@ -98,7 +101,8 @@ let handle_nnet_max_input_values n_inputs in_channel =
let handle_nnet_mean_values n_inputs in_channel =
try
let mean_values = handle_nnet_line ~f:Float.of_string in_channel in
- if List.length mean_values = n_inputs + 1 then
+ if List.length mean_values = n_inputs + 1
+ then
let mean_input_values, mean_output_value =
List.split_n mean_values n_inputs
in
@@ -110,7 +114,8 @@ let handle_nnet_mean_values n_inputs in_channel =
let handle_nnet_range_values n_inputs in_channel =
try
let range_values = handle_nnet_line ~f:Float.of_string in_channel in
- if List.length range_values = n_inputs + 1 then
+ if List.length range_values = n_inputs + 1
+ then
let range_input_values, range_output_value =
List.split_n range_values n_inputs
in
diff --git a/lib/nnet/nnet.mli b/lib/nnet/nnet.mli
index a1b5076fefaccfcea806f896708b3d48260d0eeb..437803c8e1bd9c10ace5b2157ef81048dc7005b1 100644
--- a/lib/nnet/nnet.mli
+++ b/lib/nnet/nnet.mli
@@ -13,9 +13,9 @@ type t = private {
min_input_values : float list; (** Minimum values of inputs. *)
max_input_values : float list; (** Maximum values of inputs. *)
mean_values : float list * float;
- (** Mean values of inputs and one value for all outputs. *)
+ (** Mean values of inputs and one value for all outputs. *)
range_values : float list * float;
- (** Range values of inputs and one value for all outputs. *)
+ (** Range values of inputs and one value for all outputs. *)
weights_biases : float list list; (** All weights and biases of NNet model. *)
}
(** NNet model metadata. *)
diff --git a/src/detection.ml b/src/detection.ml
index ed15cdc15bf5bf686309eab4e8993a7c785833b2..c4fa222a5ace8ff5025cb8e9eacd8bb058eb7c40 100644
--- a/src/detection.ml
+++ b/src/detection.ml
@@ -1,24 +1,27 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
open Base
module Sys = Caml.Sys
let null = if Sys.unix then "/dev/null" else "NUL"
-let rec lookup_file l f =
- match l with
+let rec lookup_file dirs filename =
+ match dirs with
| [] -> raise Caml.Not_found
- | a :: l ->
- let abs = Caml.Filename.concat a f in
- if Sys.file_exists abs then abs else lookup_file l f
+ | dir :: dirs ->
+ let file = Caml.Filename.concat dir filename in
+ if Sys.file_exists file then file else lookup_file dirs filename
let detect () =
- Why3.Debug.set_flag Why3.Autodetection.debug;
- let caisar_autodetection =
- lookup_file Stdlib_path.Sites.config "provers_autodetection.conf"
- in
- let data =
- Why3.Autodetection.Prover_autodetection_data.from_file caisar_autodetection
- in
- let config = Why3.Whyconf.init_config (Some null) in
- let binaries = Why3.Autodetection.request_binaries_version config data in
- let provers = Why3.Autodetection.compute_builtin_prover binaries data in
- Why3.Whyconf.set_provers config provers
+ let open Why3 in
+ Debug.set_flag Why3.Autodetection.debug;
+ let caisar_conf = lookup_file Dirs.Sites.config "caisar.conf" in
+ let data = Autodetection.Prover_autodetection_data.from_file caisar_conf in
+ let config = Whyconf.init_config (Some null) in
+ let binaries = Autodetection.request_binaries_version config data in
+ let provers = Autodetection.compute_builtin_prover binaries data in
+ Whyconf.set_provers config provers
diff --git a/src/dune b/src/dune
index 0e5cc551f334b959e6ee9c7564e3347740d71645..3d9b62cc15be31725720c7cf92474d8f1110e275 100644
--- a/src/dune
+++ b/src/dune
@@ -6,4 +6,6 @@
(package caisar)
)
-(generate_sites_module (module stdlib_path) (sites caisar))
+(generate_sites_module
+ (module dirs)
+ (sites caisar))
diff --git a/src/language.ml b/src/language.ml
index ee97874283d40ee8769c1899b37d914ea1920784..d5a0606319a70b39e25b5bb5c1f1c39477362269 100644
--- a/src/language.ml
+++ b/src/language.ml
@@ -6,7 +6,7 @@
open Base
-(* Register neural network languages *)
+(* Register neural network formats. *)
let nnet_parser env _ filename _ =
let open Why3 in
@@ -18,24 +18,24 @@ let nnet_parser env _ filename _ =
match header with
| Error s -> Loc.errorm "%s" s
| Ok header ->
- let id_as_tuple = Ident.id_fresh "As_tuple" in
- let th_uc = Pmodule.create_module env id_as_tuple in
- let th_uc = Pmodule.use_export th_uc nnet in
- let ls_out =
- Term.create_fsymbol
- (Ident.id_fresh "nnet_apply")
- (List.init header.n_inputs ~f:(fun _ -> nnet_input_type))
- (Ty.ty_tuple
- (List.init header.n_outputs ~f:(fun _ -> nnet_input_type)))
- in
+ let id_as_tuple = Ident.id_fresh "AsTuple" in
+ let th_uc = Pmodule.create_module env id_as_tuple in
+ let th_uc = Pmodule.use_export th_uc nnet in
+ let ls_nnet_apply =
+ let f _ = nnet_input_type in
+ Term.create_fsymbol
+ (Ident.id_fresh "nnet_apply")
+ (List.init header.n_inputs ~f)
+ (Ty.ty_tuple (List.init header.n_outputs ~f))
+ in
- let th_uc =
- Pmodule.add_pdecl ~vc:false th_uc
- (Pdecl.create_pure_decl @@ Decl.create_param_decl ls_out)
- in
- Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
+ let th_uc =
+ Pmodule.add_pdecl ~vc:false th_uc
+ (Pdecl.create_pure_decl @@ Decl.create_param_decl ls_nnet_apply)
+ in
+ Wstdlib.Mstr.singleton "AsTuple" (Pmodule.close_module th_uc)
let register () =
- Why3.Env.(
- register_format ~desc:"NNet format (ReLU only)" Why3.Pmodule.mlw_language
+ Why3.(
+ Env.register_format ~desc:"NNet format (ReLU only)" Pmodule.mlw_language
"NNet" [ "nnet" ] nnet_parser)
diff --git a/src/main.ml b/src/main.ml
index 8cda571d7003b06e78164942c268aa84da68db50..81d0a2b30f598b485333d04a8f127d8a97577ec8 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -24,13 +24,13 @@ let pp_header =
match l with
| Logs.App -> Fmt.pf ppf "[%a] " Fmt.(styled app_style string) x
| Logs.Error ->
- pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
+ pp_h ppf err_style (match h with None -> "ERROR" | Some h -> h)
| Logs.Warning ->
- pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
+ pp_h ppf warn_style (match h with None -> "WARNING" | Some h -> h)
| Logs.Info ->
- pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
+ pp_h ppf info_style (match h with None -> "INFO" | Some h -> h)
| Logs.Debug ->
- pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
+ pp_h ppf debug_style (match h with None -> "DEBUG" | Some h -> h)
let setup_logs =
let setup_log level =
@@ -78,11 +78,12 @@ let config_cmd =
( Term.(
ret
(const (fun cmdname detect _ ->
- if not detect then `Help (`Pager, Some "config")
- else
- (* TODO: Do not only check for [detect], and enable it by
- default, as soon as other options are available. *)
- `Ok (config cmdname true ()))
+ if not detect
+ then `Help (`Pager, Some "config")
+ else
+ (* TODO: Do not only check for [detect], and enable it by
+ default, as soon as other options are available. *)
+ `Ok (config cmdname true ()))
$ const cmdname $ detect $ setup_logs)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~envs ~exits ~doc ~man )
@@ -110,7 +111,7 @@ let verify_cmd =
( Term.(
ret
(const (fun format loadpath files ->
- `Ok (List.iter ~f:(Prove.prove format loadpath) files))
+ `Ok (List.iter ~f:(Verify.do_verify format loadpath) files))
$ format $ loadpath $ files)),
Term.info cmdname ~sdocs:Manpage.s_common_options ~exits ~doc ~man )
diff --git a/src/prove.ml b/src/prove.ml
deleted file mode 100644
index bdddcae4af7b0851250da637f8aa8a207cf84d7c..0000000000000000000000000000000000000000
--- a/src/prove.ml
+++ /dev/null
@@ -1,36 +0,0 @@
-open Base
-
-let () = Language.register ()
-
-let create_env loadpath =
- let conf = Detection.detect () in
- let stdlib = Stdlib_path.Sites.stdlib in
- ( Why3.Env.create_env
- (loadpath @ stdlib @ Why3.Whyconf.loadpath (Why3.Whyconf.get_main conf)),
- conf )
-
-let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
-
-let prove format loadpath file =
- let env, config = create_env loadpath in
- let _, m =
- match file with
- | "-" ->
- ( "stdin",
- Why3.Env.read_channel ?format Why3.Env.base_language env "stdin"
- Caml.stdin )
- | fname ->
- let mlw_files, _ =
- Why3.Env.read_file ?format Why3.Env.base_language env fname
- in
- (fname, mlw_files)
- in
- Why3.Wstdlib.Mstr.iter
- (fun _ th ->
- let l = Why3.Task.split_theory th None None in
- let prover = Why3.Whyconf.filter_one_prover config altergo in
- let driver =
- Why3.Whyconf.load_driver (Why3.Whyconf.get_main config) env prover
- in
- List.iter l ~f:(Fmt.pr "%a" (Why3.Driver.print_task driver)))
- m
diff --git a/src/verify.ml b/src/verify.ml
new file mode 100644
index 0000000000000000000000000000000000000000..3aa60d7bb21fb797dcdb59d50db05836bd747db1
--- /dev/null
+++ b/src/verify.ml
@@ -0,0 +1,40 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Caisar. *)
+(* *)
+(**************************************************************************)
+
+open Base
+module Format = Caml.Format
+
+let () = Language.register ()
+
+let create_env loadpath =
+ let config = Detection.detect () in
+ let stdlib = Dirs.Sites.stdlib in
+
+ let open Why3 in
+ ( Env.create_env
+ (loadpath @ stdlib @ Whyconf.loadpath (Whyconf.get_main config)),
+ config )
+
+let altergo = Why3.Whyconf.mk_filter_prover "Alt-Ergo"
+
+let do_verify format loadpath file =
+ let open Why3 in
+ let env, config = create_env loadpath in
+ let _, mstr_theory =
+ match file with
+ | "-" ->
+ ("stdin", Env.(read_channel ?format base_language env "stdin" Caml.stdin))
+ | filename ->
+ let mlw_files, _ = Env.(read_file ?format base_language env filename) in
+ (filename, mlw_files)
+ in
+ Wstdlib.Mstr.iter
+ (fun _ theory ->
+ let tasks = Task.split_theory theory None None in
+ let prover = Whyconf.filter_one_prover config altergo in
+ let driver = Whyconf.(load_driver (get_main config) env prover) in
+ List.iter tasks ~f:(Format.printf "%a" (Driver.print_task driver)))
+ mstr_theory
diff --git a/stdlib/caisar.mlw b/stdlib/caisar.mlw
index 09763d9fea2daaf27063263bd4e2ec532a3a23d7..c29586772de968684847674cfe0347514ebc3204 100644
--- a/stdlib/caisar.mlw
+++ b/stdlib/caisar.mlw
@@ -1,4 +1,4 @@
theory NNet
- use ieee_float.Float64
- type input_type = t
+ use ieee_float.Float64
+ type input_type = t
end
diff --git a/tests/simple.t b/tests/simple.t
index b1729081aa728e20fc804ecefaddedfa2c1140c4..2fd8bba5e21304a722ac04c66183b78c91de96bf 100644
--- a/tests/simple.t
+++ b/tests/simple.t
@@ -11,1542 +11,1359 @@ Test help
> 0.0 <. t'real y1 <. 0.1
> end
> EOF
- theory Task
- type int
-
- type real
-
- type string
-
- predicate (=) 'a 'a
-
- (* use why3.BuiltIn.BuiltIn *)
-
- type bool =
- | True
- | False
-
- (* use why3.Bool.Bool *)
-
- type tuple0 =
- | Tuple0
-
- (* use why3.Tuple0.Tuple01 *)
-
- type unit = unit
-
- (* use why3.Unit.Unit *)
-
- constant zero : int = 0
-
- constant one : int = 1
-
- function (-_) int : int
-
- function (+) int int : int
-
- function ( * ) int int : int
-
- predicate (<) int int
-
- function (-) (x:int) (y:int) : int = x + (- y)
-
- predicate (>) (x:int) (y:int) = y < x
-
- predicate (<=) (x:int) (y:int) = x < y \/ x = y
-
- predicate (>=) (x:int) (y:int) = y <= x
-
- Assoc : forall x:int, y:int, z:int. ((x + y) + z) = (x + (y + z))
-
- (* clone algebra.Assoc with type t = int, function op = (+),
- prop Assoc1 = Assoc, *)
-
- Unit_def_l : forall x:int. (zero + x) = x
-
- Unit_def_r : forall x:int. (x + zero) = x
-
- (* clone algebra.Monoid with type t1 = int, constant unit = zero,
- function op1 = (+), prop Unit_def_r1 = Unit_def_r,
- prop Unit_def_l1 = Unit_def_l, prop Assoc2 = Assoc, *)
-
- Inv_def_l : forall x:int. ((- x) + x) = zero
-
- Inv_def_r : forall x:int. (x + (- x)) = zero
-
- (* clone algebra.Group with type t2 = int, function inv = (-_),
- constant unit1 = zero, function op2 = (+), prop Inv_def_r1 = Inv_def_r,
- prop Inv_def_l1 = Inv_def_l, prop Unit_def_r2 = Unit_def_r,
- prop Unit_def_l2 = Unit_def_l, prop Assoc3 = Assoc, *)
-
- Comm : forall x:int, y:int. (x + y) = (y + x)
-
- (* clone algebra.Comm with type t3 = int, function op3 = (+),
- prop Comm1 = Comm, *)
-
- (* meta AC function (+) *)
-
- (* clone algebra.CommutativeGroup with type t4 = int, function inv1 = (-_),
- constant unit2 = zero, function op4 = (+), prop Comm2 = Comm,
- prop Inv_def_r2 = Inv_def_r, prop Inv_def_l2 = Inv_def_l,
- prop Unit_def_r3 = Unit_def_r, prop Unit_def_l3 = Unit_def_l,
- prop Assoc4 = Assoc, *)
-
- Assoc5 : forall x:int, y:int, z:int. ((x * y) * z) = (x * (y * z))
-
- (* clone algebra.Assoc with type t = int, function op = ( * ),
- prop Assoc1 = Assoc5, *)
-
- Mul_distr_l :
- forall x:int, y:int, z:int. (x * (y + z)) = ((x * y) + (x * z))
-
- Mul_distr_r :
- forall x:int, y:int, z:int. ((y + z) * x) = ((y * x) + (z * x))
-
- (* clone algebra.Ring with type t5 = int, function ( *') = ( * ),
- function (-'_) = (-_), function (+') = (+), constant zero1 = zero,
- prop Mul_distr_r1 = Mul_distr_r, prop Mul_distr_l1 = Mul_distr_l,
- prop Assoc6 = Assoc5, prop Comm3 = Comm, prop Inv_def_r3 = Inv_def_r,
- prop Inv_def_l3 = Inv_def_l, prop Unit_def_r4 = Unit_def_r,
- prop Unit_def_l4 = Unit_def_l, prop Assoc7 = Assoc, *)
-
- Comm4 : forall x:int, y:int. (x * y) = (y * x)
-
- (* clone algebra.Comm with type t3 = int, function op3 = ( * ),
- prop Comm1 = Comm4, *)
-
- (* meta AC function ( * ) *)
-
- (* clone algebra.CommutativeRing with type t6 = int,
- function ( *'') = ( * ), function (-''_) = (-_), function (+'') = (+),
- constant zero2 = zero, prop Comm5 = Comm4,
- prop Mul_distr_r2 = Mul_distr_r, prop Mul_distr_l2 = Mul_distr_l,
- prop Assoc8 = Assoc5, prop Comm6 = Comm, prop Inv_def_r4 = Inv_def_r,
- prop Inv_def_l4 = Inv_def_l, prop Unit_def_r5 = Unit_def_r,
- prop Unit_def_l5 = Unit_def_l, prop Assoc9 = Assoc, *)
-
- Unitary : forall x:int. (one * x) = x
-
- NonTrivialRing : not zero = one
-
- (* clone algebra.UnitaryCommutativeRing with type t7 = int,
- constant one1 = one, function ( *''') = ( * ), function (-'''_) = (-_),
- function (+''') = (+), constant zero3 = zero,
- prop NonTrivialRing1 = NonTrivialRing, prop Unitary1 = Unitary,
- prop Comm7 = Comm4, prop Mul_distr_r3 = Mul_distr_r,
- prop Mul_distr_l3 = Mul_distr_l, prop Assoc10 = Assoc5,
- prop Comm8 = Comm, prop Inv_def_r5 = Inv_def_r,
- prop Inv_def_l5 = Inv_def_l, prop Unit_def_r6 = Unit_def_r,
- prop Unit_def_l6 = Unit_def_l, prop Assoc11 = Assoc, *)
-
- (* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
- *)
-
- Refl : forall x:int. x <= x
-
- (* clone relations.Reflexive with type t9 = int, predicate rel1 = (<=),
- prop Refl1 = Refl, *)
-
- (* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
- *)
-
- Trans : forall x:int, y:int, z:int. x <= y -> y <= z -> x <= z
-
- (* clone relations.Transitive with type t10 = int, predicate rel2 = (<=),
- prop Trans1 = Trans, *)
-
- (* clone relations.PreOrder with type t11 = int, predicate rel3 = (<=),
- prop Trans2 = Trans, prop Refl2 = Refl, *)
-
- (* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
- *)
-
- Antisymm : forall x:int, y:int. x <= y -> y <= x -> x = y
-
- (* clone relations.Antisymmetric with type t12 = int,
- predicate rel4 = (<=), prop Antisymm1 = Antisymm, *)
-
- (* clone relations.PartialOrder with type t13 = int, predicate rel5 = (<=),
- prop Antisymm2 = Antisymm, prop Trans3 = Trans, prop Refl3 = Refl, *)
-
- (* clone relations.EndoRelation with type t8 = int, predicate rel = (<=),
- *)
-
- Total : forall x:int, y:int. x <= y \/ y <= x
-
- (* clone relations.Total with type t14 = int, predicate rel6 = (<=),
- prop Total1 = Total, *)
-
- (* clone relations.TotalOrder with type t15 = int, predicate rel7 = (<=),
- prop Total2 = Total, prop Antisymm3 = Antisymm, prop Trans4 = Trans,
- prop Refl4 = Refl, *)
-
- ZeroLessOne : zero <= one
-
- CompatOrderAdd : forall x:int, y:int, z:int. x <= y -> (x + z) <= (y + z)
-
- CompatOrderMult :
- forall x:int, y:int, z:int. x <= y -> zero <= z -> (x * z) <= (y * z)
-
- (* clone algebra.OrderedUnitaryCommutativeRing with type t16 = int,
- predicate (<=') = (<=), constant one2 = one, function ( *'''') = ( * ),
- function (-''''_) = (-_), function (+'''') = (+), constant zero4 = zero,
- prop CompatOrderMult1 = CompatOrderMult,
- prop CompatOrderAdd1 = CompatOrderAdd, prop ZeroLessOne1 = ZeroLessOne,
- prop Total3 = Total, prop Antisymm4 = Antisymm, prop Trans5 = Trans,
- prop Refl5 = Refl, prop NonTrivialRing2 = NonTrivialRing,
- prop Unitary2 = Unitary, prop Comm9 = Comm4,
- prop Mul_distr_r4 = Mul_distr_r, prop Mul_distr_l4 = Mul_distr_l,
- prop Assoc12 = Assoc5, prop Comm10 = Comm, prop Inv_def_r6 = Inv_def_r,
- prop Inv_def_l6 = Inv_def_l, prop Unit_def_r7 = Unit_def_r,
- prop Unit_def_l7 = Unit_def_l, prop Assoc13 = Assoc, *)
-
- (* use int.Int *)
-
- constant zero5 : real = 0.0
-
- constant one3 : real = 1.0
-
- function (-'''''_) real : real
-
- function (+''''') real real : real
-
- function ( *''''') real real : real
-
- predicate (<') real real
-
- predicate (>') (x:real) (y:real) = y <' x
-
- predicate (<='') (x:real) (y:real) = x <' y \/ x = y
-
- predicate (>=') (x:real) (y:real) = y <='' x
-
- Assoc14 :
- forall x:real, y:real, z:real.
- ((x +''''' y) +''''' z) = (x +''''' (y +''''' z))
-
- (* clone algebra.Assoc with type t = real, function op = (+'''''),
- prop Assoc1 = Assoc14, *)
-
- Unit_def_l8 : forall x:real. (zero5 +''''' x) = x
-
- Unit_def_r8 : forall x:real. (x +''''' zero5) = x
-
- (* clone algebra.Monoid with type t1 = real, constant unit = zero5,
- function op1 = (+'''''), prop Unit_def_r1 = Unit_def_r8,
- prop Unit_def_l1 = Unit_def_l8, prop Assoc2 = Assoc14, *)
-
- Inv_def_l7 : forall x:real. ((-''''' x) +''''' x) = zero5
-
- Inv_def_r7 : forall x:real. (x +''''' (-''''' x)) = zero5
-
- (* clone algebra.Group with type t2 = real, function inv = (-'''''_),
- constant unit1 = zero5, function op2 = (+'''''),
- prop Inv_def_r1 = Inv_def_r7, prop Inv_def_l1 = Inv_def_l7,
- prop Unit_def_r2 = Unit_def_r8, prop Unit_def_l2 = Unit_def_l8,
- prop Assoc3 = Assoc14, *)
-
- Comm11 : forall x:real, y:real. (x +''''' y) = (y +''''' x)
-
- (* clone algebra.Comm with type t3 = real, function op3 = (+'''''),
- prop Comm1 = Comm11, *)
-
- (* meta AC function (+''''') *)
-
- (* clone algebra.CommutativeGroup with type t4 = real,
- function inv1 = (-'''''_), constant unit2 = zero5,
- function op4 = (+'''''), prop Comm2 = Comm11,
- prop Inv_def_r2 = Inv_def_r7, prop Inv_def_l2 = Inv_def_l7,
- prop Unit_def_r3 = Unit_def_r8, prop Unit_def_l3 = Unit_def_l8,
- prop Assoc4 = Assoc14, *)
-
- Assoc15 :
- forall x:real, y:real, z:real.
- ((x *''''' y) *''''' z) = (x *''''' (y *''''' z))
-
- (* clone algebra.Assoc with type t = real, function op = ( *'''''),
- prop Assoc1 = Assoc15, *)
-
- Mul_distr_l5 :
- forall x:real, y:real, z:real.
- (x *''''' (y +''''' z)) = ((x *''''' y) +''''' (x *''''' z))
-
- Mul_distr_r5 :
- forall x:real, y:real, z:real.
- ((y +''''' z) *''''' x) = ((y *''''' x) +''''' (z *''''' x))
-
- (* clone algebra.Ring with type t5 = real, function ( *') = ( *'''''),
- function (-'_) = (-'''''_), function (+') = (+'''''),
- constant zero1 = zero5, prop Mul_distr_r1 = Mul_distr_r5,
- prop Mul_distr_l1 = Mul_distr_l5, prop Assoc6 = Assoc15,
- prop Comm3 = Comm11, prop Inv_def_r3 = Inv_def_r7,
- prop Inv_def_l3 = Inv_def_l7, prop Unit_def_r4 = Unit_def_r8,
- prop Unit_def_l4 = Unit_def_l8, prop Assoc7 = Assoc14, *)
-
- Comm12 : forall x:real, y:real. (x *''''' y) = (y *''''' x)
-
- (* clone algebra.Comm with type t3 = real, function op3 = ( *'''''),
- prop Comm1 = Comm12, *)
-
- (* meta AC function ( *''''') *)
-
- (* clone algebra.CommutativeRing with type t6 = real,
- function ( *'') = ( *'''''), function (-''_) = (-'''''_),
- function (+'') = (+'''''), constant zero2 = zero5, prop Comm5 = Comm12,
- prop Mul_distr_r2 = Mul_distr_r5, prop Mul_distr_l2 = Mul_distr_l5,
- prop Assoc8 = Assoc15, prop Comm6 = Comm11, prop Inv_def_r4 = Inv_def_r7,
- prop Inv_def_l4 = Inv_def_l7, prop Unit_def_r5 = Unit_def_r8,
- prop Unit_def_l5 = Unit_def_l8, prop Assoc9 = Assoc14, *)
-
- Unitary3 : forall x:real. (one3 *''''' x) = x
-
- NonTrivialRing3 : not zero5 = one3
-
- (* clone algebra.UnitaryCommutativeRing with type t7 = real,
- constant one1 = one3, function ( *''') = ( *'''''),
- function (-'''_) = (-'''''_), function (+''') = (+'''''),
- constant zero3 = zero5, prop NonTrivialRing1 = NonTrivialRing3,
- prop Unitary1 = Unitary3, prop Comm7 = Comm12,
- prop Mul_distr_r3 = Mul_distr_r5, prop Mul_distr_l3 = Mul_distr_l5,
- prop Assoc10 = Assoc15, prop Comm8 = Comm11,
- prop Inv_def_r5 = Inv_def_r7, prop Inv_def_l5 = Inv_def_l7,
- prop Unit_def_r6 = Unit_def_r8, prop Unit_def_l6 = Unit_def_l8,
- prop Assoc11 = Assoc14, *)
-
- function inv2 real : real
-
- Inverse : forall x:real. not x = zero5 -> (x *''''' inv2 x) = one3
-
- function (-') (x:real) (y:real) : real = x +''''' (-''''' y)
-
- function (/) (x:real) (y:real) : real = x *''''' inv2 y
-
- add_div :
- forall x:real, y:real, z:real.
- not z = zero5 -> ((x +''''' y) / z) = ((x / z) +''''' (y / z))
-
- sub_div :
- forall x:real, y:real, z:real.
- not z = zero5 -> ((x -' y) / z) = ((x / z) -' (y / z))
-
- neg_div :
- forall x:real, y:real.
- not y = zero5 -> ((-''''' x) / y) = (-''''' (x / y))
-
- assoc_mul_div :
- forall x:real, y:real, z:real.
- not z = zero5 -> ((x *''''' y) / z) = (x *''''' (y / z))
-
- assoc_div_mul :
- forall x:real, y:real, z:real.
- not y = zero5 /\ not z = zero5 -> ((x / y) / z) = (x / (y *''''' z))
-
- assoc_div_div :
- forall x:real, y:real, z:real.
- not y = zero5 /\ not z = zero5 -> (x / (y / z)) = ((x *''''' z) / y)
-
- (* clone algebra.Field with type t17 = real, function (/') = (/),
- function (-'') = (-'), function inv3 = inv2, constant one4 = one3,
- function ( *'''''') = ( *'''''), function (-''''''_) = (-'''''_),
- function (+'''''') = (+'''''), constant zero6 = zero5,
- prop assoc_div_div1 = assoc_div_div, prop assoc_div_mul1 = assoc_div_mul,
- prop assoc_mul_div1 = assoc_mul_div, prop neg_div1 = neg_div,
- prop sub_div1 = sub_div, prop add_div1 = add_div,
- prop Inverse1 = Inverse, prop NonTrivialRing4 = NonTrivialRing3,
- prop Unitary4 = Unitary3, prop Comm13 = Comm12,
- prop Mul_distr_r6 = Mul_distr_r5, prop Mul_distr_l6 = Mul_distr_l5,
- prop Assoc16 = Assoc15, prop Comm14 = Comm11,
- prop Inv_def_r8 = Inv_def_r7, prop Inv_def_l8 = Inv_def_l7,
- prop Unit_def_r9 = Unit_def_r8, prop Unit_def_l9 = Unit_def_l8,
- prop Assoc17 = Assoc14, *)
-
- (* clone relations.EndoRelation with type t8 = real,
- predicate rel = (<=''), *)
-
- Refl6 : forall x:real. x <='' x
-
- (* clone relations.Reflexive with type t9 = real, predicate rel1 = (<=''),
- prop Refl1 = Refl6, *)
-
- (* clone relations.EndoRelation with type t8 = real,
- predicate rel = (<=''), *)
-
- Trans6 : forall x:real, y:real, z:real. x <='' y -> y <='' z -> x <='' z
-
- (* clone relations.Transitive with type t10 = real,
- predicate rel2 = (<=''), prop Trans1 = Trans6, *)
-
- (* clone relations.PreOrder with type t11 = real, predicate rel3 = (<=''),
- prop Trans2 = Trans6, prop Refl2 = Refl6, *)
-
- (* clone relations.EndoRelation with type t8 = real,
- predicate rel = (<=''), *)
-
- Antisymm5 : forall x:real, y:real. x <='' y -> y <='' x -> x = y
-
- (* clone relations.Antisymmetric with type t12 = real,
- predicate rel4 = (<=''), prop Antisymm1 = Antisymm5, *)
-
- (* clone relations.PartialOrder with type t13 = real,
- predicate rel5 = (<=''), prop Antisymm2 = Antisymm5,
- prop Trans3 = Trans6, prop Refl3 = Refl6, *)
-
- (* clone relations.EndoRelation with type t8 = real,
- predicate rel = (<=''), *)
-
- Total4 : forall x:real, y:real. x <='' y \/ y <='' x
-
- (* clone relations.Total with type t14 = real, predicate rel6 = (<=''),
- prop Total1 = Total4, *)
-
- (* clone relations.TotalOrder with type t15 = real,
- predicate rel7 = (<=''), prop Total2 = Total4,
- prop Antisymm3 = Antisymm5, prop Trans4 = Trans6, prop Refl4 = Refl6, *)
-
- ZeroLessOne2 : zero5 <='' one3
-
- CompatOrderAdd2 :
- forall x:real, y:real, z:real. x <='' y -> (x +''''' z) <='' (y +''''' z)
-
- CompatOrderMult2 :
- forall x:real, y:real, z:real.
- x <='' y -> zero5 <='' z -> (x *''''' z) <='' (y *''''' z)
-
- (* clone algebra.OrderedField with type t18 = real,
- predicate (<=''') = (<=''), function (/'') = (/), function (-''') = (-'),
- function inv4 = inv2, constant one5 = one3,
- function ( *''''''') = ( *'''''), function (-'''''''_) = (-'''''_),
- function (+''''''') = (+'''''), constant zero7 = zero5,
- prop CompatOrderMult3 = CompatOrderMult2,
- prop CompatOrderAdd3 = CompatOrderAdd2, prop ZeroLessOne3 = ZeroLessOne2,
- prop Total5 = Total4, prop Antisymm6 = Antisymm5, prop Trans7 = Trans6,
- prop Refl7 = Refl6, prop assoc_div_div2 = assoc_div_div,
- prop assoc_div_mul2 = assoc_div_mul, prop assoc_mul_div2 = assoc_mul_div,
- prop neg_div2 = neg_div, prop sub_div2 = sub_div,
- prop add_div2 = add_div, prop Inverse2 = Inverse,
- prop NonTrivialRing5 = NonTrivialRing3, prop Unitary5 = Unitary3,
- prop Comm15 = Comm12, prop Mul_distr_r7 = Mul_distr_r5,
- prop Mul_distr_l7 = Mul_distr_l5, prop Assoc18 = Assoc15,
- prop Comm16 = Comm11, prop Inv_def_r9 = Inv_def_r7,
- prop Inv_def_l9 = Inv_def_l7, prop Unit_def_r10 = Unit_def_r8,
- prop Unit_def_l10 = Unit_def_l8, prop Assoc19 = Assoc14, *)
-
- (* use real.Real *)
-
- type t19 = <float 11 53>
-
- function t'real t19 : real
-
- predicate t'isFinite t19
-
- constant t'eb : int = 11
-
- constant t'sb : int = 53
-
- (* meta float_type type t19, function t'real, predicate t'isFinite *)
-
- (* meta model_projection function t'real *)
-
- constant pow2sb : int = 9007199254740992
-
- constant max_real : real = 0x1.FFFFFFFFFFFFFp1023
-
- function pow2 int : int
-
- axiom Power_0 : pow2 0 = 1
-
- axiom Power_s : forall n:int. n >= 0 -> pow2 (n + 1) = (2 * pow2 n)
-
- Power_1 : pow2 1 = 2
-
- Power_sum :
- forall n:int, m:int. n >= 0 /\ m >= 0 -> pow2 (n + m) = (pow2 n * pow2 m)
-
- pow2pos : forall i:int. i >= 0 -> pow2 i > 0
-
- pow2_0 : pow2 0 = 0x1
-
- pow2_1 : pow2 1 = 0x2
-
- pow2_2 : pow2 2 = 0x4
-
- pow2_3 : pow2 3 = 0x8
-
- pow2_4 : pow2 4 = 0x10
-
- pow2_5 : pow2 5 = 0x20
-
- pow2_6 : pow2 6 = 0x40
-
- pow2_7 : pow2 7 = 0x80
-
- pow2_8 : pow2 8 = 0x100
-
- pow2_9 : pow2 9 = 0x200
-
- pow2_10 : pow2 10 = 0x400
-
- pow2_11 : pow2 11 = 0x800
-
- pow2_12 : pow2 12 = 0x1000
-
- pow2_13 : pow2 13 = 0x2000
-
- pow2_14 : pow2 14 = 0x4000
-
- pow2_15 : pow2 15 = 0x8000
-
- pow2_16 : pow2 16 = 0x10000
-
- pow2_17 : pow2 17 = 0x20000
-
- pow2_18 : pow2 18 = 0x40000
-
- pow2_19 : pow2 19 = 0x80000
-
- pow2_20 : pow2 20 = 0x100000
-
- pow2_21 : pow2 21 = 0x200000
-
- pow2_22 : pow2 22 = 0x400000
-
- pow2_23 : pow2 23 = 0x800000
-
- pow2_24 : pow2 24 = 0x1000000
-
- pow2_25 : pow2 25 = 0x2000000
-
- pow2_26 : pow2 26 = 0x4000000
-
- pow2_27 : pow2 27 = 0x8000000
-
- pow2_28 : pow2 28 = 0x10000000
-
- pow2_29 : pow2 29 = 0x20000000
-
- pow2_30 : pow2 30 = 0x40000000
-
- pow2_31 : pow2 31 = 0x80000000
-
- pow2_32 : pow2 32 = 0x100000000
-
- pow2_33 : pow2 33 = 0x200000000
-
- pow2_34 : pow2 34 = 0x400000000
-
- pow2_35 : pow2 35 = 0x800000000
-
- pow2_36 : pow2 36 = 0x1000000000
-
- pow2_37 : pow2 37 = 0x2000000000
-
- pow2_38 : pow2 38 = 0x4000000000
-
- pow2_39 : pow2 39 = 0x8000000000
-
- pow2_40 : pow2 40 = 0x10000000000
-
- pow2_41 : pow2 41 = 0x20000000000
-
- pow2_42 : pow2 42 = 0x40000000000
-
- pow2_43 : pow2 43 = 0x80000000000
-
- pow2_44 : pow2 44 = 0x100000000000
-
- pow2_45 : pow2 45 = 0x200000000000
-
- pow2_46 : pow2 46 = 0x400000000000
-
- pow2_47 : pow2 47 = 0x800000000000
-
- pow2_48 : pow2 48 = 0x1000000000000
-
- pow2_49 : pow2 49 = 0x2000000000000
-
- pow2_50 : pow2 50 = 0x4000000000000
-
- pow2_51 : pow2 51 = 0x8000000000000
-
- pow2_52 : pow2 52 = 0x10000000000000
-
- pow2_53 : pow2 53 = 0x20000000000000
-
- pow2_54 : pow2 54 = 0x40000000000000
-
- pow2_55 : pow2 55 = 0x80000000000000
-
- pow2_56 : pow2 56 = 0x100000000000000
-
- pow2_57 : pow2 57 = 0x200000000000000
-
- pow2_58 : pow2 58 = 0x400000000000000
-
- pow2_59 : pow2 59 = 0x800000000000000
-
- pow2_60 : pow2 60 = 0x1000000000000000
-
- pow2_61 : pow2 61 = 0x2000000000000000
-
- pow2_62 : pow2 62 = 0x4000000000000000
-
- pow2_63 : pow2 63 = 0x8000000000000000
-
- pow2_64 : pow2 64 = 0x10000000000000000
-
- (* use bv.Pow2int *)
-
- function abs (x:real) : real = if x >=' 0.0 then x else -''''' x
-
- Abs_le :
- forall x:real, y:real. abs x <='' y <-> (-''''' y) <='' x /\ x <='' y
-
- Abs_pos : forall x:real. abs x >=' 0.0
-
- Abs_sum : forall x:real, y:real. abs (x +''''' y) <='' (abs x +''''' abs y)
-
- Abs_prod : forall x:real, y:real. abs (x *''''' y) = (abs x *''''' abs y)
-
- triangular_inequality :
- forall x:real, y:real, z:real.
- abs (x -' z) <='' (abs (x -' y) +''''' abs (y -' z))
-
- (* use real.Abs *)
-
- function from_int int : real
-
- axiom Zero : from_int 0 = 0.0
-
- axiom One : from_int 1 = 1.0
-
- axiom Add :
- forall x:int, y:int. from_int (x + y) = (from_int x +''''' from_int y)
-
- axiom Sub :
- forall x:int, y:int. from_int (x - y) = (from_int x -' from_int y)
-
- axiom Mul :
- forall x:int, y:int. from_int (x * y) = (from_int x *''''' from_int y)
-
- axiom Neg : forall x:int. from_int (- x) = (-''''' from_int x)
-
- Injective : forall x:int, y:int. from_int x = from_int y -> x = y
-
- axiom Monotonic : forall x:int, y:int. x <= y -> from_int x <='' from_int y
-
- (* use real.FromInt *)
-
- function truncate real : int
-
- axiom Truncate_int : forall i:int. truncate (from_int i) = i
-
- axiom Truncate_down_pos :
- forall x:real.
- x >=' 0.0 ->
- from_int (truncate x) <='' x /\ x <' from_int (truncate x + 1)
-
- axiom Truncate_up_neg :
- forall x:real.
- x <='' 0.0 ->
- from_int (truncate x - 1) <' x /\ x <='' from_int (truncate x)
-
- axiom Real_of_truncate :
- forall x:real.
- (x -' 1.0) <='' from_int (truncate x) /\
- from_int (truncate x) <='' (x +''''' 1.0)
-
- axiom Truncate_monotonic :
- forall x:real, y:real. x <='' y -> truncate x <= truncate y
-
- axiom Truncate_monotonic_int1 :
- forall x:real, i:int. x <='' from_int i -> truncate x <= i
-
- axiom Truncate_monotonic_int2 :
- forall x:real, i:int. from_int i <='' x -> i <= truncate x
-
- function floor real : int
-
- function ceil real : int
-
- axiom Floor_int : forall i:int. floor (from_int i) = i
-
- axiom Ceil_int : forall i:int. ceil (from_int i) = i
-
- axiom Floor_down :
- forall x:real. from_int (floor x) <='' x /\ x <' from_int (floor x + 1)
-
- axiom Ceil_up :
- forall x:real. from_int (ceil x - 1) <' x /\ x <='' from_int (ceil x)
-
- axiom Floor_monotonic :
- forall x:real, y:real. x <='' y -> floor x <= floor y
-
- axiom Ceil_monotonic : forall x:real, y:real. x <='' y -> ceil x <= ceil y
-
- (* use real.Truncate *)
-
- function (+.) (x:real) (y:real) : real = x +''''' y
-
- function (-.) (x:real) (y:real) : real = x -' y
-
- function ( *.) (x:real) (y:real) : real = x *''''' y
-
- function (/.) (x:real) (y:real) : real = x / y
-
- function (-._) (x:real) : real = -''''' x
-
- function inv5 (x:real) : real = inv2 x
-
- predicate (<=.) (x:real) (y:real) = x <='' y
-
- predicate (>=.) (x:real) (y:real) = x >=' y
-
- predicate (<.) (x:real) (y:real) = x <' y
-
- predicate (>.) (x:real) (y:real) = x >' y
-
- (* use real.RealInfix *)
-
- type mode =
- | RNE
- | RNA
- | RTP
- | RTN
- | RTZ
-
- predicate to_nearest (m:mode) = m = RNE \/ m = RNA
-
- (* use ieee_float.RoundingMode *)
-
- constant zeroF : t19
-
- function add mode t19 t19 : t19
-
- function sub mode t19 t19 : t19
-
- function mul mode t19 t19 : t19
-
- function div mode t19 t19 : t19
-
- function abs1 t19 : t19
-
- function neg t19 : t19
-
- function fma mode t19 t19 t19 : t19
-
- function sqrt mode t19 : t19
-
- function (.-_) (x:t19) : t19 = neg x
-
- function (.+) (x:t19) (y:t19) : t19 = add RNE x y
-
- function (.-) (x:t19) (y:t19) : t19 = sub RNE x y
-
- function (.* ) (x:t19) (y:t19) : t19 = mul RNE x y
-
- function (./) (x:t19) (y:t19) : t19 = div RNE x y
-
- function roundToIntegral mode t19 : t19
-
- function min t19 t19 : t19
-
- function max t19 t19 : t19
-
- predicate le t19 t19
-
- predicate lt t19 t19
-
- predicate ge (x:t19) (y:t19) = le y x
-
- predicate gt (x:t19) (y:t19) = lt y x
-
- predicate eq t19 t19
-
- predicate (.<=) (x:t19) (y:t19) = le x y
-
- predicate (.<) (x:t19) (y:t19) = lt x y
-
- predicate (.>=) (x:t19) (y:t19) = ge x y
-
- predicate (.>) (x:t19) (y:t19) = gt x y
-
- predicate (.=) (x:t19) (y:t19) = eq x y
-
- predicate is_normal t19
-
- predicate is_subnormal t19
-
- predicate is_zero t19
-
- predicate is_infinite t19
-
- predicate is_nan t19
-
- predicate is_positive t19
-
- predicate is_negative t19
-
- predicate is_plus_infinity (x:t19) = is_infinite x /\ is_positive x
-
- predicate is_minus_infinity (x:t19) = is_infinite x /\ is_negative x
-
- predicate is_plus_zero (x:t19) = is_zero x /\ is_positive x
-
- predicate is_minus_zero (x:t19) = is_zero x /\ is_negative x
-
- predicate is_not_nan (x:t19) = t'isFinite x \/ is_infinite x
-
- is_not_nan : forall x:t19. is_not_nan x <-> not is_nan x
-
- is_not_finite :
- forall x:t19. not t'isFinite x <-> is_infinite x \/ is_nan x
-
- zeroF_is_positive : is_positive zeroF
-
- zeroF_is_zero : is_zero zeroF
-
- zero_to_real :
- forall x:t19 [is_zero x]. is_zero x <-> t'isFinite x /\ t'real x = 0.0
-
- function of_int mode int : t19
-
- function to_int mode t19 : int
-
- zero_of_int : forall m:mode. zeroF = of_int m 0
-
- function round mode real : real
-
- constant max_int : int
-
- constant emax : int = pow2 (t'eb - 1)
-
- max_real_int : max_real = from_int max_int
-
- predicate in_range (x:real) = (-. max_real) <=. x /\ x <=. max_real
-
- predicate in_int_range (i:int) = (- max_int) <= i /\ i <= max_int
-
- is_finite : forall x:t19. t'isFinite x -> in_range (t'real x)
-
- predicate no_overflow (m:mode) (x:real) = in_range (round m x)
-
- Bounded_real_no_overflow :
- forall m:mode, x:real. in_range x -> no_overflow m x
-
- Round_monotonic :
- forall m:mode, x:real, y:real. x <=. y -> round m x <=. round m y
-
- Round_idempotent :
- forall m1:mode, m2:mode, x:real. round m1 (round m2 x) = round m2 x
-
- Round_to_real :
- forall m:mode, x:t19. t'isFinite x -> round m (t'real x) = t'real x
-
- Round_down_le : forall x:real. round RTN x <=. x
-
- Round_up_ge : forall x:real. round RTP x >=. x
-
- Round_down_neg : forall x:real. round RTN (-. x) = (-. round RTP x)
-
- Round_up_neg : forall x:real. round RTP (-. x) = (-. round RTN x)
-
- predicate in_safe_int_range (i:int) = (- pow2sb) <= i /\ i <= pow2sb
-
- Exact_rounding_for_integers :
- forall m:mode, i:int.
- in_safe_int_range i -> round m (from_int i) = from_int i
-
- predicate same_sign (x:t19) (y:t19) =
- is_positive x /\ is_positive y \/ is_negative x /\ is_negative y
-
- predicate diff_sign (x:t19) (y:t19) =
- is_positive x /\ is_negative y \/ is_negative x /\ is_positive y
-
- feq_eq :
- forall x:t19, y:t19.
- t'isFinite x -> t'isFinite y -> not is_zero x -> x .= y -> x = y
-
- eq_feq :
- forall x:t19, y:t19. t'isFinite x -> t'isFinite y -> x = y -> x .= y
-
- eq_refl : forall x:t19. t'isFinite x -> x .= x
-
- eq_sym : forall x:t19, y:t19. x .= y -> y .= x
-
- eq_trans : forall x:t19, y:t19, z:t19. x .= y -> y .= z -> x .= z
-
- eq_zero : zeroF .= (.- zeroF)
-
- eq_to_real_finite :
- forall x:t19, y:t19.
- t'isFinite x /\ t'isFinite y -> x .= y <-> t'real x = t'real y
-
- eq_special :
- forall x:t19, y:t19.
- x .= y ->
- is_not_nan x /\
- is_not_nan y /\
- (t'isFinite x /\ t'isFinite y \/
- is_infinite x /\ is_infinite y /\ same_sign x y)
-
- lt_finite :
- forall x:t19, y:t19 [lt x y].
- t'isFinite x /\ t'isFinite y -> lt x y <-> t'real x <. t'real y
-
- le_finite :
- forall x:t19, y:t19 [le x y].
- t'isFinite x /\ t'isFinite y -> le x y <-> t'real x <=. t'real y
-
- le_lt_trans : forall x:t19, y:t19, z:t19. x .<= y /\ y .< z -> x .< z
-
- lt_le_trans : forall x:t19, y:t19, z:t19. x .< y /\ y .<= z -> x .< z
-
- le_ge_asym : forall x:t19, y:t19. x .<= y /\ x .>= y -> x .= y
-
- not_lt_ge :
- forall x:t19, y:t19.
- not x .< y /\ is_not_nan x /\ is_not_nan y -> x .>= y
-
- not_gt_le :
- forall x:t19, y:t19.
- not x .> y /\ is_not_nan x /\ is_not_nan y -> x .<= y
-
- le_special :
- forall x:t19, y:t19 [le x y].
- le x y ->
- t'isFinite x /\ t'isFinite y \/
- is_minus_infinity x /\ is_not_nan y \/
- is_not_nan x /\ is_plus_infinity y
-
- lt_special :
- forall x:t19, y:t19 [lt x y].
- lt x y ->
- t'isFinite x /\ t'isFinite y \/
- is_minus_infinity x /\ is_not_nan y /\ not is_minus_infinity y \/
- is_not_nan x /\ not is_plus_infinity x /\ is_plus_infinity y
-
- lt_lt_finite : forall x:t19, y:t19, z:t19. lt x y -> lt y z -> t'isFinite y
-
- positive_to_real :
- forall x:t19 [is_positive x| t'real x >=. 0.0].
- t'isFinite x -> is_positive x -> t'real x >=. 0.0
-
- to_real_positive :
- forall x:t19 [is_positive x].
- t'isFinite x -> t'real x >. 0.0 -> is_positive x
-
- negative_to_real :
- forall x:t19 [is_negative x| t'real x <=. 0.0].
- t'isFinite x -> is_negative x -> t'real x <=. 0.0
-
- to_real_negative :
- forall x:t19 [is_negative x].
- t'isFinite x -> t'real x <. 0.0 -> is_negative x
-
- negative_xor_positive : forall x:t19. not (is_positive x /\ is_negative x)
-
- negative_or_positive :
- forall x:t19. is_not_nan x -> is_positive x \/ is_negative x
-
- diff_sign_trans :
- forall x:t19, y:t19, z:t19.
- diff_sign x y /\ diff_sign y z -> same_sign x z
-
- diff_sign_product :
- forall x:t19, y:t19.
- t'isFinite x /\ t'isFinite y /\ (t'real x *. t'real y) <. 0.0 ->
- diff_sign x y
-
- same_sign_product :
- forall x:t19, y:t19.
- t'isFinite x /\ t'isFinite y /\ same_sign x y ->
- (t'real x *. t'real y) >=. 0.0
-
- predicate product_sign (z:t19) (x:t19) (y:t19) =
- (same_sign x y -> is_positive z) /\ (diff_sign x y -> is_negative z)
-
- predicate overflow_value (m:mode) (x:t19) =
- match m with
- | RTN ->
- if is_positive x then t'isFinite x /\ t'real x = max_real
- else is_infinite x
- | RTP ->
- if is_positive x then is_infinite x
- else t'isFinite x /\ t'real x = (-. max_real)
- | RTZ ->
- if is_positive x then t'isFinite x /\ t'real x = max_real
- else t'isFinite x /\ t'real x = (-. max_real)
- | RNA | RNE -> is_infinite x
- end
-
- predicate sign_zero_result (m:mode) (x:t19) =
- is_zero x -> match m with
- | RTN -> is_negative x
- | _ -> is_positive x
- end
-
- add_finite :
- forall m:mode, x:t19, y:t19 [add m x y].
- t'isFinite x ->
- t'isFinite y ->
- no_overflow m (t'real x +. t'real y) ->
- t'isFinite (add m x y) /\
- t'real (add m x y) = round m (t'real x +. t'real y)
-
- add_finite_rev :
- forall m:mode, x:t19, y:t19 [add m x y].
- t'isFinite (add m x y) -> t'isFinite x /\ t'isFinite y
-
- add_finite_rev_n :
- forall m:mode, x:t19, y:t19 [add m x y].
- to_nearest m ->
- t'isFinite (add m x y) ->
- no_overflow m (t'real x +. t'real y) /\
- t'real (add m x y) = round m (t'real x +. t'real y)
-
- sub_finite :
- forall m:mode, x:t19, y:t19 [sub m x y].
- t'isFinite x ->
- t'isFinite y ->
- no_overflow m (t'real x -. t'real y) ->
- t'isFinite (sub m x y) /\
- t'real (sub m x y) = round m (t'real x -. t'real y)
-
- sub_finite_rev :
- forall m:mode, x:t19, y:t19 [sub m x y].
- t'isFinite (sub m x y) -> t'isFinite x /\ t'isFinite y
-
- sub_finite_rev_n :
- forall m:mode, x:t19, y:t19 [sub m x y].
- to_nearest m ->
- t'isFinite (sub m x y) ->
- no_overflow m (t'real x -. t'real y) /\
- t'real (sub m x y) = round m (t'real x -. t'real y)
-
- mul_finite :
- forall m:mode, x:t19, y:t19 [mul m x y].
- t'isFinite x ->
- t'isFinite y ->
- no_overflow m (t'real x *. t'real y) ->
- t'isFinite (mul m x y) /\
- t'real (mul m x y) = round m (t'real x *. t'real y)
-
- mul_finite_rev :
- forall m:mode, x:t19, y:t19 [mul m x y].
- t'isFinite (mul m x y) -> t'isFinite x /\ t'isFinite y
-
- mul_finite_rev_n :
- forall m:mode, x:t19, y:t19 [mul m x y].
- to_nearest m ->
- t'isFinite (mul m x y) ->
- no_overflow m (t'real x *. t'real y) /\
- t'real (mul m x y) = round m (t'real x *. t'real y)
-
- div_finite :
- forall m:mode, x:t19, y:t19 [div m x y].
- t'isFinite x ->
- t'isFinite y ->
- not is_zero y ->
- no_overflow m (t'real x /. t'real y) ->
- t'isFinite (div m x y) /\
- t'real (div m x y) = round m (t'real x /. t'real y)
-
- div_finite_rev :
- forall m:mode, x:t19, y:t19 [div m x y].
- t'isFinite (div m x y) ->
- t'isFinite x /\ t'isFinite y /\ not is_zero y \/
- t'isFinite x /\ is_infinite y /\ t'real (div m x y) = 0.0
-
- div_finite_rev_n :
- forall m:mode, x:t19, y:t19 [div m x y].
- to_nearest m ->
- t'isFinite (div m x y) ->
- t'isFinite y ->
- no_overflow m (t'real x /. t'real y) /\
- t'real (div m x y) = round m (t'real x /. t'real y)
-
- neg_finite :
- forall x:t19 [neg x].
- t'isFinite x -> t'isFinite (neg x) /\ t'real (neg x) = (-. t'real x)
-
- neg_finite_rev :
- forall x:t19 [neg x].
- t'isFinite (neg x) -> t'isFinite x /\ t'real (neg x) = (-. t'real x)
-
- abs_finite :
- forall x:t19 [abs1 x].
- t'isFinite x ->
- t'isFinite (abs1 x) /\
- t'real (abs1 x) = abs (t'real x) /\ is_positive (abs1 x)
-
- abs_finite_rev :
- forall x:t19 [abs1 x].
- t'isFinite (abs1 x) -> t'isFinite x /\ t'real (abs1 x) = abs (t'real x)
-
- abs_universal : forall x:t19 [abs1 x]. not is_negative (abs1 x)
-
- fma_finite :
- forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
- t'isFinite x ->
- t'isFinite y ->
- t'isFinite z ->
- no_overflow m ((t'real x *. t'real y) +. t'real z) ->
- t'isFinite (fma m x y z) /\
- t'real (fma m x y z) = round m ((t'real x *. t'real y) +. t'real z)
-
- fma_finite_rev :
- forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
- t'isFinite (fma m x y z) -> t'isFinite x /\ t'isFinite y /\ t'isFinite z
-
- fma_finite_rev_n :
- forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
- to_nearest m ->
- t'isFinite (fma m x y z) ->
- no_overflow m ((t'real x *. t'real y) +. t'real z) /\
- t'real (fma m x y z) = round m ((t'real x *. t'real y) +. t'real z)
-
- function sqr (x:real) : real = x *''''' x
-
- function sqrt1 real : real
-
- axiom Sqrt_positive : forall x:real. x >=' 0.0 -> sqrt1 x >=' 0.0
-
- axiom Sqrt_square : forall x:real. x >=' 0.0 -> sqr (sqrt1 x) = x
-
- axiom Square_sqrt : forall x:real. x >=' 0.0 -> sqrt1 (x *''''' x) = x
-
- axiom Sqrt_mul :
- forall x:real, y:real.
- x >=' 0.0 /\ y >=' 0.0 -> sqrt1 (x *''''' y) = (sqrt1 x *''''' sqrt1 y)
-
- axiom Sqrt_le :
- forall x:real, y:real. 0.0 <='' x /\ x <='' y -> sqrt1 x <='' sqrt1 y
-
- (* use real.Square *)
-
- sqrt_finite :
- forall m:mode, x:t19 [sqrt m x].
- t'isFinite x ->
- t'real x >=. 0.0 ->
- t'isFinite (sqrt m x) /\ t'real (sqrt m x) = round m (sqrt1 (t'real x))
-
- sqrt_finite_rev :
- forall m:mode, x:t19 [sqrt m x].
- t'isFinite (sqrt m x) ->
- t'isFinite x /\
- t'real x >=. 0.0 /\ t'real (sqrt m x) = round m (sqrt1 (t'real x))
-
- predicate same_sign_real (x:t19) (r:real) =
- is_positive x /\ r >. 0.0 \/ is_negative x /\ r <. 0.0
-
- add_special :
- forall m:mode, x:t19, y:t19 [add m x y].
- let r = add m x y in
- (is_nan x \/ is_nan y -> is_nan r) /\
- (t'isFinite x /\ is_infinite y -> is_infinite r /\ same_sign r y) /\
- (is_infinite x /\ t'isFinite y -> is_infinite r /\ same_sign r x) /\
- (is_infinite x /\ is_infinite y /\ same_sign x y ->
- is_infinite r /\ same_sign r x) /\
- (is_infinite x /\ is_infinite y /\ diff_sign x y -> is_nan r) /\
- (t'isFinite x /\
- t'isFinite y /\ not no_overflow m (t'real x +. t'real y) ->
- same_sign_real r (t'real x +. t'real y) /\ overflow_value m r) /\
- (t'isFinite x /\ t'isFinite y ->
- (if same_sign x y then same_sign r x else sign_zero_result m r))
-
- sub_special :
- forall m:mode, x:t19, y:t19 [sub m x y].
- let r = sub m x y in
- (is_nan x \/ is_nan y -> is_nan r) /\
- (t'isFinite x /\ is_infinite y -> is_infinite r /\ diff_sign r y) /\
- (is_infinite x /\ t'isFinite y -> is_infinite r /\ same_sign r x) /\
- (is_infinite x /\ is_infinite y /\ same_sign x y -> is_nan r) /\
- (is_infinite x /\ is_infinite y /\ diff_sign x y ->
- is_infinite r /\ same_sign r x) /\
- (t'isFinite x /\
- t'isFinite y /\ not no_overflow m (t'real x -. t'real y) ->
- same_sign_real r (t'real x -. t'real y) /\ overflow_value m r) /\
- (t'isFinite x /\ t'isFinite y ->
- (if diff_sign x y then same_sign r x else sign_zero_result m r))
-
- mul_special :
- forall m:mode, x:t19, y:t19 [mul m x y].
- let r = mul m x y in
- (is_nan x \/ is_nan y -> is_nan r) /\
- (is_zero x /\ is_infinite y -> is_nan r) /\
- (t'isFinite x /\ is_infinite y /\ not is_zero x -> is_infinite r) /\
- (is_infinite x /\ is_zero y -> is_nan r) /\
- (is_infinite x /\ t'isFinite y /\ not is_zero y -> is_infinite r) /\
- (is_infinite x /\ is_infinite y -> is_infinite r) /\
- (t'isFinite x /\
- t'isFinite y /\ not no_overflow m (t'real x *. t'real y) ->
- overflow_value m r) /\
- (not is_nan r -> product_sign r x y)
-
- div_special :
- forall m:mode, x:t19, y:t19 [div m x y].
- let r = div m x y in
- (is_nan x \/ is_nan y -> is_nan r) /\
- (t'isFinite x /\ is_infinite y -> is_zero r) /\
- (is_infinite x /\ t'isFinite y -> is_infinite r) /\
- (is_infinite x /\ is_infinite y -> is_nan r) /\
- (t'isFinite x /\
- t'isFinite y /\
- not is_zero y /\ not no_overflow m (t'real x /. t'real y) ->
- overflow_value m r) /\
- (t'isFinite x /\ is_zero y /\ not is_zero x -> is_infinite r) /\
- (is_zero x /\ is_zero y -> is_nan r) /\
- (not is_nan r -> product_sign r x y)
-
- neg_special :
- forall x:t19 [neg x].
- (is_nan x -> is_nan (neg x)) /\
- (is_infinite x -> is_infinite (neg x)) /\
- (not is_nan x -> diff_sign x (neg x))
-
- abs_special :
- forall x:t19 [abs1 x].
- (is_nan x -> is_nan (abs1 x)) /\
- (is_infinite x -> is_infinite (abs1 x)) /\
- (not is_nan x -> is_positive (abs1 x))
-
- fma_special :
- forall m:mode, x:t19, y:t19, z:t19 [fma m x y z].
- let r = fma m x y z in
- (is_nan x \/ is_nan y \/ is_nan z -> is_nan r) /\
- (is_zero x /\ is_infinite y -> is_nan r) /\
- (is_infinite x /\ is_zero y -> is_nan r) /\
- (t'isFinite x /\ not is_zero x /\ is_infinite y /\ t'isFinite z ->
- is_infinite r /\ product_sign r x y) /\
- (t'isFinite x /\ not is_zero x /\ is_infinite y /\ is_infinite z ->
- (if product_sign z x y then is_infinite r /\ same_sign r z
- else is_nan r)) /\
- (is_infinite x /\ t'isFinite y /\ not is_zero y /\ t'isFinite z ->
- is_infinite r /\ product_sign r x y) /\
- (is_infinite x /\ t'isFinite y /\ not is_zero y /\ is_infinite z ->
- (if product_sign z x y then is_infinite r /\ same_sign r z
- else is_nan r)) /\
- (is_infinite x /\ is_infinite y /\ t'isFinite z ->
- is_infinite r /\ product_sign r x y) /\
- (t'isFinite x /\ t'isFinite y /\ is_infinite z ->
- is_infinite r /\ same_sign r z) /\
- (is_infinite x /\ is_infinite y /\ is_infinite z ->
- (if product_sign z x y then is_infinite r /\ same_sign r z
- else is_nan r)) /\
- (t'isFinite x /\
- t'isFinite y /\
- t'isFinite z /\ not no_overflow m ((t'real x *. t'real y) +. t'real z) ->
- same_sign_real r ((t'real x *. t'real y) +. t'real z) /\
- overflow_value m r) /\
- (t'isFinite x /\ t'isFinite y /\ t'isFinite z ->
- (if product_sign z x y then same_sign r z
- else ((t'real x *. t'real y) +. t'real z) = 0.0 ->
- (if m = RTN then is_negative r else is_positive r)))
-
- sqrt_special :
- forall m:mode, x:t19 [sqrt m x].
- let r = sqrt m x in
- (is_nan x -> is_nan r) /\
- (is_plus_infinity x -> is_plus_infinity r) /\
- (is_minus_infinity x -> is_nan r) /\
- (t'isFinite x /\ t'real x <. 0.0 -> is_nan r) /\
- (is_zero x -> same_sign r x) /\
- (t'isFinite x /\ t'real x >. 0.0 -> is_positive r)
-
- of_int_add_exact :
- forall m:mode, n:mode, i:int, j:int.
- in_safe_int_range i ->
- in_safe_int_range j ->
- in_safe_int_range (i + j) ->
- eq (of_int m (i + j)) (add n (of_int m i) (of_int m j))
-
- of_int_sub_exact :
- forall m:mode, n:mode, i:int, j:int.
- in_safe_int_range i ->
- in_safe_int_range j ->
- in_safe_int_range (i - j) ->
- eq (of_int m (i - j)) (sub n (of_int m i) (of_int m j))
-
- of_int_mul_exact :
- forall m:mode, n:mode, i:int, j:int.
- in_safe_int_range i ->
- in_safe_int_range j ->
- in_safe_int_range (i * j) ->
- eq (of_int m (i * j)) (mul n (of_int m i) (of_int m j))
-
- Min_r : forall x:t19, y:t19. y .<= x -> min x y .= y
-
- Min_l : forall x:t19, y:t19. x .<= y -> min x y .= x
-
- Max_r : forall x:t19, y:t19. y .<= x -> max x y .= x
-
- Max_l : forall x:t19, y:t19. x .<= y -> max x y .= y
-
- predicate is_int t19
-
- zeroF_is_int : is_int zeroF
-
- of_int_is_int : forall m:mode, x:int. in_int_range x -> is_int (of_int m x)
-
- big_float_is_int :
- forall m:mode, i:t19.
- t'isFinite i ->
- i .<= neg (of_int m pow2sb) \/ of_int m pow2sb .<= i -> is_int i
-
- roundToIntegral_is_int :
- forall m:mode, x:t19. t'isFinite x -> is_int (roundToIntegral m x)
-
- eq_is_int : forall x:t19, y:t19. eq x y -> is_int x -> is_int y
-
- add_int :
- forall x:t19, y:t19, m:mode.
- is_int x -> is_int y -> t'isFinite (add m x y) -> is_int (add m x y)
-
- sub_int :
- forall x:t19, y:t19, m:mode.
- is_int x -> is_int y -> t'isFinite (sub m x y) -> is_int (sub m x y)
-
- mul_int :
- forall x:t19, y:t19, m:mode.
- is_int x -> is_int y -> t'isFinite (mul m x y) -> is_int (mul m x y)
-
- fma_int :
- forall x:t19, y:t19, z:t19, m:mode.
- is_int x ->
- is_int y -> is_int z -> t'isFinite (fma m x y z) -> is_int (fma m x y z)
-
- neg_int : forall x:t19. is_int x -> is_int (neg x)
-
- abs_int : forall x:t19. is_int x -> is_int (abs1 x)
-
- is_int_of_int :
- forall x:t19, m:mode, m':mode. is_int x -> eq x (of_int m' (to_int m x))
-
- is_int_to_int : forall m:mode, x:t19. is_int x -> in_int_range (to_int m x)
-
- is_int_is_finite : forall x:t19. is_int x -> t'isFinite x
-
- int_to_real :
- forall m:mode, x:t19. is_int x -> t'real x = from_int (to_int m x)
-
- truncate_int : forall m:mode, i:t19. is_int i -> roundToIntegral m i .= i
-
- truncate_neg :
- forall x:t19.
- t'isFinite x ->
- is_negative x -> roundToIntegral RTZ x = roundToIntegral RTP x
-
- truncate_pos :
- forall x:t19.
- t'isFinite x ->
- is_positive x -> roundToIntegral RTZ x = roundToIntegral RTN x
-
- ceil_le : forall x:t19. t'isFinite x -> x .<= roundToIntegral RTP x
-
- ceil_lest :
- forall x:t19, y:t19. x .<= y /\ is_int y -> roundToIntegral RTP x .<= y
-
- ceil_to_real :
- forall x:t19.
- t'isFinite x ->
- t'real (roundToIntegral RTP x) = from_int (ceil (t'real x))
-
- ceil_to_int :
- forall m:mode, x:t19.
- t'isFinite x -> to_int m (roundToIntegral RTP x) = ceil (t'real x)
-
- floor_le : forall x:t19. t'isFinite x -> roundToIntegral RTN x .<= x
-
- floor_lest :
- forall x:t19, y:t19. y .<= x /\ is_int y -> y .<= roundToIntegral RTN x
-
- floor_to_real :
- forall x:t19.
- t'isFinite x ->
- t'real (roundToIntegral RTN x) = from_int (floor (t'real x))
-
- floor_to_int :
- forall m:mode, x:t19.
- t'isFinite x -> to_int m (roundToIntegral RTN x) = floor (t'real x)
-
- RNA_down :
- forall x:t19.
- (x .- roundToIntegral RTN x) .< (roundToIntegral RTP x .- x) ->
- roundToIntegral RNA x = roundToIntegral RTN x
-
- RNA_up :
- forall x:t19.
- (x .- roundToIntegral RTN x) .> (roundToIntegral RTP x .- x) ->
- roundToIntegral RNA x = roundToIntegral RTP x
-
- RNA_down_tie :
- forall x:t19.
- (x .- roundToIntegral RTN x) .= (roundToIntegral RTP x .- x) ->
- is_negative x -> roundToIntegral RNA x = roundToIntegral RTN x
-
- RNA_up_tie :
- forall x:t19.
- (roundToIntegral RTP x .- x) .= (x .- roundToIntegral RTN x) ->
- is_positive x -> roundToIntegral RNA x = roundToIntegral RTP x
-
- to_int_roundToIntegral :
- forall m:mode, x:t19. to_int m x = to_int m (roundToIntegral m x)
-
- to_int_monotonic :
- forall m:mode, x:t19, y:t19.
- t'isFinite x -> t'isFinite y -> le x y -> to_int m x <= to_int m y
-
- to_int_of_int :
- forall m:mode, i:int. in_safe_int_range i -> to_int m (of_int m i) = i
-
- eq_to_int :
- forall m:mode, x:t19, y:t19.
- t'isFinite x -> x .= y -> to_int m x = to_int m y
-
- neg_to_int :
- forall m:mode, x:t19. is_int x -> to_int m (neg x) = (- to_int m x)
-
- roundToIntegral_is_finite :
- forall m:mode, x:t19. t'isFinite x -> t'isFinite (roundToIntegral m x)
-
- (* clone ieee_float.GenericFloat with type t20 = t19,
- predicate is_int1 = is_int, predicate same_sign_real1 = same_sign_real,
- predicate sign_zero_result1 = sign_zero_result,
- predicate overflow_value1 = overflow_value,
- predicate product_sign1 = product_sign, predicate diff_sign1 = diff_sign,
- predicate same_sign1 = same_sign,
- predicate in_safe_int_range1 = in_safe_int_range,
- constant pow2sb1 = pow2sb, predicate no_overflow1 = no_overflow,
- predicate in_int_range1 = in_int_range, predicate in_range1 = in_range,
- constant emax1 = emax, constant max_int1 = max_int,
- constant max_real1 = max_real, function round1 = round,
- function to_int1 = to_int, function of_int1 = of_int,
- function to_real = t'real, predicate is_not_nan1 = is_not_nan,
- predicate is_minus_zero1 = is_minus_zero,
- predicate is_plus_zero1 = is_plus_zero,
- predicate is_minus_infinity1 = is_minus_infinity,
- predicate is_plus_infinity1 = is_plus_infinity,
- predicate is_finite = t'isFinite, predicate is_negative1 = is_negative,
- predicate is_positive1 = is_positive, predicate is_nan1 = is_nan,
- predicate is_infinite1 = is_infinite, predicate is_zero1 = is_zero,
- predicate is_subnormal1 = is_subnormal, predicate is_normal1 = is_normal,
- predicate (.=') = (.=), predicate (.>') = (.>), predicate (.>=') = (.>=),
- predicate (.<') = (.<), predicate (.<=') = (.<=), predicate eq1 = eq,
- predicate gt1 = gt, predicate ge1 = ge, predicate lt1 = lt,
- predicate le1 = le, function max1 = max, function min1 = min,
- function roundToIntegral1 = roundToIntegral, function (./') = (./),
- function (.*') = (.* ), function (.-') = (.-), function (.+') = (.+),
- function (.-'_) = (.-_), function sqrt2 = sqrt, function fma1 = fma,
- function neg1 = neg, function abs2 = abs1, function div1 = div,
- function mul1 = mul, function sub1 = sub, function add1 = add,
- constant zeroF1 = zeroF, constant sb = t'sb, constant eb = t'eb,
- prop roundToIntegral_is_finite1 = roundToIntegral_is_finite,
- prop neg_to_int1 = neg_to_int, prop eq_to_int1 = eq_to_int,
- prop to_int_of_int1 = to_int_of_int,
- prop to_int_monotonic1 = to_int_monotonic,
- prop to_int_roundToIntegral1 = to_int_roundToIntegral,
- prop RNA_up_tie1 = RNA_up_tie, prop RNA_down_tie1 = RNA_down_tie,
- prop RNA_up1 = RNA_up, prop RNA_down1 = RNA_down,
- prop floor_to_int1 = floor_to_int, prop floor_to_real1 = floor_to_real,
- prop floor_lest1 = floor_lest, prop floor_le1 = floor_le,
- prop ceil_to_int1 = ceil_to_int, prop ceil_to_real1 = ceil_to_real,
- prop ceil_lest1 = ceil_lest, prop ceil_le1 = ceil_le,
- prop truncate_pos1 = truncate_pos, prop truncate_neg1 = truncate_neg,
- prop truncate_int1 = truncate_int, prop int_to_real1 = int_to_real,
- prop is_int_is_finite1 = is_int_is_finite,
- prop is_int_to_int1 = is_int_to_int, prop is_int_of_int1 = is_int_of_int,
- prop abs_int1 = abs_int, prop neg_int1 = neg_int,
- prop fma_int1 = fma_int, prop mul_int1 = mul_int,
- prop sub_int1 = sub_int, prop add_int1 = add_int,
- prop eq_is_int1 = eq_is_int,
- prop roundToIntegral_is_int1 = roundToIntegral_is_int,
- prop big_float_is_int1 = big_float_is_int,
- prop of_int_is_int1 = of_int_is_int, prop zeroF_is_int1 = zeroF_is_int,
- prop Max_l1 = Max_l, prop Max_r1 = Max_r, prop Min_l1 = Min_l,
- prop Min_r1 = Min_r, prop of_int_mul_exact1 = of_int_mul_exact,
- prop of_int_sub_exact1 = of_int_sub_exact,
- prop of_int_add_exact1 = of_int_add_exact,
- prop sqrt_special1 = sqrt_special, prop fma_special1 = fma_special,
- prop abs_special1 = abs_special, prop neg_special1 = neg_special,
- prop div_special1 = div_special, prop mul_special1 = mul_special,
- prop sub_special1 = sub_special, prop add_special1 = add_special,
- prop sqrt_finite_rev1 = sqrt_finite_rev, prop sqrt_finite1 = sqrt_finite,
- prop fma_finite_rev_n1 = fma_finite_rev_n,
- prop fma_finite_rev1 = fma_finite_rev, prop fma_finite1 = fma_finite,
- prop abs_universal1 = abs_universal,
- prop abs_finite_rev1 = abs_finite_rev, prop abs_finite1 = abs_finite,
- prop neg_finite_rev1 = neg_finite_rev, prop neg_finite1 = neg_finite,
- prop div_finite_rev_n1 = div_finite_rev_n,
- prop div_finite_rev1 = div_finite_rev, prop div_finite1 = div_finite,
- prop mul_finite_rev_n1 = mul_finite_rev_n,
- prop mul_finite_rev1 = mul_finite_rev, prop mul_finite1 = mul_finite,
- prop sub_finite_rev_n1 = sub_finite_rev_n,
- prop sub_finite_rev1 = sub_finite_rev, prop sub_finite1 = sub_finite,
- prop add_finite_rev_n1 = add_finite_rev_n,
- prop add_finite_rev1 = add_finite_rev, prop add_finite1 = add_finite,
- prop same_sign_product1 = same_sign_product,
- prop diff_sign_product1 = diff_sign_product,
- prop diff_sign_trans1 = diff_sign_trans,
- prop negative_or_positive1 = negative_or_positive,
- prop negative_xor_positive1 = negative_xor_positive,
- prop to_real_negative1 = to_real_negative,
- prop negative_to_real1 = negative_to_real,
- prop to_real_positive1 = to_real_positive,
- prop positive_to_real1 = positive_to_real,
- prop lt_lt_finite1 = lt_lt_finite, prop lt_special1 = lt_special,
- prop le_special1 = le_special, prop not_gt_le1 = not_gt_le,
- prop not_lt_ge1 = not_lt_ge, prop le_ge_asym1 = le_ge_asym,
- prop lt_le_trans1 = lt_le_trans, prop le_lt_trans1 = le_lt_trans,
- prop le_finite1 = le_finite, prop lt_finite1 = lt_finite,
- prop eq_special1 = eq_special,
- prop eq_to_real_finite1 = eq_to_real_finite, prop eq_zero1 = eq_zero,
- prop eq_trans1 = eq_trans, prop eq_sym1 = eq_sym,
- prop eq_refl1 = eq_refl, prop eq_feq1 = eq_feq, prop feq_eq1 = feq_eq,
- prop Exact_rounding_for_integers1 = Exact_rounding_for_integers,
- prop pow2sb = pow2sb1, prop Round_up_neg1 = Round_up_neg,
- prop Round_down_neg1 = Round_down_neg, prop Round_up_ge1 = Round_up_ge,
- prop Round_down_le1 = Round_down_le, prop Round_to_real1 = Round_to_real,
- prop Round_idempotent1 = Round_idempotent,
- prop Round_monotonic1 = Round_monotonic,
- prop Bounded_real_no_overflow1 = Bounded_real_no_overflow,
- prop is_finite1 = is_finite, prop max_real_int1 = max_real_int,
- prop max_int = max_int1, prop zero_of_int1 = zero_of_int,
- prop zero_to_real1 = zero_to_real, prop zeroF_is_zero1 = zeroF_is_zero,
- prop zeroF_is_positive1 = zeroF_is_positive,
- prop is_not_finite1 = is_not_finite, prop is_not_nan1 = is_not_nan,
- prop sb_gt_1 = sb_gt_11, prop eb_gt_1 = eb_gt_11, *)
-
- round_bound_ne :
- forall x:real [round RNE x].
- no_overflow RNE x ->
- ((x -' (0x1.0p-53 *''''' abs x)) -' 0x1.0p-1075) <='' round RNE x /\
- round RNE x
- <='' ((x +''''' (0x1.0p-53 *''''' abs x)) +''''' 0x1.0p-1075)
-
- round_bound :
- forall m:mode, x:real [round m x].
- no_overflow m x ->
- ((x -' (0x1.0p-52 *''''' abs x)) -' 0x1.0p-1074) <='' round m x /\
- round m x <='' ((x +''''' (0x1.0p-52 *''''' abs x)) +''''' 0x1.0p-1074)
-
- (* use ieee_float.Float64 *)
-
- type input_type = t19
-
- (* use caisar.NNet *)
-
- type tuple5 'a 'a1 'a2 'a3 'a4 =
- | Tuple5 'a 'a1 'a2 'a3 'a4
-
- (* use why3.Tuple5.Tuple51 *)
-
- function nnet_apply t19 t19 t19 t19 t19 : (t19, t19, t19, t19, t19)
-
- (* use As_tuple *)
-
- goal G :
- forall x1:t19, x2:t19, x3:t19, x4:t19, x5:t19.
- match nnet_apply x1 x2 x3 x4 x5 with
- | y1, _, _, _, _ -> 0.0 <. t'real y1 /\ t'real y1 <. 0.1
- end
- end
+ <autodetect>0 prover(s) added
+ <autodetect>Generating strategies:
+ <autodetect>Run: (alt-ergo --version) > /tmp/build71161f.dune/out615f55 2>&1
+ <autodetect>Run: (alt-ergo-2.4.0 --version) > /tmp/build71161f.dune/outd1f15f 2>&1
+ <autodetect>command 'alt-ergo-2.4.0 --version' failed. Output:
+ sh: 1: alt-ergo-2.4.0: not found
+
+ <autodetect>Found prover Alt-Ergo version 2.4.0, OK.
+ <autodetect>1 prover(s) added
+ (* this is the prelude for Alt-Ergo, version >= 2.4.0 *)
+ (* this is a prelude for Alt-Ergo integer arithmetic *)
+ (* this is a prelude for Alt-Ergo real arithmetic *)
+ type string
+
+ logic match_bool : bool, 'a, 'a -> 'a
+
+ axiom match_bool_True :
+ (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))
+
+ axiom match_bool_False :
+ (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))
+
+ axiom CompatOrderMult :
+ (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) ->
+ ((x * z) <= (y * z)))))
+
+ axiom add_div :
+ (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
+ (((x + y) / z) = ((x / z) + (y / z)))))
+
+ axiom sub_div :
+ (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
+ (((x - y) / z) = ((x / z) - (y / z)))))
+
+ axiom neg_div :
+ (forall x:real. forall y:real. ((not (y = 0.0)) ->
+ (((-x) / y) = (-(x / y)))))
+
+ axiom assoc_mul_div :
+ (forall x:real. forall y:real. forall z:real. ((not (z = 0.0)) ->
+ (((x * y) / z) = (x * (y / z)))))
+
+ axiom assoc_div_mul :
+ (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
+ (not (z = 0.0))) -> (((x / y) / z) = (x / (y * z)))))
+
+ axiom assoc_div_div :
+ (forall x:real. forall y:real. forall z:real. (((not (y = 0.0)) and
+ (not (z = 0.0))) -> ((x / (y / z)) = ((x * z) / y))))
+
+ axiom CompatOrderMult1 :
+ (forall x:real. forall y:real. forall z:real. ((x <= y) -> ((0.0 <= z) ->
+ ((x * z) <= (y * z)))))
+
+ type t
+
+ logic tqtreal : t -> real
+
+ logic tqtisFinite : t -> prop
+
+ axiom tqtaxiom :
+ (forall x:t. (tqtisFinite(x) ->
+ ((-179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) <= tqtreal(x))))
+
+ axiom tqtaxiom1 :
+ (forall x:t. (tqtisFinite(x) ->
+ (tqtreal(x) <= 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)))
+
+ logic pow2 : int -> int
+
+ axiom Power_0 : (pow2(0) = 1)
+
+ axiom Power_s : (forall n:int. ((0 <= n) -> (pow2((n + 1)) = (2 * pow2(n)))))
+
+ axiom Power_1 : (pow2(1) = 2)
+
+ axiom Power_sum :
+ (forall n:int. forall m:int. (((0 <= n) and (0 <= m)) ->
+ (pow2((n + m)) = (pow2(n) * pow2(m)))))
+
+ axiom pow2pos : (forall i:int. ((0 <= i) -> (0 < pow2(i))))
+
+ axiom pow2_0 : (pow2(0) = 1)
+
+ axiom pow2_1 : (pow2(1) = 2)
+
+ axiom pow2_2 : (pow2(2) = 4)
+
+ axiom pow2_3 : (pow2(3) = 8)
+
+ axiom pow2_4 : (pow2(4) = 16)
+
+ axiom pow2_5 : (pow2(5) = 32)
+
+ axiom pow2_6 : (pow2(6) = 64)
+
+ axiom pow2_7 : (pow2(7) = 128)
+
+ axiom pow2_8 : (pow2(8) = 256)
+
+ axiom pow2_9 : (pow2(9) = 512)
+
+ axiom pow2_10 : (pow2(10) = 1024)
+
+ axiom pow2_11 : (pow2(11) = 2048)
+
+ axiom pow2_12 : (pow2(12) = 4096)
+
+ axiom pow2_13 : (pow2(13) = 8192)
+
+ axiom pow2_14 : (pow2(14) = 16384)
+
+ axiom pow2_15 : (pow2(15) = 32768)
+
+ axiom pow2_16 : (pow2(16) = 65536)
+
+ axiom pow2_17 : (pow2(17) = 131072)
+
+ axiom pow2_18 : (pow2(18) = 262144)
+
+ axiom pow2_19 : (pow2(19) = 524288)
+
+ axiom pow2_20 : (pow2(20) = 1048576)
+
+ axiom pow2_21 : (pow2(21) = 2097152)
+
+ axiom pow2_22 : (pow2(22) = 4194304)
+
+ axiom pow2_23 : (pow2(23) = 8388608)
+
+ axiom pow2_24 : (pow2(24) = 16777216)
+
+ axiom pow2_25 : (pow2(25) = 33554432)
+
+ axiom pow2_26 : (pow2(26) = 67108864)
+
+ axiom pow2_27 : (pow2(27) = 134217728)
+
+ axiom pow2_28 : (pow2(28) = 268435456)
+
+ axiom pow2_29 : (pow2(29) = 536870912)
+
+ axiom pow2_30 : (pow2(30) = 1073741824)
+
+ axiom pow2_31 : (pow2(31) = 2147483648)
+
+ axiom pow2_32 : (pow2(32) = 4294967296)
+
+ axiom pow2_33 : (pow2(33) = 8589934592)
+
+ axiom pow2_34 : (pow2(34) = 17179869184)
+
+ axiom pow2_35 : (pow2(35) = 34359738368)
+
+ axiom pow2_36 : (pow2(36) = 68719476736)
+
+ axiom pow2_37 : (pow2(37) = 137438953472)
+
+ axiom pow2_38 : (pow2(38) = 274877906944)
+
+ axiom pow2_39 : (pow2(39) = 549755813888)
+
+ axiom pow2_40 : (pow2(40) = 1099511627776)
+
+ axiom pow2_41 : (pow2(41) = 2199023255552)
+
+ axiom pow2_42 : (pow2(42) = 4398046511104)
+
+ axiom pow2_43 : (pow2(43) = 8796093022208)
+
+ axiom pow2_44 : (pow2(44) = 17592186044416)
+
+ axiom pow2_45 : (pow2(45) = 35184372088832)
+
+ axiom pow2_46 : (pow2(46) = 70368744177664)
+
+ axiom pow2_47 : (pow2(47) = 140737488355328)
+
+ axiom pow2_48 : (pow2(48) = 281474976710656)
+
+ axiom pow2_49 : (pow2(49) = 562949953421312)
+
+ axiom pow2_50 : (pow2(50) = 1125899906842624)
+
+ axiom pow2_51 : (pow2(51) = 2251799813685248)
+
+ axiom pow2_52 : (pow2(52) = 4503599627370496)
+
+ axiom pow2_53 : (pow2(53) = 9007199254740992)
+
+ axiom pow2_54 : (pow2(54) = 18014398509481984)
+
+ axiom pow2_55 : (pow2(55) = 36028797018963968)
+
+ axiom pow2_56 : (pow2(56) = 72057594037927936)
+
+ axiom pow2_57 : (pow2(57) = 144115188075855872)
+
+ axiom pow2_58 : (pow2(58) = 288230376151711744)
+
+ axiom pow2_59 : (pow2(59) = 576460752303423488)
+
+ axiom pow2_60 : (pow2(60) = 1152921504606846976)
+
+ axiom pow2_61 : (pow2(61) = 2305843009213693952)
+
+ axiom pow2_62 : (pow2(62) = 4611686018427387904)
+
+ axiom pow2_63 : (pow2(63) = 9223372036854775808)
+
+ axiom pow2_64 : (pow2(64) = 18446744073709551616)
+
+ function abs(x: real) : real = (if (0.0 <= x) then x else (-x))
+
+ axiom Abs_le : (forall x:real. forall y:real. ((abs(x) <= y) -> ((-y) <= x)))
+
+ axiom Abs_le1 : (forall x:real. forall y:real. ((abs(x) <= y) -> (x <= y)))
+
+ axiom Abs_le2 :
+ (forall x:real. forall y:real. ((((-y) <= x) and (x <= y)) ->
+ (abs(x) <= y)))
+
+ axiom Abs_pos : (forall x:real. (0.0 <= abs(x)))
+
+ axiom Abs_sum :
+ (forall x:real. forall y:real. (abs((x + y)) <= (abs(x) + abs(y))))
+
+ axiom Abs_prod :
+ (forall x:real. forall y:real. (abs((x * y)) = (abs(x) * abs(y))))
+
+ axiom triangular_inequality :
+ (forall x:real. forall y:real. forall z:real.
+ (abs((x - z)) <= (abs((x - y)) + abs((y - z)))))
+
+ logic from_int : int -> real
+
+ axiom Zero : (from_int(0) = 0.0)
+
+ axiom One : (from_int(1) = 1.0)
+
+ axiom Add :
+ (forall x:int. forall y:int.
+ (from_int((x + y)) = (from_int(x) + from_int(y))))
+
+ axiom Sub :
+ (forall x:int. forall y:int.
+ (from_int((x - y)) = (from_int(x) - from_int(y))))
+
+ axiom Mul :
+ (forall x:int. forall y:int.
+ (from_int((x * y)) = (from_int(x) * from_int(y))))
+
+ axiom Neg : (forall x:int. (from_int((-x)) = (-from_int(x))))
+
+ axiom Injective :
+ (forall x:int. forall y:int. ((from_int(x) = from_int(y)) -> (x = y)))
+
+ axiom Monotonic :
+ (forall x:int. forall y:int. ((x <= y) -> (from_int(x) <= from_int(y))))
+
+ logic truncate : real -> int
+
+ axiom Truncate_int : (forall i:int. (truncate(from_int(i)) = i))
+
+ axiom Truncate_down_pos :
+ (forall x:real. ((0.0 <= x) -> (from_int(truncate(x)) <= x)))
+
+ axiom Truncate_down_pos1 :
+ (forall x:real. ((0.0 <= x) -> (x < from_int((truncate(x) + 1)))))
+
+ axiom Truncate_up_neg :
+ (forall x:real. ((x <= 0.0) -> (from_int((truncate(x) - 1)) < x)))
+
+ axiom Truncate_up_neg1 :
+ (forall x:real. ((x <= 0.0) -> (x <= from_int(truncate(x)))))
+
+ axiom Real_of_truncate :
+ (forall x:real. ((x - 1.0) <= from_int(truncate(x))))
+
+ axiom Real_of_truncate1 :
+ (forall x:real. (from_int(truncate(x)) <= (x + 1.0)))
+
+ axiom Truncate_monotonic :
+ (forall x:real. forall y:real. ((x <= y) -> (truncate(x) <= truncate(y))))
+
+ axiom Truncate_monotonic_int1 :
+ (forall x:real. forall i:int. ((x <= from_int(i)) -> (truncate(x) <= i)))
+
+ axiom Truncate_monotonic_int2 :
+ (forall x:real. forall i:int. ((from_int(i) <= x) -> (i <= truncate(x))))
+
+ logic floor : real -> int
+
+ logic ceil : real -> int
+
+ axiom Floor_int : (forall i:int. (floor(from_int(i)) = i))
+
+ axiom Ceil_int : (forall i:int. (ceil(from_int(i)) = i))
+
+ axiom Floor_down : (forall x:real. (from_int(floor(x)) <= x))
+
+ axiom Floor_down1 : (forall x:real. (x < from_int((floor(x) + 1))))
+
+ axiom Ceil_up : (forall x:real. (from_int((ceil(x) - 1)) < x))
+
+ axiom Ceil_up1 : (forall x:real. (x <= from_int(ceil(x))))
+
+ axiom Floor_monotonic :
+ (forall x:real. forall y:real. ((x <= y) -> (floor(x) <= floor(y))))
+
+ axiom Ceil_monotonic :
+ (forall x:real. forall y:real. ((x <= y) -> (ceil(x) <= ceil(y))))
+
+ type mode = RNE | RNA | RTP | RTN | RTZ
+
+ logic match_mode : mode, 'a, 'a, 'a, 'a, 'a -> 'a
+
+ axiom match_mode_RNE :
+ (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
+ (match_mode(RNE, z, z1, z2, z3, z4) = z))
+
+ axiom match_mode_RNA :
+ (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
+ (match_mode(RNA, z, z1, z2, z3, z4) = z1))
+
+ axiom match_mode_RTP :
+ (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
+ (match_mode(RTP, z, z1, z2, z3, z4) = z2))
+
+ axiom match_mode_RTN :
+ (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
+ (match_mode(RTN, z, z1, z2, z3, z4) = z3))
+
+ axiom match_mode_RTZ :
+ (forall z:'a. forall z1:'a. forall z2:'a. forall z3:'a. forall z4:'a.
+ (match_mode(RTZ, z, z1, z2, z3, z4) = z4))
+
+ predicate to_nearest(m: mode) = ((m = RNE) or (m = RNA))
+
+ logic zeroF : t
+
+ logic add : mode, t, t -> t
+
+ logic sub : mode, t, t -> t
+
+ logic mul : mode, t, t -> t
+
+ logic div : mode, t, t -> t
+
+ logic abs1 : t -> t
+
+ logic neg : t -> t
+
+ logic fma : mode, t, t, t -> t
+
+ logic sqrt : mode, t -> t
+
+ logic roundToIntegral : mode, t -> t
+
+ logic min : t, t -> t
+
+ logic max : t, t -> t
+
+ logic le : t, t -> prop
+
+ logic lt : t, t -> prop
+
+ logic eq : t, t -> prop
+
+ logic is_normal : t -> prop
+
+ logic is_subnormal : t -> prop
+
+ logic is_zero : t -> prop
+
+ logic is_infinite : t -> prop
+
+ logic is_nan : t -> prop
+
+ logic is_positive : t -> prop
+
+ logic is_negative : t -> prop
+
+ predicate is_plus_infinity(x: t) = (is_infinite(x) and is_positive(x))
+
+ predicate is_minus_infinity(x: t) = (is_infinite(x) and is_negative(x))
+
+ predicate is_plus_zero(x: t) = (is_zero(x) and is_positive(x))
+
+ predicate is_minus_zero(x: t) = (is_zero(x) and is_negative(x))
+
+ predicate is_not_nan(x: t) = (tqtisFinite(x) or is_infinite(x))
+
+ axiom is_not_nan1 : (forall x:t. (is_not_nan(x) -> (not is_nan(x))))
+
+ axiom is_not_nan2 : (forall x:t. ((not is_nan(x)) -> is_not_nan(x)))
+
+ axiom is_not_finite :
+ (forall x:t. ((not tqtisFinite(x)) -> (is_infinite(x) or is_nan(x))))
+
+ axiom is_not_finite1 :
+ (forall x:t. ((is_infinite(x) or is_nan(x)) -> (not tqtisFinite(x))))
+
+ axiom zeroF_is_positive : is_positive(zeroF)
+
+ axiom zeroF_is_zero : is_zero(zeroF)
+
+ axiom zero_to_real :
+ (forall x:t [is_zero(x)]. (is_zero(x) -> tqtisFinite(x)))
+
+ axiom zero_to_real1 :
+ (forall x:t [is_zero(x)]. (is_zero(x) -> (tqtreal(x) = 0.0)))
+
+ axiom zero_to_real2 :
+ (forall x:t [is_zero(x)]. ((tqtisFinite(x) and (tqtreal(x) = 0.0)) ->
+ is_zero(x)))
+
+ logic of_int : mode, int -> t
+
+ logic to_int : mode, t -> int
+
+ axiom zero_of_int : (forall m:mode. (zeroF = of_int(m, 0)))
+
+ logic round : mode, real -> real
+
+ logic max_int1 : int
+
+ axiom max_real_int : (0x1.FFFFFFFFFFFFFp1023 = from_int(max_int1))
+
+ predicate in_range(x: real) = (((-0x1.FFFFFFFFFFFFFp1023) <= x) and
+ (x <= 0x1.FFFFFFFFFFFFFp1023))
+
+ predicate in_int_range(i: int) = (((-max_int1) <= i) and (i <= max_int1))
+
+ axiom is_finite : (forall x:t. (tqtisFinite(x) -> in_range(tqtreal(x))))
+
+ predicate no_overflow(m: mode, x: real) = in_range(round(m, x))
+
+ axiom Bounded_real_no_overflow :
+ (forall m:mode. forall x:real. (in_range(x) -> no_overflow(m, x)))
+
+ axiom Round_monotonic :
+ (forall m:mode. forall x:real. forall y:real. ((x <= y) -> (round(m,
+ x) <= round(m, y))))
+
+ axiom Round_idempotent :
+ (forall m1:mode. forall m2:mode. forall x:real. (round(m1, round(m2,
+ x)) = round(m2, x)))
+
+ axiom Round_to_real :
+ (forall m:mode. forall x:t. (tqtisFinite(x) -> (round(m,
+ tqtreal(x)) = tqtreal(x))))
+
+ axiom Round_down_le : (forall x:real. (round(RTN, x) <= x))
+
+ axiom Round_up_ge : (forall x:real. (x <= round(RTP, x)))
+
+ axiom Round_down_neg : (forall x:real. (round(RTN, (-x)) = (-round(RTP, x))))
+
+ axiom Round_up_neg : (forall x:real. (round(RTP, (-x)) = (-round(RTN, x))))
+
+ predicate in_safe_int_range(i: int) = (((-9007199254740992) <= i) and
+ (i <= 9007199254740992))
+
+ axiom Exact_rounding_for_integers :
+ (forall m:mode. forall i:int. (in_safe_int_range(i) -> (round(m,
+ from_int(i)) = from_int(i))))
+
+ predicate same_sign(x: t, y: t) = ((is_positive(x) and is_positive(y)) or
+ (is_negative(x) and is_negative(y)))
+
+ predicate diff_sign(x: t, y: t) = ((is_positive(x) and is_negative(y)) or
+ (is_negative(x) and is_positive(y)))
+
+ axiom feq_eq :
+ (forall x:t. forall y:t. (tqtisFinite(x) -> (tqtisFinite(y) ->
+ ((not is_zero(x)) -> (eq(x, y) -> (x = y))))))
+
+ axiom eq_feq :
+ (forall x:t. forall y:t. (tqtisFinite(x) -> (tqtisFinite(y) -> ((x = y) ->
+ eq(x, y)))))
+
+ axiom eq_refl : (forall x:t. (tqtisFinite(x) -> eq(x, x)))
+
+ axiom eq_sym : (forall x:t. forall y:t. (eq(x, y) -> eq(y, x)))
+
+ axiom eq_trans :
+ (forall x:t. forall y:t. forall z:t. (eq(x, y) -> (eq(y, z) -> eq(x, z))))
+
+ axiom eq_zero : eq(zeroF, neg(zeroF))
+
+ axiom eq_to_real_finite :
+ (forall x:t. forall y:t. ((tqtisFinite(x) and tqtisFinite(y)) -> (eq(x,
+ y) -> (tqtreal(x) = tqtreal(y)))))
+
+ axiom eq_to_real_finite1 :
+ (forall x:t. forall y:t. ((tqtisFinite(x) and tqtisFinite(y)) ->
+ ((tqtreal(x) = tqtreal(y)) -> eq(x, y))))
+
+ axiom eq_special : (forall x:t. forall y:t. (eq(x, y) -> is_not_nan(x)))
+
+ axiom eq_special1 : (forall x:t. forall y:t. (eq(x, y) -> is_not_nan(y)))
+
+ axiom eq_special2 :
+ (forall x:t. forall y:t. (eq(x, y) -> ((tqtisFinite(x) and
+ tqtisFinite(y)) or (is_infinite(x) and (is_infinite(y) and same_sign(x,
+ y))))))
+
+ axiom lt_finite :
+ (forall x:t. forall y:t [lt(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
+ (lt(x, y) -> (tqtreal(x) < tqtreal(y)))))
+
+ axiom lt_finite1 :
+ (forall x:t. forall y:t [lt(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
+ ((tqtreal(x) < tqtreal(y)) -> lt(x, y))))
+
+ axiom le_finite :
+ (forall x:t. forall y:t [le(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
+ (le(x, y) -> (tqtreal(x) <= tqtreal(y)))))
+
+ axiom le_finite1 :
+ (forall x:t. forall y:t [le(x, y)]. ((tqtisFinite(x) and tqtisFinite(y)) ->
+ ((tqtreal(x) <= tqtreal(y)) -> le(x, y))))
+
+ axiom le_lt_trans :
+ (forall x:t. forall y:t. forall z:t. ((le(x, y) and lt(y, z)) -> lt(x, z)))
+
+ axiom lt_le_trans :
+ (forall x:t. forall y:t. forall z:t. ((lt(x, y) and le(y, z)) -> lt(x, z)))
+
+ axiom le_ge_asym :
+ (forall x:t. forall y:t. ((le(x, y) and le(y, x)) -> eq(x, y)))
+
+ axiom not_lt_ge :
+ (forall x:t. forall y:t. (((not lt(x, y)) and (is_not_nan(x) and
+ is_not_nan(y))) -> le(y, x)))
+
+ axiom not_gt_le :
+ (forall x:t. forall y:t. (((not lt(y, x)) and (is_not_nan(x) and
+ is_not_nan(y))) -> le(x, y)))
+
+ axiom le_special :
+ (forall x:t. forall y:t [le(x, y)]. (le(x, y) -> ((tqtisFinite(x) and
+ tqtisFinite(y)) or ((is_minus_infinity(x) and is_not_nan(y)) or
+ (is_not_nan(x) and is_plus_infinity(y))))))
+
+ axiom lt_special :
+ (forall x:t. forall y:t [lt(x, y)]. (lt(x, y) -> ((tqtisFinite(x) and
+ tqtisFinite(y)) or ((is_minus_infinity(x) and (is_not_nan(y) and
+ (not is_minus_infinity(y)))) or (is_not_nan(x) and
+ ((not is_plus_infinity(x)) and is_plus_infinity(y)))))))
+
+ axiom lt_lt_finite :
+ (forall x:t. forall y:t. forall z:t. (lt(x, y) -> (lt(y, z) ->
+ tqtisFinite(y))))
+
+ axiom positive_to_real :
+ (forall x:t [is_positive(x)]. (tqtisFinite(x) -> (is_positive(x) ->
+ (0.0 <= tqtreal(x)))))
+
+ axiom to_real_positive :
+ (forall x:t [is_positive(x)]. (tqtisFinite(x) -> ((0.0 < tqtreal(x)) ->
+ is_positive(x))))
+
+ axiom negative_to_real :
+ (forall x:t [is_negative(x)]. (tqtisFinite(x) -> (is_negative(x) ->
+ (tqtreal(x) <= 0.0))))
+
+ axiom to_real_negative :
+ (forall x:t [is_negative(x)]. (tqtisFinite(x) -> ((tqtreal(x) < 0.0) ->
+ is_negative(x))))
+
+ axiom negative_xor_positive :
+ (forall x:t. (not (is_positive(x) and is_negative(x))))
+
+ axiom negative_or_positive :
+ (forall x:t. (is_not_nan(x) -> (is_positive(x) or is_negative(x))))
+
+ axiom diff_sign_trans :
+ (forall x:t. forall y:t. forall z:t. ((diff_sign(x, y) and diff_sign(y,
+ z)) -> same_sign(x, z)))
+
+ axiom diff_sign_product :
+ (forall x:t. forall y:t. ((tqtisFinite(x) and (tqtisFinite(y) and
+ ((tqtreal(x) * tqtreal(y)) < 0.0))) -> diff_sign(x, y)))
+
+ axiom same_sign_product :
+ (forall x:t. forall y:t. ((tqtisFinite(x) and (tqtisFinite(y) and
+ same_sign(x, y))) -> (0.0 <= (tqtreal(x) * tqtreal(y)))))
+
+ predicate product_sign(z: t, x: t, y: t) = ((same_sign(x, y) ->
+ is_positive(z)) and (diff_sign(x, y) -> is_negative(z)))
+
+ predicate overflow_value(m: mode, x: t) = ((((((m = RNE) ->
+ is_infinite(x)) and ((m = RNA) -> is_infinite(x))) and ((m = RTP) ->
+ (if is_positive(x) then is_infinite(x) else (tqtisFinite(x) and
+ (tqtreal(x) = (-0x1.FFFFFFFFFFFFFp1023)))))) and ((m = RTN) ->
+ (if is_positive(x) then (tqtisFinite(x) and
+ (tqtreal(x) = 0x1.FFFFFFFFFFFFFp1023)) else is_infinite(x)))) and
+ ((m = RTZ) -> (if is_positive(x) then (tqtisFinite(x) and
+ (tqtreal(x) = 0x1.FFFFFFFFFFFFFp1023)) else (tqtisFinite(x) and
+ (tqtreal(x) = (-0x1.FFFFFFFFFFFFFp1023))))))
+
+ predicate sign_zero_result(m: mode, x: t) = (is_zero(x) -> ((((((m = RNE) ->
+ is_positive(x)) and ((m = RNA) -> is_positive(x))) and ((m = RTP) ->
+ is_positive(x))) and ((m = RTN) -> is_negative(x))) and ((m = RTZ) ->
+ is_positive(x))))
+
+ axiom add_finite :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) + tqtreal(y))) ->
+ tqtisFinite(add(m, x, y))))))
+
+ axiom add_finite1 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) + tqtreal(y))) ->
+ (tqtreal(add(m, x, y)) = round(m, (tqtreal(x) + tqtreal(y))))))))
+
+ axiom add_finite_rev :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(add(m,
+ x, y)) -> tqtisFinite(x)))
+
+ axiom add_finite_rev1 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (tqtisFinite(add(m,
+ x, y)) -> tqtisFinite(y)))
+
+ axiom add_finite_rev_n :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(add(m, x, y)) -> no_overflow(m, (tqtreal(x) + tqtreal(y))))))
+
+ axiom add_finite_rev_n1 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(add(m, x, y)) -> (tqtreal(add(m, x, y)) = round(m,
+ (tqtreal(x) + tqtreal(y)))))))
+
+ axiom sub_finite :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) - tqtreal(y))) ->
+ tqtisFinite(sub(m, x, y))))))
+
+ axiom sub_finite1 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) - tqtreal(y))) ->
+ (tqtreal(sub(m, x, y)) = round(m, (tqtreal(x) - tqtreal(y))))))))
+
+ axiom sub_finite_rev :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(sub(m,
+ x, y)) -> tqtisFinite(x)))
+
+ axiom sub_finite_rev1 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (tqtisFinite(sub(m,
+ x, y)) -> tqtisFinite(y)))
+
+ axiom sub_finite_rev_n :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(sub(m, x, y)) -> no_overflow(m, (tqtreal(x) - tqtreal(y))))))
+
+ axiom sub_finite_rev_n1 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(sub(m, x, y)) -> (tqtreal(sub(m, x, y)) = round(m,
+ (tqtreal(x) - tqtreal(y)))))))
+
+ axiom mul_finite :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) * tqtreal(y))) ->
+ tqtisFinite(mul(m, x, y))))))
+
+ axiom mul_finite1 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (no_overflow(m, (tqtreal(x) * tqtreal(y))) ->
+ (tqtreal(mul(m, x, y)) = round(m, (tqtreal(x) * tqtreal(y))))))))
+
+ axiom mul_finite_rev :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(mul(m,
+ x, y)) -> tqtisFinite(x)))
+
+ axiom mul_finite_rev1 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (tqtisFinite(mul(m,
+ x, y)) -> tqtisFinite(y)))
+
+ axiom mul_finite_rev_n :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(mul(m, x, y)) -> no_overflow(m, (tqtreal(x) * tqtreal(y))))))
+
+ axiom mul_finite_rev_n1 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(mul(m, x, y)) -> (tqtreal(mul(m, x, y)) = round(m,
+ (tqtreal(x) * tqtreal(y)))))))
+
+ axiom div_finite :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> ((not is_zero(y)) -> (no_overflow(m,
+ (tqtreal(x) / tqtreal(y))) -> tqtisFinite(div(m, x, y)))))))
+
+ axiom div_finite1 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> ((not is_zero(y)) -> (no_overflow(m,
+ (tqtreal(x) / tqtreal(y))) -> (tqtreal(div(m, x, y)) = round(m,
+ (tqtreal(x) / tqtreal(y)))))))))
+
+ axiom div_finite_rev :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (tqtisFinite(div(m,
+ x, y)) -> ((tqtisFinite(x) and (tqtisFinite(y) and (not is_zero(y)))) or
+ (tqtisFinite(x) and (is_infinite(y) and (tqtreal(div(m, x, y)) = 0.0))))))
+
+ axiom div_finite_rev_n :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(div(m, x, y)) -> (tqtisFinite(y) -> no_overflow(m,
+ (tqtreal(x) / tqtreal(y)))))))
+
+ axiom div_finite_rev_n1 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (to_nearest(m) ->
+ (tqtisFinite(div(m, x, y)) -> (tqtisFinite(y) -> (tqtreal(div(m, x,
+ y)) = round(m, (tqtreal(x) / tqtreal(y))))))))
+
+ axiom neg_finite :
+ (forall x:t [neg(x)]. (tqtisFinite(x) -> tqtisFinite(neg(x))))
+
+ axiom neg_finite1 :
+ (forall x:t [neg(x)]. (tqtisFinite(x) ->
+ (tqtreal(neg(x)) = (-tqtreal(x)))))
+
+ axiom neg_finite_rev :
+ (forall x:t [neg(x)]. (tqtisFinite(neg(x)) -> tqtisFinite(x)))
+
+ axiom neg_finite_rev1 :
+ (forall x:t [neg(x)]. (tqtisFinite(neg(x)) ->
+ (tqtreal(neg(x)) = (-tqtreal(x)))))
+
+ axiom abs_finite :
+ (forall x:t [abs1(x)]. (tqtisFinite(x) -> tqtisFinite(abs1(x))))
+
+ axiom abs_finite1 :
+ (forall x:t [abs1(x)]. (tqtisFinite(x) ->
+ (tqtreal(abs1(x)) = abs(tqtreal(x)))))
+
+ axiom abs_finite2 :
+ (forall x:t [abs1(x)]. (tqtisFinite(x) -> is_positive(abs1(x))))
+
+ axiom abs_finite_rev :
+ (forall x:t [abs1(x)]. (tqtisFinite(abs1(x)) -> tqtisFinite(x)))
+
+ axiom abs_finite_rev1 :
+ (forall x:t [abs1(x)]. (tqtisFinite(abs1(x)) ->
+ (tqtreal(abs1(x)) = abs(tqtreal(x)))))
+
+ axiom abs_universal : (forall x:t [abs1(x)]. (not is_negative(abs1(x))))
+
+ axiom fma_finite :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (tqtisFinite(x) -> (tqtisFinite(y) -> (tqtisFinite(z) -> (no_overflow(m,
+ ((tqtreal(x) * tqtreal(y)) + tqtreal(z))) -> tqtisFinite(fma(m, x, y,
+ z)))))))
+
+ axiom fma_finite1 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (tqtisFinite(x) -> (tqtisFinite(y) -> (tqtisFinite(z) -> (no_overflow(m,
+ ((tqtreal(x) * tqtreal(y)) + tqtreal(z))) -> (tqtreal(fma(m, x, y,
+ z)) = round(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z)))))))))
+
+ axiom fma_finite_rev :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (tqtisFinite(fma(m, x, y, z)) -> tqtisFinite(x)))
+
+ axiom fma_finite_rev1 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (tqtisFinite(fma(m, x, y, z)) -> tqtisFinite(y)))
+
+ axiom fma_finite_rev2 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (tqtisFinite(fma(m, x, y, z)) -> tqtisFinite(z)))
+
+ axiom fma_finite_rev_n :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (to_nearest(m) -> (tqtisFinite(fma(m, x, y, z)) -> no_overflow(m,
+ ((tqtreal(x) * tqtreal(y)) + tqtreal(z))))))
+
+ axiom fma_finite_rev_n1 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ (to_nearest(m) -> (tqtisFinite(fma(m, x, y, z)) -> (tqtreal(fma(m, x, y,
+ z)) = round(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z)))))))
+
+ function sqr(x: real) : real = (x * x)
+
+ logic sqrt1 : real -> real
+
+ axiom Sqrt_positive : (forall x:real. ((0.0 <= x) -> (0.0 <= sqrt1(x))))
+
+ axiom Sqrt_square : (forall x:real. ((0.0 <= x) -> (sqr(sqrt1(x)) = x)))
+
+ axiom Square_sqrt : (forall x:real. ((0.0 <= x) -> (sqrt1((x * x)) = x)))
+
+ axiom Sqrt_mul :
+ (forall x:real. forall y:real. (((0.0 <= x) and (0.0 <= y)) ->
+ (sqrt1((x * y)) = (sqrt1(x) * sqrt1(y)))))
+
+ axiom Sqrt_le :
+ (forall x:real. forall y:real. (((0.0 <= x) and (x <= y)) ->
+ (sqrt1(x) <= sqrt1(y))))
+
+ axiom sqrt_finite :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(x) ->
+ ((0.0 <= tqtreal(x)) -> tqtisFinite(sqrt(m, x)))))
+
+ axiom sqrt_finite1 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(x) ->
+ ((0.0 <= tqtreal(x)) -> (tqtreal(sqrt(m, x)) = round(m,
+ sqrt1(tqtreal(x)))))))
+
+ axiom sqrt_finite_rev :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(sqrt(m, x)) ->
+ tqtisFinite(x)))
+
+ axiom sqrt_finite_rev1 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(sqrt(m, x)) ->
+ (0.0 <= tqtreal(x))))
+
+ axiom sqrt_finite_rev2 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (tqtisFinite(sqrt(m, x)) ->
+ (tqtreal(sqrt(m, x)) = round(m, sqrt1(tqtreal(x))))))
+
+ predicate same_sign_real(x: t, r: real) = ((is_positive(x) and (0.0 < r)) or
+ (is_negative(x) and (r < 0.0)))
+
+ axiom add_special :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_nan(x) or
+ is_nan(y)) -> is_nan(add(m, x, y))))
+
+ axiom add_special1 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
+ is_infinite(y)) -> is_infinite(add(m, x, y))))
+
+ axiom add_special2 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
+ is_infinite(y)) -> same_sign(add(m, x, y), y)))
+
+ axiom add_special3 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
+ tqtisFinite(y)) -> is_infinite(add(m, x, y))))
+
+ axiom add_special4 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
+ tqtisFinite(y)) -> same_sign(add(m, x, y), x)))
+
+ axiom add_special5 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
+ (is_infinite(y) and same_sign(x, y))) -> is_infinite(add(m, x, y))))
+
+ axiom add_special6 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
+ (is_infinite(y) and same_sign(x, y))) -> same_sign(add(m, x, y), x)))
+
+ axiom add_special7 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((is_infinite(x) and
+ (is_infinite(y) and diff_sign(x, y))) -> is_nan(add(m, x, y))))
+
+ axiom add_special8 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
+ (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) + tqtreal(y)))))) ->
+ same_sign_real(add(m, x, y), (tqtreal(x) + tqtreal(y)))))
+
+ axiom add_special9 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
+ (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) + tqtreal(y)))))) ->
+ overflow_value(m, add(m, x, y))))
+
+ axiom add_special10 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
+ tqtisFinite(y)) -> (same_sign(x, y) -> same_sign(add(m, x, y), x))))
+
+ axiom add_special11 :
+ (forall m:mode. forall x:t. forall y:t [add(m, x, y)]. ((tqtisFinite(x) and
+ tqtisFinite(y)) -> ((not same_sign(x, y)) -> sign_zero_result(m, add(m, x,
+ y)))))
+
+ axiom sub_special :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_nan(x) or
+ is_nan(y)) -> is_nan(sub(m, x, y))))
+
+ axiom sub_special1 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
+ is_infinite(y)) -> is_infinite(sub(m, x, y))))
+
+ axiom sub_special2 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
+ is_infinite(y)) -> diff_sign(sub(m, x, y), y)))
+
+ axiom sub_special3 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
+ tqtisFinite(y)) -> is_infinite(sub(m, x, y))))
+
+ axiom sub_special4 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
+ tqtisFinite(y)) -> same_sign(sub(m, x, y), x)))
+
+ axiom sub_special5 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
+ (is_infinite(y) and same_sign(x, y))) -> is_nan(sub(m, x, y))))
+
+ axiom sub_special6 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
+ (is_infinite(y) and diff_sign(x, y))) -> is_infinite(sub(m, x, y))))
+
+ axiom sub_special7 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((is_infinite(x) and
+ (is_infinite(y) and diff_sign(x, y))) -> same_sign(sub(m, x, y), x)))
+
+ axiom sub_special8 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
+ (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) - tqtreal(y)))))) ->
+ same_sign_real(sub(m, x, y), (tqtreal(x) - tqtreal(y)))))
+
+ axiom sub_special9 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
+ (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) - tqtreal(y)))))) ->
+ overflow_value(m, sub(m, x, y))))
+
+ axiom sub_special10 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
+ tqtisFinite(y)) -> (diff_sign(x, y) -> same_sign(sub(m, x, y), x))))
+
+ axiom sub_special11 :
+ (forall m:mode. forall x:t. forall y:t [sub(m, x, y)]. ((tqtisFinite(x) and
+ tqtisFinite(y)) -> ((not diff_sign(x, y)) -> sign_zero_result(m, sub(m, x,
+ y)))))
+
+ axiom mul_special :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_nan(x) or
+ is_nan(y)) -> is_nan(mul(m, x, y))))
+
+ axiom mul_special1 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_zero(x) and
+ is_infinite(y)) -> is_nan(mul(m, x, y))))
+
+ axiom mul_special2 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((tqtisFinite(x) and
+ (is_infinite(y) and (not is_zero(x)))) -> is_infinite(mul(m, x, y))))
+
+ axiom mul_special3 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_infinite(x) and
+ is_zero(y)) -> is_nan(mul(m, x, y))))
+
+ axiom mul_special4 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_infinite(x) and
+ (tqtisFinite(y) and (not is_zero(y)))) -> is_infinite(mul(m, x, y))))
+
+ axiom mul_special5 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((is_infinite(x) and
+ is_infinite(y)) -> is_infinite(mul(m, x, y))))
+
+ axiom mul_special6 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. ((tqtisFinite(x) and
+ (tqtisFinite(y) and (not no_overflow(m, (tqtreal(x) * tqtreal(y)))))) ->
+ overflow_value(m, mul(m, x, y))))
+
+ axiom mul_special7 :
+ (forall m:mode. forall x:t. forall y:t [mul(m, x, y)]. (let r = mul(m, x,
+ y) : t in ((not is_nan(r)) -> product_sign(r, x, y))))
+
+ axiom div_special :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_nan(x) or
+ is_nan(y)) -> is_nan(div(m, x, y))))
+
+ axiom div_special1 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((tqtisFinite(x) and
+ is_infinite(y)) -> is_zero(div(m, x, y))))
+
+ axiom div_special2 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_infinite(x) and
+ tqtisFinite(y)) -> is_infinite(div(m, x, y))))
+
+ axiom div_special3 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_infinite(x) and
+ is_infinite(y)) -> is_nan(div(m, x, y))))
+
+ axiom div_special4 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((tqtisFinite(x) and
+ (tqtisFinite(y) and ((not is_zero(y)) and (not no_overflow(m,
+ (tqtreal(x) / tqtreal(y))))))) -> overflow_value(m, div(m, x, y))))
+
+ axiom div_special5 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((tqtisFinite(x) and
+ (is_zero(y) and (not is_zero(x)))) -> is_infinite(div(m, x, y))))
+
+ axiom div_special6 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. ((is_zero(x) and
+ is_zero(y)) -> is_nan(div(m, x, y))))
+
+ axiom div_special7 :
+ (forall m:mode. forall x:t. forall y:t [div(m, x, y)]. (let r = div(m, x,
+ y) : t in ((not is_nan(r)) -> product_sign(r, x, y))))
+
+ axiom neg_special : (forall x:t [neg(x)]. (is_nan(x) -> is_nan(neg(x))))
+
+ axiom neg_special1 :
+ (forall x:t [neg(x)]. (is_infinite(x) -> is_infinite(neg(x))))
+
+ axiom neg_special2 :
+ (forall x:t [neg(x)]. ((not is_nan(x)) -> diff_sign(x, neg(x))))
+
+ axiom abs_special : (forall x:t [abs1(x)]. (is_nan(x) -> is_nan(abs1(x))))
+
+ axiom abs_special1 :
+ (forall x:t [abs1(x)]. (is_infinite(x) -> is_infinite(abs1(x))))
+
+ axiom abs_special2 :
+ (forall x:t [abs1(x)]. ((not is_nan(x)) -> is_positive(abs1(x))))
+
+ axiom fma_special :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_nan(x) or (is_nan(y) or is_nan(z))) -> is_nan(fma(m, x, y, z))))
+
+ axiom fma_special1 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_zero(x) and is_infinite(y)) -> is_nan(fma(m, x, y, z))))
+
+ axiom fma_special2 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and is_zero(y)) -> is_nan(fma(m, x, y, z))))
+
+ axiom fma_special3 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
+ tqtisFinite(z)))) -> is_infinite(fma(m, x, y, z))))
+
+ axiom fma_special4 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
+ tqtisFinite(z)))) -> product_sign(fma(m, x, y, z), x, y)))
+
+ axiom fma_special5 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
+ is_infinite(z)))) -> (product_sign(z, x, y) -> is_infinite(fma(m, x, y,
+ z)))))
+
+ axiom fma_special6 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
+ is_infinite(z)))) -> (product_sign(z, x, y) -> same_sign(fma(m, x, y, z),
+ z))))
+
+ axiom fma_special7 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and ((not is_zero(x)) and (is_infinite(y) and
+ is_infinite(z)))) -> ((not product_sign(z, x, y)) -> is_nan(fma(m, x, y,
+ z)))))
+
+ axiom fma_special8 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
+ tqtisFinite(z)))) -> is_infinite(fma(m, x, y, z))))
+
+ axiom fma_special9 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
+ tqtisFinite(z)))) -> product_sign(fma(m, x, y, z), x, y)))
+
+ axiom fma_special10 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
+ is_infinite(z)))) -> (product_sign(z, x, y) -> is_infinite(fma(m, x, y,
+ z)))))
+
+ axiom fma_special11 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
+ is_infinite(z)))) -> (product_sign(z, x, y) -> same_sign(fma(m, x, y, z),
+ z))))
+
+ axiom fma_special12 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (tqtisFinite(y) and ((not is_zero(y)) and
+ is_infinite(z)))) -> ((not product_sign(z, x, y)) -> is_nan(fma(m, x, y,
+ z)))))
+
+ axiom fma_special13 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (is_infinite(y) and tqtisFinite(z))) ->
+ is_infinite(fma(m, x, y, z))))
+
+ axiom fma_special14 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (is_infinite(y) and tqtisFinite(z))) ->
+ product_sign(fma(m, x, y, z), x, y)))
+
+ axiom fma_special15 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and is_infinite(z))) ->
+ is_infinite(fma(m, x, y, z))))
+
+ axiom fma_special16 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and is_infinite(z))) ->
+ same_sign(fma(m, x, y, z), z)))
+
+ axiom fma_special17 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (is_infinite(y) and is_infinite(z))) ->
+ (product_sign(z, x, y) -> is_infinite(fma(m, x, y, z)))))
+
+ axiom fma_special18 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (is_infinite(y) and is_infinite(z))) ->
+ (product_sign(z, x, y) -> same_sign(fma(m, x, y, z), z))))
+
+ axiom fma_special19 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((is_infinite(x) and (is_infinite(y) and is_infinite(z))) ->
+ ((not product_sign(z, x, y)) -> is_nan(fma(m, x, y, z)))))
+
+ axiom fma_special20 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and (tqtisFinite(z) and
+ (not no_overflow(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z))))))) ->
+ same_sign_real(fma(m, x, y, z), ((tqtreal(x) * tqtreal(y)) + tqtreal(z)))))
+
+ axiom fma_special21 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and (tqtisFinite(z) and
+ (not no_overflow(m, ((tqtreal(x) * tqtreal(y)) + tqtreal(z))))))) ->
+ overflow_value(m, fma(m, x, y, z))))
+
+ axiom fma_special22 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and tqtisFinite(z))) ->
+ (product_sign(z, x, y) -> same_sign(fma(m, x, y, z), z))))
+
+ axiom fma_special23 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and tqtisFinite(z))) ->
+ ((not product_sign(z, x, y)) ->
+ ((((tqtreal(x) * tqtreal(y)) + tqtreal(z)) = 0.0) -> ((m = RTN) ->
+ is_negative(fma(m, x, y, z)))))))
+
+ axiom fma_special24 :
+ (forall m:mode. forall x:t. forall y:t. forall z:t [fma(m, x, y, z)].
+ ((tqtisFinite(x) and (tqtisFinite(y) and tqtisFinite(z))) ->
+ ((not product_sign(z, x, y)) ->
+ ((((tqtreal(x) * tqtreal(y)) + tqtreal(z)) = 0.0) -> ((not (m = RTN)) ->
+ is_positive(fma(m, x, y, z)))))))
+
+ axiom sqrt_special :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (is_nan(x) -> is_nan(sqrt(m, x))))
+
+ axiom sqrt_special1 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (is_plus_infinity(x) ->
+ is_plus_infinity(sqrt(m, x))))
+
+ axiom sqrt_special2 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (is_minus_infinity(x) ->
+ is_nan(sqrt(m, x))))
+
+ axiom sqrt_special3 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. ((tqtisFinite(x) and
+ (tqtreal(x) < 0.0)) -> is_nan(sqrt(m, x))))
+
+ axiom sqrt_special4 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. (is_zero(x) -> same_sign(sqrt(m,
+ x), x)))
+
+ axiom sqrt_special5 :
+ (forall m:mode. forall x:t [sqrt(m, x)]. ((tqtisFinite(x) and
+ (0.0 < tqtreal(x))) -> is_positive(sqrt(m, x))))
+
+ axiom of_int_add_exact :
+ (forall m:mode. forall n:mode. forall i:int. forall j:int.
+ (in_safe_int_range(i) -> (in_safe_int_range(j) ->
+ (in_safe_int_range((i + j)) -> eq(of_int(m, (i + j)), add(n, of_int(m, i),
+ of_int(m, j)))))))
+
+ axiom of_int_sub_exact :
+ (forall m:mode. forall n:mode. forall i:int. forall j:int.
+ (in_safe_int_range(i) -> (in_safe_int_range(j) ->
+ (in_safe_int_range((i - j)) -> eq(of_int(m, (i - j)), sub(n, of_int(m, i),
+ of_int(m, j)))))))
+
+ axiom of_int_mul_exact :
+ (forall m:mode. forall n:mode. forall i:int. forall j:int.
+ (in_safe_int_range(i) -> (in_safe_int_range(j) ->
+ (in_safe_int_range((i * j)) -> eq(of_int(m, (i * j)), mul(n, of_int(m, i),
+ of_int(m, j)))))))
+
+ axiom Min_r : (forall x:t. forall y:t. (le(y, x) -> eq(min(x, y), y)))
+
+ axiom Min_l : (forall x:t. forall y:t. (le(x, y) -> eq(min(x, y), x)))
+
+ axiom Max_r : (forall x:t. forall y:t. (le(y, x) -> eq(max(x, y), x)))
+
+ axiom Max_l : (forall x:t. forall y:t. (le(x, y) -> eq(max(x, y), y)))
+
+ logic is_int : t -> prop
+
+ axiom zeroF_is_int : is_int(zeroF)
+
+ axiom of_int_is_int :
+ (forall m:mode. forall x:int. (in_int_range(x) -> is_int(of_int(m, x))))
+
+ axiom big_float_is_int :
+ (forall m:mode. forall i:t. (tqtisFinite(i) -> ((le(i, neg(of_int(m,
+ 9007199254740992))) or le(of_int(m, 9007199254740992), i)) -> is_int(i))))
+
+ axiom roundToIntegral_is_int :
+ (forall m:mode. forall x:t. (tqtisFinite(x) -> is_int(roundToIntegral(m,
+ x))))
+
+ axiom eq_is_int :
+ (forall x:t. forall y:t. (eq(x, y) -> (is_int(x) -> is_int(y))))
+
+ axiom add_int :
+ (forall x:t. forall y:t. forall m:mode. (is_int(x) -> (is_int(y) ->
+ (tqtisFinite(add(m, x, y)) -> is_int(add(m, x, y))))))
+
+ axiom sub_int :
+ (forall x:t. forall y:t. forall m:mode. (is_int(x) -> (is_int(y) ->
+ (tqtisFinite(sub(m, x, y)) -> is_int(sub(m, x, y))))))
+
+ axiom mul_int :
+ (forall x:t. forall y:t. forall m:mode. (is_int(x) -> (is_int(y) ->
+ (tqtisFinite(mul(m, x, y)) -> is_int(mul(m, x, y))))))
+
+ axiom fma_int :
+ (forall x:t. forall y:t. forall z:t. forall m:mode. (is_int(x) ->
+ (is_int(y) -> (is_int(z) -> (tqtisFinite(fma(m, x, y, z)) -> is_int(fma(m,
+ x, y, z)))))))
+
+ axiom neg_int : (forall x:t. (is_int(x) -> is_int(neg(x))))
+
+ axiom abs_int1 : (forall x:t. (is_int(x) -> is_int(abs1(x))))
+
+ axiom is_int_of_int :
+ (forall x:t. forall m:mode. forall mqt:mode. (is_int(x) -> eq(x,
+ of_int(mqt, to_int(m, x)))))
+
+ axiom is_int_to_int :
+ (forall m:mode. forall x:t. (is_int(x) -> in_int_range(to_int(m, x))))
+
+ axiom is_int_is_finite : (forall x:t. (is_int(x) -> tqtisFinite(x)))
+
+ axiom int_to_real :
+ (forall m:mode. forall x:t. (is_int(x) -> (tqtreal(x) = from_int(to_int(m,
+ x)))))
+
+ axiom truncate_int :
+ (forall m:mode. forall i:t. (is_int(i) -> eq(roundToIntegral(m, i), i)))
+
+ axiom truncate_neg :
+ (forall x:t. (tqtisFinite(x) -> (is_negative(x) -> (roundToIntegral(RTZ,
+ x) = roundToIntegral(RTP, x)))))
+
+ axiom truncate_pos :
+ (forall x:t. (tqtisFinite(x) -> (is_positive(x) -> (roundToIntegral(RTZ,
+ x) = roundToIntegral(RTN, x)))))
+
+ axiom ceil_le :
+ (forall x:t. (tqtisFinite(x) -> le(x, roundToIntegral(RTP, x))))
+
+ axiom ceil_lest :
+ (forall x:t. forall y:t. ((le(x, y) and is_int(y)) ->
+ le(roundToIntegral(RTP, x), y)))
+
+ axiom ceil_to_real :
+ (forall x:t. (tqtisFinite(x) -> (tqtreal(roundToIntegral(RTP,
+ x)) = from_int(ceil(tqtreal(x))))))
+
+ axiom ceil_to_int :
+ (forall m:mode. forall x:t. (tqtisFinite(x) -> (to_int(m,
+ roundToIntegral(RTP, x)) = ceil(tqtreal(x)))))
+
+ axiom floor_le :
+ (forall x:t. (tqtisFinite(x) -> le(roundToIntegral(RTN, x), x)))
+
+ axiom floor_lest :
+ (forall x:t. forall y:t. ((le(y, x) and is_int(y)) -> le(y,
+ roundToIntegral(RTN, x))))
+
+ axiom floor_to_real :
+ (forall x:t. (tqtisFinite(x) -> (tqtreal(roundToIntegral(RTN,
+ x)) = from_int(floor(tqtreal(x))))))
+
+ axiom floor_to_int :
+ (forall m:mode. forall x:t. (tqtisFinite(x) -> (to_int(m,
+ roundToIntegral(RTN, x)) = floor(tqtreal(x)))))
+
+ axiom RNA_down :
+ (forall x:t. (lt(sub(RNE, x, roundToIntegral(RTN, x)), sub(RNE,
+ roundToIntegral(RTP, x), x)) -> (roundToIntegral(RNA,
+ x) = roundToIntegral(RTN, x))))
+
+ axiom RNA_up :
+ (forall x:t. (lt(sub(RNE, roundToIntegral(RTP, x), x), sub(RNE, x,
+ roundToIntegral(RTN, x))) -> (roundToIntegral(RNA,
+ x) = roundToIntegral(RTP, x))))
+
+ axiom RNA_down_tie :
+ (forall x:t. (eq(sub(RNE, x, roundToIntegral(RTN, x)), sub(RNE,
+ roundToIntegral(RTP, x), x)) -> (is_negative(x) -> (roundToIntegral(RNA,
+ x) = roundToIntegral(RTN, x)))))
+
+ axiom RNA_up_tie :
+ (forall x:t. (eq(sub(RNE, roundToIntegral(RTP, x), x), sub(RNE, x,
+ roundToIntegral(RTN, x))) -> (is_positive(x) -> (roundToIntegral(RNA,
+ x) = roundToIntegral(RTP, x)))))
+
+ axiom to_int_roundToIntegral :
+ (forall m:mode. forall x:t. (to_int(m, x) = to_int(m, roundToIntegral(m,
+ x))))
+
+ axiom to_int_monotonic :
+ (forall m:mode. forall x:t. forall y:t. (tqtisFinite(x) ->
+ (tqtisFinite(y) -> (le(x, y) -> (to_int(m, x) <= to_int(m, y))))))
+
+ axiom to_int_of_int :
+ (forall m:mode. forall i:int. (in_safe_int_range(i) -> (to_int(m, of_int(m,
+ i)) = i)))
+
+ axiom eq_to_int :
+ (forall m:mode. forall x:t. forall y:t. (tqtisFinite(x) -> (eq(x, y) ->
+ (to_int(m, x) = to_int(m, y)))))
+
+ axiom neg_to_int :
+ (forall m:mode. forall x:t. (is_int(x) -> (to_int(m, neg(x)) = (-to_int(m,
+ x)))))
+
+ axiom roundToIntegral_is_finite :
+ (forall m:mode. forall x:t. (tqtisFinite(x) ->
+ tqtisFinite(roundToIntegral(m, x))))
+
+ axiom round_bound_ne :
+ (forall x:real [round(RNE, x)]. (no_overflow(RNE, x) ->
+ (((x - (0x1.0p-53 * abs(x))) - 0x1.0p-1075) <= round(RNE, x))))
+
+ axiom round_bound_ne1 :
+ (forall x:real [round(RNE, x)]. (no_overflow(RNE, x) -> (round(RNE,
+ x) <= ((x + (0x1.0p-53 * abs(x))) + 0x1.0p-1075))))
+
+ axiom round_bound :
+ (forall m:mode. forall x:real [round(m, x)]. (no_overflow(m, x) ->
+ (((x - (0x1.0p-52 * abs(x))) - 0x1.0p-1074) <= round(m, x))))
+
+ axiom round_bound1 :
+ (forall m:mode. forall x:real [round(m, x)]. (no_overflow(m, x) ->
+ (round(m, x) <= ((x + (0x1.0p-52 * abs(x))) + 0x1.0p-1074))))
+
+ type ('a, 'a1, 'a2, 'a3, 'a4) tuple5 = { Tuple5_proj_1 : 'a; Tuple5_proj_2 :
+ 'a1; Tuple5_proj_3 : 'a2; Tuple5_proj_4 : 'a3; Tuple5_proj_5 : 'a4
+ }
+
+ logic nnet_apply : t, t, t, t, t -> (t, t, t, t, t) tuple5
+
+ goal G :
+ (forall x1:t. forall x2:t. forall x3:t. forall x4:t. forall x5:t.
+ (forall x:t. forall x6:t. forall x7:t. forall x8:t. forall x9:t.
+ ((nnet_apply(x1, x2, x3, x4, x5) = { Tuple5_proj_1 = x; Tuple5_proj_2 = x6;
+ Tuple5_proj_3 = x7; Tuple5_proj_4 = x8; Tuple5_proj_5 = x9 }) ->
+ ((0.0 < tqtreal(x)) and (tqtreal(x) < 0.1)))))