Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: abstract_min.prf Sprache: PVS

Original von: PVS^©

(parallel_2D
(abs_det_par 0
  (abs_det_par-1 nil 3430221694
   ("" (skeep)
    (("" (case-replace "det(nzu, nzv) = 0 IFF sq(det(nzu, nzv)) = 0")
      (("1" (hide -1)
        (("1" (rewrite "sq_det")
          (("1" (rewrite "sq_norm" :dir rl)
            (("1" (rewrite "sq_norm" :dir rl)
              (("1" (split)
                (("1" (flatten) (("1" (grind) nil nil)) nil)
                 ("2" (flatten)
                  (("2" (lemma "sq_eq_abs")
                    (("2" (inst -1 "^(nzu)*^(nzv)" "1")
                      (("2" (rewrite "sq_1")
                        (("2" (expand "abs" -1 2)
                          (("2" (replaces -1 :dir rl)
                            (("2" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (rewrite "sq_eq_0") (("2" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def 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)
    (det const-decl "real" det_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_det formula-decl nil det_2D nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (Normalized type-eq-decl nil vectors_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (sq_1 formula-decl nil sq "reals/")
    (sq_eq_abs formula-decl nil sq "reals/")
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (^ const-decl "Normalized" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (sq_norm formula-decl nil vectors_2D nil)
    (sq_eq_0 formula-decl nil sq "reals/"))
   nil))
(parallel_dot_1 0
  (parallel_dot_1-2 nil 3430222307
   ("" (skeep)
    (("" (expand "parallel?")
      (("" (prop)
        (("1" (skeep -1)
          (("1" (replaces -1)
            (("1" (lemma "norm_scal")
              (("1" (inst?)
                (("1" (expand "^")
                  (("1" (replaces -1)
                    (("1" (rewrite "dot_scal_canon")
                      (("1" (cross-mult 1)
                        (("1" (lemma "dot_sq_norm")
                          (("1" (inst -1 "nzv")
                            (("1" (replaces -1)
                              (("1"
                                (expand "sq")
                                (("1"
                                  (rewrite "abs_div")
                                  (("1"
                                    (rewrite "abs_mult")
                                    (("1"
                                      (rewrite "abs_abs")
                                      (("1"
                                        (rewrite "abs_div")
                                        (("1"
                                          (rewrite "abs_mult")
                                          (("1"
                                            (rewrite "abs_mult")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "abs_det_par")
          (("2" (inst?)
            (("2" (assert)
              (("2" (hide -2)
                (("2" (expand "det")
                  (("2" (typepred "nzv")
                    (("2" (rewrite "nzv_xy_neq_0")
                      (("2" (expand "*")
                        (("2" (typepred "nzu")
                          (("2" (rewrite "nzv_xy_neq_0")
                            (("2" (split -2)
                              (("1"
                                (inst 1 "nzu`x/nzv`x")
                                (("1" (decompose-equality 1) nil nil)
                                 ("2" (grind-reals) nil nil))
                                nil)
                               ("2"
                                (inst 1 "nzu`y/nzv`y")
                                (("1" (decompose-equality 1) nil nil)
                                 ("2" (grind-reals) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((parallel? const-decl "bool" vectors_2D nil)
    (abs_det_par formula-decl nil parallel_2D nil)
    (det const-decl "real" det_2D nil)
    (nzv_xy_neq_0 formula-decl nil vectors_2D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nzu skolem-const-decl "Nz_vector" parallel_2D nil)
    (nzv skolem-const-decl "Nz_vector" parallel_2D nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (norm_scal formula-decl nil vectors_2D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (^ const-decl "Normalized" vectors_2D nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (dot_scal_canon formula-decl nil vectors_2D nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (abs_div formula-decl nil real_props nil)
    (abs_abs formula-decl nil real_props nil)
    (abs_mult formula-decl nil real_props nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (times_div2 formula-decl nil real_props nil)
    (* const-decl "real" vectors_2D nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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))
   nil)
  (parallel_dot_1-1 nil 3430221756
   ("" (skeep)
    (("" (prop)
      (("1" (expand "paral?")
        (("1" (skeep -1)
          (("1" (replaces -1)
            (("1" (lemma "norm_scal")
              (("1" (inst?)
                (("1" (expand "^")
                  (("1" (replaces -1)
                    (("1" (rewrite "dot_scal_canon")
                      (("1" (cross-mult 1)
                        (("1" (lemma "dot_sq_norm")
                          (("1" (inst -1 "nzv")
                            (("1" (replaces -1)
                              (("1"
                                (expand "sq")
                                (("1"
                                  (rewrite "abs_div")
                                  (("1"
                                    (rewrite "abs_mult")
                                    (("1"
                                      (rewrite "abs_abs")
                                      (("1"
                                        (rewrite "abs_div")
                                        (("1"
                                          (rewrite "abs_mult")
                                          (("1"
                                            (rewrite "abs_mult")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "paral?")
        (("2" (lemma "abs_det_par")
          (("2" (inst?)
            (("2" (assert)
              (("2" (hide -2)
                (("2" (expand "det")
                  (("2" (typepred "nzv")
                    (("2" (flatten)
                      (("2" (rewrite "norm_xy_eq_0")
                        (("2" (typepred "nzu")
                          (("2" (flatten)
                            (("2" (rewrite "norm_xy_eq_0")
                              (("2"
                                (expand "*")
                                (("2"
                                  (split 2)
                                  (("1"
                                    (inst 3 "nzu`x/nzv`x")
                                    (("1"
                                      (decompose-equality 3)
                                      nil
                                      nil)
                                     ("2" (grind-reals) nil nil)
                                     ("3" (grind-reals) nil nil))
                                    nil)
                                   ("2"
                                    (inst 3 "nzu`y/nzv`y")
                                    (("1"
                                      (decompose-equality 3)
                                      nil
                                      nil)
                                     ("2" (grind-reals) nil nil)
                                     ("3" (grind-reals) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm_scal formula-decl nil vectors_2D nil)
    (^ const-decl "Normalized" vectors_2D nil)
    (dot_scal_canon formula-decl nil vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (dot_scal_left formula-decl nil vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (* const-decl "real" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (det const-decl "real" det_2D nil)
    (norm_xy_eq_0 formula-decl nil vectors_2D nil))
   nil))
(parallel_det_0 0
  (parallel_det_0-1 nil 3430222402
   ("" (skeep)
    (("" (lemma "parallel_dot_1")
      (("" (inst?)
        (("" (lemma "abs_det_par")
          (("" (inst?) (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((parallel_dot_1 formula-decl nil parallel_2D nil)
    (abs_det_par formula-decl nil parallel_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (real nonempty-type-from-decl nil reals nil))
   shostak))
(dot_perpL_parallel 0
  (dot_perpL_parallel-1 nil 3476105424
   ("" (skosimp*)
    (("" (expand "parallel?")
      (("" (expand "perpL")
        (("" (expand "*")
          (("" (typepred "nzu!1")
            (("" (typepred "nzv!1")
              (("" (flatten)
                (("" (case-replace "nzv!1`y = 0")
                  (("1" (assert)
                    (("1" (mult-cases -2)
                      (("1" (inst + "-nzu!1`y/nzv!1`x")
                        (("1" (assert) nil nil)
                         ("2" (assert)
                          (("2" (flatten)
                            (("2" (cross-mult -1)
                              (("2"
                                (reveal 1)
                                (("2"
                                  (apply-extensionality 2 :hide? t)
                                  (("2"
                                    (apply-extensionality 3 :hide? t)
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("3" (flatten)
                          (("3" (apply-extensionality :hide? t) nil
                            nil))
                          nil))
                        nil)
                       ("2" (apply-extensionality 1 :hide? t) nil nil))
                      nil))
                    nil)
                   ("2" (case-replace "nzv!1`x = 0")
                    (("1" (assert)
                      (("1" (mult-cases -2)
                        (("1" (inst + "nzu!1`x/nzv!1`y")
                          (("1" (assert) nil nil)
                           ("2" (flatten)
                            (("2" (cross-mult -1)
                              (("2"
                                (assert)
                                (("2"
                                  (apply-extensionality 2 :hide? t)
                                  (("2"
                                    (apply-extensionality 3 :hide? t)
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (inst + "-nzu!1`y/nzv!1`x")
                      (("1" (assert) nil nil)
                       ("2" (flatten)
                        (("2" (cross-mult -1)
                          (("2" (assert)
                            (("2" (case-replace "nzu!1`y = 0")
                              (("1"
                                (assert)
                                (("1"
                                  (apply-extensionality 4 :hide? t)
                                  nil
                                  nil))
                                nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (flatten) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((parallel? const-decl "bool" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (zero_times3 formula-decl nil real_props 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)
    (div_cancel3 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nzu!1 skolem-const-decl "Nz_vector" parallel_2D nil)
    (- const-decl "[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)
    (nzv!1 skolem-const-decl "Nz_vector" parallel_2D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (perpL const-decl "Vect2" perpendicular_2D nil))
   nil))
(dot_perpR_parallel 0
  (dot_perpR_parallel-1 nil 3476105449
   ("" (skosimp*)
    (("" (expand "parallel?")
      (("" (expand "perpR")
        (("" (expand "*")
          (("" (typepred "nzu!1")
            (("" (typepred "nzv!1")
              (("" (flatten)
                (("" (case-replace "nzv!1`y = 0")
                  (("1" (assert)
                    (("1" (mult-cases -2)
                      (("1" (inst + "nzu!1`y/nzv!1`x")
                        (("1" (assert) nil nil)
                         ("2" (flatten)
                          (("2" (cross-mult -1)
                            (("2" (assert)
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                (("2"
                                  (apply-extensionality 2 :hide? t)
                                  nil
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("3" (assert)
                          (("3" (flatten)
                            (("3" (apply-extensionality 1 :hide? t) nil
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (apply-extensionality 1 :hide? t) nil nil))
                      nil))
                    nil)
                   ("2" (case-replace "nzv!1`x = 0")
                    (("1" (assert)
                      (("1" (mult-cases -2)
                        (("1" (inst + "-nzu!1`x/nzv!1`y")
                          (("1" (assert) nil nil)
                           ("2" (flatten)
                            (("2" (cross-mult -1)
                              (("2"
                                (assert)
                                (("2"
                                  (apply-extensionality 2 :hide? t)
                                  (("2"
                                    (apply-extensionality 3 :hide? t)
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (inst + "nzu!1`y/nzv!1`x")
                      (("1" (assert) nil nil)
                       ("2" (flatten)
                        (("2" (cross-mult -1)
                          (("2" (assert)
                            (("2" (apply-extensionality 3 :hide? t)
                              (("1"
                                (apply-extensionality 4 :hide? t)
                                nil
                                nil)
                               ("2"
                                (apply-extensionality 4 :hide? t)
                                nil
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (flatten) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((parallel? const-decl "bool" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (zero_times3 formula-decl nil real_props 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)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel3 formula-decl nil real_props nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nzu!1 skolem-const-decl "Nz_vector" parallel_2D 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)
    (nzv!1 skolem-const-decl "Nz_vector" parallel_2D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (perpR const-decl "Vect2" perpendicular_2D nil))
   nil)))

¤ Dauer der Verarbeitung: 0.42 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

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.