| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/float/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 10 kB |
|
Quelle infinity_arithmetic.prf Sprache: Lisp |
|||||||||
|
(infinity_arithmetic
(fp_sub_inf_def_TCC1 0 (fp_sub_inf_def_TCC1-1 nil 3507032124 ("" (skolem-typepred) (("" (rewrite "toggle_infinite") (("" (rewrite "toggle_finite") (("" (ground) nil)))))) nil) ((toggle_infinite formula-decl nil IEEE_854_values nil) (toggle_finite formula-decl nil IEEE_854_values nil) (infinite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" infinity_arithmetic nil) (E_max formal-const-decl "integer" infinity_arithmetic nil) (integer nonempty-type-from-decl nil integers nil) (p formal-const-decl "above(1)" infinity_arithmetic nil) (b formal-const-decl "above(1)" infinity_arithmetic nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (fp_sub_inf_def 0 (fp_sub_inf_def-1 nil 3507032124 ("" (skosimp*) (("" (rewrite "fp_sub_inf") (("" (rewrite "fp_add_inf") (("" (rewrite "toggle_infinite") (("" (lift-if) (("" (lift-if) (("" (ground) (("1" (expand "toggle_sign") (("1" (assert) (("1" (typepred "i_sign(num2!1)") (("1" (typepred "i_sign(num1!1)") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "toggle_sign") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fp_sub_inf const-decl "fp_num" infinity_arithmetic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (above nonempty-type-eq-decl nil integers nil) (b formal-const-decl "above(1)" infinity_arithmetic nil) (p formal-const-decl "above(1)" infinity_arithmetic nil) (integer nonempty-type-from-decl nil integers nil) (E_max formal-const-decl "integer" infinity_arithmetic nil) (E_min formal-const-decl "{i: integer | E_max > i}" infinity_arithmetic nil) (fp_num type-decl nil IEEE_854_values nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (infinite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (toggle_infinite formula-decl nil IEEE_854_values nil) (i_sign adt-accessor-decl "[(infinite?) -> sign_rep]" IEEE_854_values nil) (sign_rep type-eq-decl nil enumerated_type_defs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (toggle_sign const-decl "fp_num" IEEE_854_values nil) (fp_add_inf const-decl "fp_num" infinity_arithmetic nil)) nil)) (mult_sign_TCC1 0 (mult_sign_TCC1-1 nil 3507032124 ("" (skolem-typepred) (("" (ground) nil)) nil) ((infinite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" infinity_arithmetic nil) (E_max formal-const-decl "integer" infinity_arithmetic nil) (integer nonempty-type-from-decl nil integers nil) (p formal-const-decl "above(1)" infinity_arithmetic nil) (b formal-const-decl "above(1)" infinity_arithmetic nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (mult_sign_TCC2 0 (mult_sign_TCC2-1 nil 3507032124 ("" (skolem-typepred) (("" (ground) nil)) nil) ((infinite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" infinity_arithmetic nil) (E_max formal-const-decl "integer" infinity_arithmetic nil) (integer nonempty-type-from-decl nil integers nil) (p formal-const-decl "above(1)" infinity_arithmetic nil) (b formal-const-decl "above(1)" infinity_arithmetic nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (mult_sign_TCC3 0 (mult_sign_TCC3-1 nil 3507032124 ("" (skolem-typepred) (("" (ground) nil)) nil) ((infinite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" infinity_arithmetic nil) (E_max formal-const-decl "integer" infinity_arithmetic nil) (integer nonempty-type-from-decl nil integers nil) (p formal-const-decl "above(1)" infinity_arithmetic nil) (b formal-const-decl "above(1)" infinity_arithmetic nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (mult_sign_TCC4 0 (mult_sign_TCC4-1 nil 3507032124 ("" (skolem-typepred) (("" (ground) nil)) nil) ((infinite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values nil) (fp_num type-decl nil IEEE_854_values nil) (E_min formal-const-decl "{i: integer | E_max > i}" infinity_arithmetic nil) (E_max formal-const-decl "integer" infinity_arithmetic nil) (integer nonempty-type-from-decl nil integers nil) (p formal-const-decl "above(1)" infinity_arithmetic nil) (b formal-const-decl "above(1)" infinity_arithmetic nil) (above nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (fp_div_inf_TCC1 0 (fp_div_inf_TCC1-1 nil 3507032124 ("" (skosimp*) (("" (assert) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil))) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28