Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Sprache: Lisp

Original von: PVS^©

(IEEE_854_defs
(fp_add_TCC1 0
  (fp_add_TCC1-1 nil 3321206130
   ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil))
(fp_add_TCC2 0
  (fp_add_TCC2-1 nil 3321206130
   ("" (skosimp*) (("" (grind) nil nil)) nil) nil nil))
(fp_add_x_correct 0
  (fp_add_x_correct-1 nil 3321206130
   ("" (skosimp*)
    (("" (expand "fp_add")
      (("" (expand "fp_add_x")
        (("" (lift-if)
          (("" (expand "fp_nan")
            (("" (expand "fp_nan_x")
              (("" (expand "fp_add_inf")
                (("" (expand "fp_add_inf_x")
                  (("" (ground)
                    (("" (expand "fp_op")
                      (("" (expand "fp_op_x")
                        (("" (expand "real_to_fp_x")
                          (("" (expand "fp_round")
                            (("" (expand "fp_round_x")
                              ((""
                                (lift-if)
                                ((""
                                  (expand "round_exceptions")
                                  ((""
                                    (propax)
                                    nil))))))))))))))))))))))))))))))))
    nil)
   ((fp_add const-decl "fp_num" IEEE_854_defs nil)
    (fp_nan_x const-decl "[fp_num, exception]" NaN_ops nil)
    (fp_add_inf_x const-decl "[fp_num, exception]" infinity_arithmetic
     nil)
    (fp_op const-decl "fp_num" arithmetic_ops nil)
    (real_to_fp_x const-decl "[fp_num, exception]" real_to_fp nil)
    (fp_round_x const-decl "[real, exception]" real_to_fp nil)
    (round_exceptions const-decl "real" real_to_fp nil)
    (fp_round const-decl "real" real_to_fp nil)
    (fp_op_x const-decl "[fp_num, exception]" arithmetic_ops nil)
    (fp_add_inf const-decl "fp_num" infinity_arithmetic nil)
    (fp_nan const-decl "fp_num" NaN_ops nil)
    (fp_add_x const-decl "[fp_num, exception]" IEEE_854_defs nil))
   nil))
(fsub_alt_def 0
  (fsub_alt_def-1 nil 3321206130
   ("" (skosimp*)
    (("" (expand "fp_sub")
      (("" (expand "fp_add")
        (("" (rewrite "toggle_finite")
          (("" (rewrite "toggle_NaN")
            (("" (lift-if)
              (("" (assert)
                (("" (split)
                  (("1" (flatten)
                    (("1" (expand "fp_op")
                      (("1" (expand "apply")
                        (("1" (rewrite "value_toggle")
                          (("1" (assert)
                            (("1" (lift-if)
                              (("1"
                                (assert)
                                (("1"
                                  (ground)
                                  (("1"
                                    (expand "signed_zero")
                                    (("1"
                                      (case
                                       "forall fp: zero?(toggle_sign(fp)) iff zero?(fp)")
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (case
                                             "forall (fin1,fin2: (finite?)): (sign(fin1) = sign(toggle_sign(fin2))) iff (sign(fin1) /= sign(fin2))")
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (replace -1)
                                                (("1" (propax) nil)))))
                                             ("2"
                                              (hide -1 -2 -3 -4 2 3 4)
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (expand
                                                   "toggle_sign")
                                                  (("2"
                                                    (typepred
                                                     "sign(fin1!1)")
                                                    (("2"
                                                      (typepred
                                                       "sign(fin2!1)")
                                                      (("2"
                                                        (ground)
                                                        nil)))))))))))
                                             ("3"
                                              (hide -1 -2 -3 -4 2 3 4)
                                              (("3"
                                                (skosimp*)
                                                (("3"
                                                  (rewrite
                                                   "toggle_finite")
                                                  nil)))))))))))
                                       ("2"
                                        (hide -1 -2 -3 2 3 4)
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (expand "zero?")
                                            (("2"
                                              (rewrite "toggle_finite")
                                              (("2"
                                                (rewrite
                                                 "value_toggle")
                                                (("2"
                                                  (ground)
                                                  nil)))))))))))))))))))))))))))))))
                   ("2" (flatten)
                    (("2" (rewrite "fp_sub_inf_def")
                      (("1" (ground) nil)
                       ("2" (ground) nil))))))))))))))))))))
    nil)
   ((fp_sub const-decl "fp_num" IEEE_854_defs nil)
    (toggle_finite formula-decl nil IEEE_854_values nil)
    (fp_num type-decl nil IEEE_854_values 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)" IEEE_854_defs nil)
    (p formal-const-decl "above(1)" IEEE_854_defs nil)
    (integer nonempty-type-from-decl nil integers nil)
    (E_max formal-const-decl "integer" IEEE_854_defs nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_defs
     nil)
    (fp_op const-decl "fp_num" arithmetic_ops nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (value_toggle formula-decl nil IEEE_854_values nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (zero? const-decl "bool" IEEE_854_values nil)
    (toggle_sign const-decl "fp_num" IEEE_854_values nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (sign adt-accessor-decl "[(finite?) -> sign_rep]" IEEE_854_values
          nil)
    (sign_rep type-eq-decl nil enumerated_type_defs nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (signed_zero const-decl "{fin | zero?(fin)}" arithmetic_ops nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (apply const-decl "real" arithmetic_ops nil)
    (fp_sub_inf_def formula-decl nil infinity_arithmetic nil)
    (infinite? adt-recognizer-decl "[fp_num -> boolean]"
     IEEE_854_values nil)
    (toggle_NaN formula-decl nil IEEE_854_values nil)
    (fp_add const-decl "fp_num" IEEE_854_defs nil))
   nil))
(fp_div_TCC1 0
  (fp_div_TCC1-1 nil 3321206130 ("" (skosimp*) (("" (assert) nil)) nil)
   nil nil))
(fp_div_TCC2 0
  (fp_div_TCC2-1 nil 3321206136 ("" (subtype-tcc) nil nil) nil nil))
(fp_sqrt_TCC1 0
  (fp_sqrt_TCC1-1 nil 3321206130
   ("" (skosimp*)
    (("" (lemma "value_positive") (("" (inst?) (("" (assert) nil))))))
    nil)
   ((E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_defs
     nil)
    (E_max formal-const-decl "integer" IEEE_854_defs nil)
    (integer nonempty-type-from-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_defs nil)
    (b formal-const-decl "above(1)" IEEE_854_defs 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)
    (value_positive formula-decl nil IEEE_854_values nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (finite? adt-recognizer-decl "[fp_num -> boolean]" IEEE_854_values
     nil)
    (fp_num type-decl nil IEEE_854_values nil))
   nil))
(fp_sqrt_TCC2 0
  (fp_sqrt_TCC2-1 nil 3321206130 ("" (tcc) nil nil)
   ((expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (E_min formal-const-decl "{i: integer | E_max > i}" IEEE_854_defs
     nil)
    (E_max formal-const-decl "integer" IEEE_854_defs nil)
    (integer nonempty-type-from-decl nil integers nil)
    (p formal-const-decl "above(1)" IEEE_854_defs nil)
    (b formal-const-decl "above(1)" IEEE_854_defs 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)
    (value const-decl "real" IEEE_854_values nil)
    (zero? const-decl "bool" IEEE_854_values nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_expt application-judgement "int" exponentiation nil)
    (nzreal_expt application-judgement "nzreal" exponentiation nil)
    (nzint_times_nzint_is_nzint application-judgement "nzint" integers
     nil))
   nil)))

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.