Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/ACCoRD/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 12 kB image not shown  

Quelle  tca_3D_interval.prf   Sprache: Lisp

 
(tca_3D_interval
 (tca_3D_interval_TCC1 0
  (tca_3D_interval_TCC1-1 nil 3487680517 ("" (subtype-tcc) nil nil)
   ((nnreal type-eq-decl nil real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (H formal-const-decl "posreal" tca_3D_interval nil)
    (D formal-const-decl "posreal" tca_3D_interval nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (tca_3D const-decl "nnreal" tca_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
 (tca_3D_interval_TCC2 0
  (tca_3D_interval_TCC2-1 nil 3487680517 ("" (subtype-tcc) nil nil)
   ((nnreal type-eq-decl nil real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (H formal-const-decl "posreal" tca_3D_interval nil)
    (D formal-const-decl "posreal" tca_3D_interval nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (tca_3D const-decl "nnreal" tca_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
 (tca_3D_interval_TCC3 0
  (tca_3D_interval_TCC3-1 nil 3487680517 ("" (subtype-tcc) nil nil)
   ((nnreal type-eq-decl nil real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (H formal-const-decl "posreal" tca_3D_interval nil)
    (D formal-const-decl "posreal" tca_3D_interval nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (tca_3D const-decl "nnreal" tca_3D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
 (tca_3D_interval_def 0
  (tca_3D_interval_def-1 nil 3487680518
   ("" (skeep)
    (("" (expand "tca_3D_interval")
      (("" (lift-if)
        (("" (ground)
          (("1" (lemma "tca_3D_def") (("1" (inst?) nil nil)) nil)
           ("2" (hide 2)
            (("2" (lemma "tca_3D_right_increasing")
              (("2" (inst - "B" "t" "s" "v")
                (("2" (assert)
                  (("2" (expand "cyl_norm_sq_fun")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (lemma "tca_3D_left_decreasing")
            (("3" (inst - "t" "T" "s" "v")
              (("3" (assert)
                (("3" (expand "cyl_norm_sq_fun")
                  (("3" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tca_3D_interval const-decl "Lookahead[B, T]" tca_3D_interval nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (Lookahead type-eq-decl nil Lookahead nil)
    (T formal-const-decl "{AB: posreal | AB > B}" tca_3D_interval nil)
    (B formal-const-decl "nnreal" tca_3D_interval nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nnreal type-eq-decl nil real_types nil)
    (tca_3D_def formula-decl nil tca_3D 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" tca_3D_interval nil)
    (H formal-const-decl "posreal" tca_3D_interval nil)
    (tca_3D_right_increasing formula-decl nil tca_3D nil)
    (cyl_norm_sq_fun const-decl "nnreal" tca_3D nil)
    (tca_3D_left_decreasing formula-decl nil tca_3D nil))
   shostak))
 (tca_3D_interval_conflict 0
  (tca_3D_interval_conflict-1 nil 3487680646
   ("" (lemma "conflict_at_cyl_norm_sq")
    (("" (skeep)
      (("" (ground)
        (("1" (expand "conflict_3D?")
          (("1" (skosimp*)
            (("1" (inst - "s" "t!1" "v")
              (("1" (assert)
                (("1" (lemma "tca_3D_interval_def")
                  (("1" (inst - "s" "t!1" "v") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (inst - "s" "tca_3D_interval(s,v)" "v")
          (("2" (assert)
            (("2" (flatten)
              (("2" (expand "conflict_3D?")
                (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tca_3D_interval const-decl "Lookahead[B, T]" tca_3D_interval nil)
    (conflict_3D? const-decl "bool" cd3d nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (B formal-const-decl "nnreal" tca_3D_interval nil)
    (T formal-const-decl "{AB: posreal | AB > B}" tca_3D_interval nil)
    (Lookahead type-eq-decl nil Lookahead nil)
    (tca_3D_interval_def formula-decl nil tca_3D_interval nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (conflict_at_cyl_norm_sq formula-decl nil tca_3D 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" tca_3D_interval nil)
    (H formal-const-decl "posreal" tca_3D_interval nil))
   shostak))
 (tca_3D_interval_conflict_at 0
  (tca_3D_interval_conflict_at-1 nil 3487680824
   ("" (skeep)
    (("" (rewrite "tca_3D_interval_conflict")
      (("" (lemma "conflict_at_cyl_norm_sq")
        (("" (inst?) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((tca_3D_interval_conflict formula-decl nil tca_3D_interval nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (B formal-const-decl "nnreal" tca_3D_interval nil)
    (T formal-const-decl "{AB: posreal | AB > B}" tca_3D_interval nil)
    (Lookahead type-eq-decl nil Lookahead nil)
    (tca_3D_interval const-decl "Lookahead[B, T]" tca_3D_interval nil)
    (conflict_at_cyl_norm_sq formula-decl nil tca_3D 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (D formal-const-decl "posreal" tca_3D_interval nil)
    (H formal-const-decl "posreal" tca_3D_interval nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.