Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
NaN_ops.prf
Sprache: Unknown
|
(NaN_ops
(mk_quiet_correct 0
(mk_quiet_correct-1 nil 3507032125
("" (grind)
(("" (lemma "fp_num_NaN_eta") (("" (inst?) (("" (assert) nil))))))
nil)
((E_min formal-const-decl "{i: integer | E_max > i}" NaN_ops nil)
(E_max formal-const-decl "integer" NaN_ops nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" NaN_ops nil)
(b formal-const-decl "above(1)" NaN_ops nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(fp_num_NaN_eta formula-decl nil IEEE_854_values nil)
(fp_num type-decl nil IEEE_854_values nil)
(NaN? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(mk_quiet const-decl "fp_num" NaN_ops nil)
(signal? const-decl "bool" NaN_ops nil))
nil))
(fp_quiet_TCC1 0
(fp_quiet_TCC1-1 nil 3507032125
(""
(inst +
"lambda op,fp1,(fp2|NaN?(fp1) or NaN?(fp2)): if NaN?(fp1) then fp1 else fp2 endif")
(("1" (skolem-typepred) (("1" (prop) nil))) ("2" (skosimp*) nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NaN? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(fp_num type-decl nil IEEE_854_values nil)
(E_min formal-const-decl "{i: integer | E_max > i}" NaN_ops nil)
(E_max formal-const-decl "integer" NaN_ops nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" NaN_ops nil)
(b formal-const-decl "above(1)" NaN_ops nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(fp_ops type-decl nil enumerated_type_defs nil))
nil))
(fp_signal_TCC1 0
(fp_signal_TCC1-1 nil 3507032125
("" (skolem-typepred) (("" (grind) nil)) nil)
((mk_quiet const-decl "fp_num" NaN_ops nil)
(NaN? 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}" NaN_ops nil)
(E_max formal-const-decl "integer" NaN_ops nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" NaN_ops nil)
(b formal-const-decl "above(1)" NaN_ops 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))
(NaN_ops_correct_TCC1 0
(NaN_ops_correct_TCC1-1 nil 3507032125 ("" (tcc :defs !) nil nil)
((signal? const-decl "bool" NaN_ops nil)
(E_min formal-const-decl "{i: integer | E_max > i}" NaN_ops nil)
(E_max formal-const-decl "integer" NaN_ops nil)
(integer nonempty-type-from-decl nil integers nil)
(p formal-const-decl "above(1)" NaN_ops nil)
(b formal-const-decl "above(1)" NaN_ops nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(invalid const-decl "(NaN?)" IEEE_854_values nil)
(mk_quiet const-decl "fp_num" NaN_ops nil)
(fp_signal const-decl "fp_num" NaN_ops nil)
(fp_nan const-decl "fp_num" NaN_ops nil))
nil))
(NaN_ops_correct 0
(NaN_ops_correct-1 nil 3507032125
("" (skosimp*)
(("" (expand "fp_nan")
(("" (lift-if)
(("" (expand "fp_signal")
(("" (assert)
(("" (split 2)
(("1" (flatten)
(("1" (hide -1)
(("1"
(typepred
"fp_quiet(op!1, mk_quiet(fp1!1), mk_quiet(fp2!1))")
(("1" (grind) nil) ("2" (grind) nil)))))))
("2" (flatten)
(("2" (typepred "fp_quiet(op!1, fp1!1, fp2!1)")
(("1" (expand "signal?") (("1" (grind) nil)))
("2" (propax) nil))))))))))))))))
nil)
((fp_nan const-decl "fp_num" NaN_ops nil)
(fp_signal const-decl "fp_num" NaN_ops nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(b formal-const-decl "above(1)" NaN_ops nil)
(p formal-const-decl "above(1)" NaN_ops nil)
(integer nonempty-type-from-decl nil integers nil)
(E_max formal-const-decl "integer" NaN_ops nil)
(E_min formal-const-decl "{i: integer | E_max > i}" NaN_ops nil)
(fp_num type-decl nil IEEE_854_values nil)
(NaN? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
nil)
(fp_ops type-decl nil enumerated_type_defs nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(fp_quiet const-decl "{nan | nan = fp1 OR nan = fp2}" NaN_ops nil)
(mk_quiet const-decl "fp_num" NaN_ops nil)
(signal? const-decl "bool" NaN_ops nil))
nil)))
[ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
]
|
|
