products/sources/formale Sprachen/C/Lyx/config image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: vectors_cos.prf   Sprache: Unknown

(vectors_cos
 (cosines_law 0
  (cosines_law-1 nil 3254159790
   ("" (skosimp*)
    (("" (skoletin* +)
      (("" (flatten)
        (("" (both-sides-f -1 "sqv")
          (("" (expand "sqv" -1)
            ((""
              (case-replace "(va!1 - vb!1)*(va!1 - vb!1) =
                                               va!1*va!1 + vb!1*vb!1 - 2*va!1*vb!1")
              (("1" (hide -1)
                (("1" (rewrite "dot_sq_norm")
                  (("1" (rewrite "dot_sq_norm")
                    (("1" (rewrite "dot_sq_norm")
                      (("1" (assertnil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (hide-all-but 1)
                  (("2" (rewrite "dot_sub_right[n]")
                    (("2" (rewrite "dot_sub_left[n]")
                      (("2" (rewrite "dot_sub_left[n]")
                        (("2" (assert)
                          (("2" (rewrite "dot_comm")
                            (("2" (rewrite "dot_comm")
                              (("2" (assertnil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IFF const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" vectors_cos nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (* const-decl "real" vectors nil)
    (cos const-decl "real" trig_basic "trig/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "real" vectors nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv const-decl "nnreal" vectors nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (* const-decl "Vector" vectors nil)
    (dot_sq_norm formula-decl nil vectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil vectors nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (dot_sub_left formula-decl nil vectors nil)
    (dot_comm formula-decl nil vectors nil)
    (dot_sub_right formula-decl nil vectors nil))
   nil))
 (angle_exists 0
  (angle_exists-1 nil 3254159790
   ("" (skosimp*)
    (("" (assert)
      (("" (case "norm(va!1)*norm(vb!1) = 0")
        (("1" (assert)
          (("1" (inst + "0")
            (("1" (rewrite "cos_0")
              (("1" (mult-cases -1)
                (("1" (lemma "norm_eq_0[n]")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (replace -1)
                        (("1" (hide -1)
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1"
                                (rewrite "dot_zero_left")
                                (("1" (assertnil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (lemma "norm_eq_0[n]")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (replace -1)
                        (("2" (hide -1)
                          (("2" (replace -1)
                            (("2" (hide -1) (("2" (assertnil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "dot_norm[n]")
          (("2" (inst?)
            (("2" (flatten)
              (("2"
                (case " -1 <= va!1 * vb!1 / (norm(va!1) * norm(vb!1)) AND
                         va!1 * vb!1 / (norm(va!1) * norm(vb!1)) <= 1")
                (("1" (flatten)
                  (("1" (hide -3 -4)
                    (("1"
                      (inst +
                       "arccos(va!1 * vb!1/( norm(va!1) * norm(vb!1))) ")
                      (("1" (rewrite "cos_arccos")
                        (("1" (cross-mult 2) nil nil)) nil)
                       ("2" (ground) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (prop)
                    (("1" (cross-mult 1) (("1" (assertnil nil)) nil)
                     ("2" (cross-mult 1) (("2" (assertnil nil)) nil))
                    nil))
                  nil)
                 ("3" (assertnil nil) ("4" (assertnil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (dot_norm formula-decl nil vectors nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (va!1 skolem-const-decl "Vector[n]" vectors_cos nil)
    (vb!1 skolem-const-decl "Vector[n]" vectors_cos nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin "trig/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi_lb const-decl "posreal" trig_basic "trig/")
    (pi_ub const-decl "posreal" trig_basic "trig/")
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     "trig/")
    (nnreal_le_pi nonempty-type-eq-decl nil acos "trig/")
    (cos const-decl "real" trig_basic "trig/")
    (arccos const-decl "{x: nnreal_le_pi | y = cos(x)}" trig_inverses
     "trig/")
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div2 formula-decl nil real_props nil)
    (cos_arccos formula-decl nil trig_inverses "trig/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "real" vectors nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (cos_0 formula-decl nil trig_basic "trig/")
    (dot_zero_right formula-decl nil vectors nil)
    (norm_eq_0 formula-decl nil vectors nil)
    (dot_zero_left formula-decl nil vectors nil)
    (zero_times3 formula-decl nil real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" vectors_cos nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors nil))
   nil))
 (angle_between_TCC1 0
  (angle_between_TCC1-2 nil 3430837199
   ("" (skosimp*)
    (("" (lemma "dot_norm[n]")
      (("" (inst?)
        (("" (assert)
          (("" (ground)
            (("1" (cross-mult 1) (("1" (assertnil nil)) nil)
             ("2" (cross-mult 1) (("2" (assertnil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((n formal-const-decl "posnat" vectors_cos nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int 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)
    (dot_norm formula-decl nil vectors nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors nil)
    (Nz_vector type-eq-decl nil vectors nil)
    (zero const-decl "Vector" vectors nil)
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil)
  (angle_between_TCC1-1 nil 3254159790
   ("" (skosimp*) (("" (mult-cases -1) nil nil)) nil)
   ((Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (norm const-decl "nnreal" vectors nil)
    (Nz_vector type-eq-decl nil vectors nil))
   nil))
 (cosines_law_bnd 0
  (cosines_law_bnd-1 nil 3254159790
   ("" (skosimp*)
    (("" (skoletin 1)
      (("" (skoletin 1)
        (("" (skoletin 1)
          (("" (flatten)
            (("" (lemma "cosines_law")
              (("" (inst?)
                (("" (assert)
                  (("" (lemma "angle_exists")
                    (("" (inst?)
                      (("" (skosimp*)
                        (("" (assert)
                          (("" (inst - "ab!1")
                            (("" (assert)
                              ((""
                                (replace -3 * rl)
                                ((""
                                  (hide -3)
                                  ((""
                                    (replace -4 * rl)
                                    ((""
                                      (hide -4)
                                      ((""
                                        (replace -4 * rl)
                                        ((""
                                          (hide -4)
                                          ((""
                                            (typepred "cos(ab!1)")
                                            ((""
                                              (mult-by -2 "2*a*b")
                                              ((""
                                                (expand "sq")
                                                (("" (assertnil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((IFF const-decl "[bool, bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" vectors_cos nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (- const-decl "real" vectors nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cosines_law formula-decl nil vectors_cos nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic "trig/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (cos const-decl "real" trig_basic "trig/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (angle_exists formula-decl nil vectors_cos nil))
   nil))
 (cosines_law_ge 0
  (cosines_law_ge-1 nil 3254159790
   ("" (skosimp*)
    (("" (assert)
      (("" (flatten)
        (("" (lemma "cosines_law_bnd")
          (("" (inst?)
            (("" (assert)
              (("" (assert)
                (("" (expand "abs")
                  (("" (lift-if)
                    (("" (ground)
                      (("1" (lemma "sq_ge")
                        (("1" (inst?)
                          (("1" (inst -1 "-(norm(va!1)- norm(vb!1))")
                            (("1" (assert)
                              (("1" (rewrite "sq_neg"nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (lemma "sq_ge")
                        (("2" (inst?) (("2" (assertnil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cosines_law_bnd formula-decl nil vectors_cos nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (norm const-decl "nnreal" vectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq_neg formula-decl nil sq "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_ge formula-decl nil sq "reals/")
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" vectors_cos nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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))
   nil))
 (cosines_law_le 0
  (cosines_law_le-1 nil 3254159790
   ("" (skosimp*)
    (("" (assert)
      (("" (flatten)
        (("" (replace -1) (("" (rewrite "norm_sub_le"nil nil)) nil))
        nil))
      nil))
    nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (n formal-const-decl "posnat" vectors_cos nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int 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)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (norm_sub_le formula-decl nil vectors nil))
   nil)))


[ Dauer der Verarbeitung: 0.6 Sekunden  (vorverarbeitet)  ]