Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: circle_solutions.prf Sprache: Lisp

Original von: PVS^©

(circle_solutions
(circle_solution_horizontal 0
  (circle_solution_horizontal-1 nil 3466332995
   ("" (skeep)
    (("" (expand "vertical_conflict?")
      (("" (expand "circle_solution?")
        (("" (flatten)
          (("" (case-replace "v`z = 0")
            (("1" (expand "vertical_solution?" -5)
              (("1" (assert) nil nil)) nil)
             ("2" (assert)
              (("2" (lemma "vertical_solution_Theta_H")
                (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (vertical_conflict? const-decl "bool" vertical nil)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal 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)
    (vertical_solution_Theta_H formula-decl nil vertical 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)
    (H formal-const-decl "posreal" circle_solutions nil)
    (vertical_solution? const-decl "bool" vertical 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)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (circle_solution? const-decl "bool" circle_solutions nil))
   shostak))
(circle_solution_vertical_TCC1 0
  (circle_solution_vertical_TCC1-1 nil 3466342106
   ("" (skeep)
    (("" (assert)
      (("" (expand "circle_solution?")
        (("" (flatten)
          (("" (lemma "circle_solution_2D_Delta_ge_0")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    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 "boolean" notequal nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign "reals/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (circle_solution_2D_Delta_ge_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" circle_solutions nil)
    (circle_solution? const-decl "bool" circle_solutions nil))
   nil))
(circle_solution_vertical 0
  (circle_solution_vertical-2 nil 3466349252
   ("" (skeep)
    (("" (expand "horizontal_conflict?")
      (("" (expand "circle_solution?")
        (("" (flatten)
          (("" (case-replace "vect2(v) = zero")
            (("1" (expand "circle_solution_2D?" -4)
              (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)
             ("2" (assert)
              (("2" (lemma "circle_solution_2D_Theta_D")
                (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((horizontal_conflict? const-decl "bool" horizontal 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 "boolean" notequal nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign "reals/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (circle_solution_2D_Theta_D formula-decl nil horizontal 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)
    (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" circle_solutions nil)
    (circle_solution_2D? const-decl "bool" horizontal nil)
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (dot_zero_right formula-decl nil vectors_2D "vectors/")
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (vect2 const-decl "Vect2" vect_3D_2D "vectors/")
    (Vect3 type-eq-decl nil vectors_3D_def "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)
    (circle_solution? const-decl "bool" circle_solutions nil))
   nil)
  (circle_solution_vertical-1 nil 3466349211 ("" (postpone) nil nil)
   nil shostak))
(circle_solution_meets_criterion 0
  (circle_solution_meets_criterion-1 nil 3461661297
   ("" (skeep)
    (("" (expand "circle_solution?")
      (("" (flatten)
        (("" (expand "circle_solution_2D?")
          (("" (flatten)
            (("" (expand "vertical_solution?")
              (("" (flatten)
                (("" (expand "circle_criterion?")
                  (("" (rewrite "vect2_add")
                    (("" (rewrite "vect2_scal")
                      (("" (assert)
                        (("" (rewrite "vz_distr_add")
                          (("" (rewrite "vz_scal")
                            (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((circle_solution? const-decl "bool" circle_solutions nil)
    (circle_solution_2D? const-decl "bool" horizontal nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (vertical_solution? const-decl "bool" vertical nil)
    (circle_criterion? const-decl "bool" circle_criterion nil)
    (vect2_scal formula-decl nil vect_3D_2D "vectors/")
    (vz_distr_add formula-decl nil vectors_3D "vectors/")
    (vz_scal formula-decl nil vectors_3D "vectors/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "Vector" vectors_3D "vectors/")
    (Vector type-eq-decl nil vectors_3D "vectors/")
    (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)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (vect2_add formula-decl nil vect_3D_2D "vectors/"))
   shostak))
(circle_solution_independence 0
  (circle_solution_independence-1 nil 3461665991
   ("" (skeep)
    (("" (lemma "circle_solution_meets_criterion")
      (("" (inst?)
        (("" (assert)
          (("" (lemma "circle_criterion_at_independence")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((circle_solution_meets_criterion formula-decl nil circle_solutions
     nil)
    (H formal-const-decl "posreal" circle_solutions nil)
    (D formal-const-decl "posreal" circle_solutions 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)
    (circle_criterion_at_independence formula-decl nil circle_criterion
     nil)
    (Vect3 type-eq-decl nil vectors_3D_def "vectors/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal 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))
   shostak)))

¤ Dauer der Verarbeitung: 0.23 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.