Quelle cd2d_inf.prf Sprache: Lisp

(cd2d_inf
(detection_2D_inf_TCC1 0
  (detection_2D_inf_TCC1-1 nil 3483958897 ("" (subtype-tcc) nil 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (det const-decl "real" det_2D "vectors/")
    (D formal-const-decl "posreal" cd2d_inf 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)
    (Delta const-decl "real" horizontal nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
(detection_2D_inf_correct 0
  (detection_2D_inf_correct-1 nil 3483958907
   ("" (skeep)
    (("" (assert)
      (("" (expand "detection_2D_inf")
        (("" (lift-if)
          (("" (assert)
            (("" (ground)
              (("" (lemma "horizontal_los_inside_Theta")
                (("" (inst?)
                  (("" (assert)
                    (("" (expand "max" -3)
                      (("" (lift-if) (("" (ground) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_nz_pos application-judgement "posreal" sq "reals/")
    (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)
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (nnreal type-eq-decl nil real_types nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (horizontal_los_inside_Theta formula-decl nil horizontal 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" cd2d_inf nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (detection_2D_inf const-decl "[nnreal, nnreal]" cd2d_inf nil))
   shostak))
(detection_2D_inf_complete 0
  (detection_2D_inf_complete-1 nil 3483959002
   ("" (skeep)
    (("" (assert)
      (("" (flatten)
        (("" (expand "detection_2D_inf")
          (("" (lift-if)
            (("" (assert)
              (("" (lemma "Delta_gt_0")
                (("" (inst?)
                  (("" (assert)
                    (("" (split -)
                      (("1" (assert)
                        (("1" (lemma "horizontal_los_inside_Theta")
                          (("1" (inst?)
                            (("1" (assert)
                              (("1"
                                (flatten)
                                (("1"
                                  (expand "max")
                                  (("1"
                                    (lift-if)
                                    (("1"
                                      (lift-if)
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (expand "horizontal_conflict_ever?")
                          (("2" (inst + "t") nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (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)
    (detection_2D_inf const-decl "[nnreal, nnreal]" cd2d_inf nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (horizontal_los_inside_Theta formula-decl nil horizontal nil)
    (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
    (nnreal type-eq-decl nil real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (horizontal_conflict_ever? const-decl "bool" horizontal nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Delta_gt_0 formula-decl nil horizontal 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" cd2d_inf nil))
   shostak))
(conflict_detection_2D_inf 0
  (conflict_detection_2D_inf-1 nil 3483959293
   ("" (skeep)
    (("" (assert)
      (("" (ground)
        (("1" (lemma "detection_2D_inf_complete")
          (("1" (expand "horizontal_conflict?")
            (("1" (skosimp*)
              (("1" (inst - "nzv" "s" "nnt!1") (("1" (assert) nil nil))
                nil))
              nil))
            nil))
          nil)
         ("2"
          (name "tav"
                "(detection_2D_inf(s, nzv)`1 + detection_2D_inf(s, nzv)`2)/2")
          (("2" (lemma "detection_2D_inf_correct")
            (("2" (inst - "nzv" "s" "tav")
              (("2" (assert)
                (("2" (split -)
                  (("1" (expand "horizontal_conflict?")
                    (("1" (inst + "tav") nil nil)) nil)
                   ("2" (hide 2) (("2" (assert) nil nil)) nil)
                   ("3" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (detection_2D_inf const-decl "[nnreal, nnreal]" cd2d_inf nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (detection_2D_inf_correct formula-decl nil cd2d_inf nil)
    (detection_2D_inf_complete formula-decl nil cd2d_inf nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (horizontal_conflict? const-decl "bool" horizontal nil))
   nil))
(cd2d_inf 0
  (cd2d_inf-1 nil 3483959557
   ("" (skeep)
    (("" (ground)
      (("1" (expand "cd2d_inf?")
        (("1" (case "v = zero")
          (("1" (replace -1)
            (("1" (expand "horizontal_conflict?")
              (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (flatten)
            (("2" (lemma "Delta_gt_0")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (lemma "horizontal_conflict_ever")
                    (("2" (inst?)
                      (("2" (assert)
                        (("2" (lemma "sdotv_lt_0")
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "cd2d_inf?")
        (("2" (split -)
          (("1" (expand "horizontal_conflict?")
            (("1" (inst + "0") (("1" (assert) nil nil)) nil)) nil)
           ("2" (flatten)
            (("2" (lemma "horizontal_tca_los")
              (("2" (inst?)
                (("1" (assert)
                  (("1" (expand "horizontal_conflict?")
                    (("1" (inst + "horizontal_tca(s,v)")
                      (("1" (assert)
                        (("1" (expand "horizontal_tca")
                          (("1" (cross-mult 1)
                            (("1" (assert)
                              (("1"
                                (ground)
                                (("1"
                                  (lemma "sqv_eq_0")
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (replace -1)
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (replace -1) (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((zero const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (horizontal_conflict? const-decl "bool" horizontal nil)
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (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)
    (D formal-const-decl "posreal" cd2d_inf 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_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)
    (Delta_gt_0 formula-decl nil horizontal 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)
    (sdotv_lt_0 formula-decl nil horizontal nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (horizontal_conflict_ever formula-decl nil horizontal nil)
    (cd2d_inf? const-decl "bool" cd2d_inf nil)
    (scal_0 formula-decl nil vectors_2D "vectors/")
    (horizontal_tca_los formula-decl nil horizontal nil)
    (horizontal_tca const-decl "real" definitions nil)
    (s skolem-const-decl "Vect2" cd2d_inf nil)
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (sqv_zero formula-decl nil vectors_2D "vectors/")
    (dot_zero_right formula-decl nil vectors_2D "vectors/")
    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_2D "vectors/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_mult_pos_neg_ge1 formula-decl nil extra_real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (v skolem-const-decl "Vect2" cd2d_inf nil)
    (/= const-decl "boolean" notequal nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

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.