Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: horizontal_sq_dtca.prf Sprache: Lisp

Original von: PVS^©

(horizontal_sq_dtca
(IMP_vect_deriv_2D_TCC1 0
  (IMP_vect_deriv_2D_TCC1-1 nil 3474200394
   ("" (expand "deriv_domain?")
    (("" (skeep)
      (("" (inst + "e/2")
        (("" (expand "abs") (("" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (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)
    (/ 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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
(IMP_vect_deriv_2D_TCC2 0
  (IMP_vect_deriv_2D_TCC2-1 nil 3474200394
   ("" (expand "not_one_element?")
    (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
(horizontal_sq_dtca_diff_TCC1 0
  (horizontal_sq_dtca_diff_TCC1-1 nil 3465680128
   ("" (skosimp*) nil nil) nil nil))
(horizontal_sq_dtca_diff 0
  (horizontal_sq_dtca_diff-1 nil 3465680179
   ("" (skeep)
    (("" (expand "horizontal_sq_dtca")
      (("" (lemma "derivable_div")
        ((""
          (inst - "LAMBDA (r): sq(det(s,V(r)))"
           "LAMBDA (r): sqv(V(r))")
          (("1" (expand "/" -1)
            (("1" (expand "derivable?" -1)
              (("1" (inst - "r1") nil nil)) nil))
            nil)
           ("2" (lemma "sqvdot_diff") (("2" (inst - "V") nil nil)) nil)
           ("3" (skosimp*)
            (("3" (inst - "r!1")
              (("3" (lemma "sqv_eq_0")
                (("3" (inst - "V(r!1)") (("3" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("4" (expand "sq" 1)
            (("4" (lemma "detsv_diff")
              (("4" (inst - "V" "s")
                (("4" (lemma "derivable_prod")
                  (("4"
                    (inst - "LAMBDA (r): det(s, V(r))"
                     "LAMBDA (r): det(s, V(r))")
                    (("1" (expand "*" -1) (("1" (propax) nil nil)) nil)
                     ("2" (expand "detsv") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((horizontal_sq_dtca const-decl "real" definitions nil)
    (V skolem-const-decl
     "(LAMBDA (V: [real -> Vect2]): derivable_rv?(V))"
     horizontal_sq_dtca nil)
    (derivable_rv? const-decl "bool" deriv_real_vect2 "vect_analysis/")
    (s skolem-const-decl "Vect2" horizontal_sq_dtca nil)
    (det const-decl "real" det_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (derivable? const-decl "bool" derivatives "analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (nz_deriv_fun type-eq-decl nil derivatives "analysis/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (sqvdot_diff formula-decl nil vect_deriv_2D "vect_analysis/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (detsv_diff formula-decl nil vect_deriv_2D "vect_analysis/")
    (derivable_prod judgement-tcc nil derivatives "analysis/")
    (detsv const-decl "real" vect_deriv_2D "vect_analysis/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (derivable_div judgement-tcc nil derivatives "analysis/")
    (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))
   nil))
(horizontal_sq_dtca_deriv_TCC1 0
  (horizontal_sq_dtca_deriv_TCC1-1 nil 3460201805
   ("" (skeep)
    (("" (lemma "horizontal_sq_dtca_diff")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((horizontal_sq_dtca_diff formula-decl nil horizontal_sq_dtca nil)
    (derivable_rv? const-decl "bool" deriv_real_vect2 "vect_analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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))
(horizontal_sq_dtca_deriv_TCC2 0
  (horizontal_sq_dtca_deriv_TCC2-2 nil 3465680322
   ("" (skeep)
    (("" (skeep)
      (("" (skeep)
        (("" (rewrite "sq_eq_0")
          (("" (rewrite "sqv_eq_0")
            (("" (inst -1 "r") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_eq_0 formula-decl nil sq "reals/")
    (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)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/"))
   nil)
  (horizontal_sq_dtca_deriv_TCC2-1 nil 3460201805
   ("" (skeep)
    (("" (expand "horizontal_sq_dtca")
      (("" (lemma "derivable_div")
        ((""
          (inst - "LAMBDA (r): sq(det(s,V(r)))"
           "LAMBDA (r): sqv(V(r))")
          (("1" (expand "/" -1)
            (("1" (expand "derivable?" -1)
              (("1" (inst - "r1") nil nil)) nil))
            nil)
           ("2" (lemma "sqvdot_diff") (("2" (inst - "V") nil nil)) nil)
           ("3" (skosimp*)
            (("3" (inst - "r!1")
              (("3" (lemma "sqv_eq_0")
                (("3" (inst - "V(r!1)") (("3" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("4" (expand "sq" 1)
            (("4" (lemma "detsv_diff")
              (("4" (inst - "V" "s")
                (("4" (lemma "derivable_prod")
                  (("4"
                    (inst - "LAMBDA (r): det(s, V(r))"
                     "LAMBDA (r): det(s, V(r))")
                    (("1" (expand "*" -1) (("1" (propax) nil nil)) nil)
                     ("2" (expand "detsv") (("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((det const-decl "real" det_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (nz_deriv_fun type-eq-decl nil derivatives "analysis/")
    (sqvdot_diff formula-decl nil vect_deriv_2D "vect_analysis/")
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (detsv_diff formula-decl nil vect_deriv_2D "vect_analysis/")
    (derivable_prod judgement-tcc nil derivatives "analysis/")
    (detsv const-decl "real" vect_deriv_2D "vect_analysis/")
    (derivable_div judgement-tcc nil derivatives "analysis/"))
   nil))
(horizontal_sq_dtca_deriv 0
  (horizontal_sq_dtca_deriv-1 nil 3465660655
   ("" (skeep)
    (("" (lemma "detsv_diff")
      (("" (inst - "V" "s")
        (("" (expand "detsv")
          (("" (copy -1)
            (("" (expand "derivable?" -1)
              (("" (inst - "r1")
                (("" (assert)
                  (("" (expand "horizontal_sq_dtca")
                    (("" (lemma "deriv_div")
                      ((""
                        (inst - "lambda (r: real): sq(det(s,V(r)))"
                         "lambda (r: real): sqv(V(r))" "r1")
                        (("1" (assert)
                          (("1" (split -1)
                            (("1" (expand "/" -1 1)
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (lemma "deriv_prod")
                                    (("1"
                                      (inst
                                       -
                                       "lambda (r: real): det(s,V(r))"
                                       "lambda (r: real): det(s,V(r))"
                                       "r1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "*" -1)
                                          (("1"
                                            (expand "sq" 1 1)
                                            (("1"
                                              (replace -1)
                                              (("1"
                                                (hide -1)
                                                (("1"
                                                  (lemma
                                                   "detsvp_deriv")
                                                  (("1"
                                                    (inst
                                                     -
                                                     "V"
                                                     "r1"
                                                     "s")
                                                    (("1"
                                                      (expand "detsv")
                                                      (("1"
                                                        (expand
                                                         "deriv"
                                                         -1)
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (lemma
                                                               "sqvdot_deriv")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "V"
                                                                 "r1")
                                                                (("1"
                                                                  (expand
                                                                   "deriv"
                                                                   -1)
                                                                  (("1"
                                                                    (replace
                                                                     -1)
                                                                    (("1"
                                                                      (hide
                                                                       -1)
                                                                      (("1"
                                                                        (expand
                                                                         "sq")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "sq" 1)
                              (("2"
                                (lemma "derivable_prod")
                                (("2"
                                  (inst
                                   -
                                   "LAMBDA (r): det(s, V(r))"
                                   "LAMBDA (r): det(s, V(r))")
                                  (("2"
                                    (expand "*" -1)
                                    (("2"
                                      (expand "derivable?" -1)
                                      (("2" (inst - "r1") nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("3" (lemma "sqvdot_diff")
                              (("3"
                                (inst - "V")
                                (("3"
                                  (expand "derivable?" -1)
                                  (("3" (inst - "r1") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skeep)
                          (("2" (inst - "r")
                            (("2" (lemma "sqv_eq_0")
                              (("2"
                                (inst - "V(r)")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (detsv_diff formula-decl nil vect_deriv_2D "vect_analysis/")
    (detsv const-decl "real" vect_deriv_2D "vect_analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (deriv_div formula-decl nil derivatives_def "analysis/")
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (sqvdot_diff formula-decl nil vect_deriv_2D "vect_analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (derivable_prod judgement-tcc nil derivatives "analysis/")
    (/ const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (detsvp_deriv formula-decl nil vect_deriv_2D "vect_analysis/")
    (sqvdot_deriv formula-decl nil vect_deriv_2D "vect_analysis/")
    (dot_scal_left formula-decl nil vectors_2D "vectors/")
    (deriv const-decl "[T -> real]" derivatives "analysis/")
    (deriv_prod formula-decl nil derivatives_def "analysis/")
    (nzreal nonempty-type-eq-decl nil reals nil)
    (det const-decl "real" det_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (V skolem-const-decl
     "(LAMBDA (V: [real -> Vect2]): derivable_rv?(V))"
     horizontal_sq_dtca nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (horizontal_sq_dtca const-decl "real" definitions nil)
    (derivable_rv? const-decl "bool" deriv_real_vect2 "vect_analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
   shostak))
(horizontal_sq_dtca_deriv_simpl 0
  (horizontal_sq_dtca_deriv_simpl-1 nil 3460201787
   ("" (skeep)
    (("" (skoletin* 1 :postfix "p")
      (("1" (cross-mult 1)
        (("1" (cancel-by 1 "2*sq(sqv(vp))")
          (("1"
            (case "sqv(vp)*wp = (wp * vp)* vp + det(wp, vp) * perpR(vp)")
            (("1" (hide 1)
              (("1"
                (case-replace
                 "(sqv(vp) * det(s, vp) * det(s, wp)) = det(s, vp) * det(s,sqv(vp)*wp)")
                (("1" (hide -1)
                  (("1" (replaces -1)
                    (("1" (rewrite "det_add_right")
                      (("1" (rewrite "det_scal_right")
                        (("1" (rewrite "det_scal_right")
                          (("1" (replace -2 :dir rl)
                            (("1" (lemma "dot_perpR")
                              (("1"
                                (inst -1 "s" "vp")
                                (("1"
                                  (neg-formula -1)
                                  (("1"
                                    (replaces -1 :dir rl)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (lemma "det_asym")
                                        (("1"
                                          (inst -1 "wp" "vp")
                                          (("1"
                                            (replaces -1)
                                            (("1"
                                              (hide-all-but 1)
                                              (("1" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
                nil))
              nil)
             ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
            nil))
          nil))
        nil)
       ("2" (skeep)
        (("2" (inst -5 "r")
          (("2" (flatten)
            (("2" (rewrite "sq_eq_0")
              (("2" (rewrite "sqv_eq_0") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (skeep)
        (("3" (skeep)
          (("3" (inst -5 "r")
            (("3" (flatten)
              (("3" (rewrite "sq_eq_0")
                (("3" (rewrite "sqv_eq_0") (("3" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (derivable_rv? const-decl "bool" deriv_real_vect2 "vect_analysis/")
    (deriv_rv const-decl "Vect2" deriv_real_vect2 "vect_analysis/")
    (/= const-decl "boolean" notequal nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "real" vectors_2D "vectors/")
    (det const-decl "real" det_2D "vectors/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (CBD_66 skolem-const-decl "nnreal" horizontal_sq_dtca nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (det_add_right formula-decl nil det_2D "vectors/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (dot_perpR formula-decl nil det_2D "vectors/")
    (neg_neg formula-decl nil extra_tegies nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (det_asym formula-decl nil det_2D "vectors/")
    (det_scal_right formula-decl nil det_2D "vectors/")
    (perpR const-decl "Vect2" perpendicular_2D "vectors/")
    (+ const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (div_cancel4 formula-decl nil real_props nil)
    (times_div2 formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel3 formula-decl nil real_props nil))
   nil))
(horizontal_sq_dtca_deriv_sign_TCC1 0
  (horizontal_sq_dtca_deriv_sign_TCC1-2 nil 3465664789
   ("" (skeep)
    (("" (lemma "horizontal_sq_dtca_diff")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((horizontal_sq_dtca_diff formula-decl nil horizontal_sq_dtca nil)
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (D formal-const-decl "posreal" horizontal_sq_dtca nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (> const-decl "bool" reals nil)
    (derivable_rv? const-decl "bool" deriv_real_vect2 "vect_analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
  (horizontal_sq_dtca_deriv_sign_TCC1-1 nil 3460214205
   ("" (skeep) (("" (postpone) nil nil)) nil) nil nil))
(horizontal_sq_dtca_deriv_sign 0
  (horizontal_sq_dtca_deriv_sign-1 nil 3460214205
   ("" (skeep)
    (("" (lemma "horizontal_sq_dtca_deriv")
      (("" (inst?)
        (("" (split -1)
          (("1" (replaces -1)
            (("1" (lemma "horizontal_sq_dtca_deriv_simpl")
              (("1" (inst?)
                (("1" (inst -1 "ss")
                  (("1" (split -1)
                    (("1" (assert)
                      (("1" (replaces -1)
                        (("1" (skeep -2)
                          (("1" (lemma "line_solution_eps")
                            (("1" (inst?)
                              (("1"
                                (assert)
                                (("1"
                                  (replaces -1 :dir rl)
                                  (("1"
                                    (lemma "parallel_nzv_Qs")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "dir_parallel?")
                                          (("1"
                                            (skeep -1)
                                            (("1"
                                              (replaces -1)
                                              (("1"
                                                (rewrite
                                                 "det_scal_left")
                                                (("1"
                                                  (rewrite
                                                   "dot_scal_right")
                                                  (("1"
                                                    (rewrite
                                                     "det_scal_right")
                                                    (("1"
                                                      (lemma
                                                       "s_dot_Qs_lt_0")
                                                      (("1"
                                                        (inst?)
                                                        (("1"
                                                          (lemma
                                                           "det_s_Qs_lt_0")
                                                          (("1"
                                                            (inst?)
                                                            (("1"
                                                              (name-replace
                                                               "ww"
                                                               "deriv_rv(V)(r1)")
                                                              (("1"
                                                                (lemma
                                                                 "det_asym")
                                                                (("1"
                                                                  (inst
                                                                   -1
                                                                   "Qs(ss,eps)"
                                                                   "ww")
                                                                  (("1"
                                                                    (replaces
                                                                     -1)
                                                                    (("1"
                                                                      (lemma
                                                                       "det_perpR")
                                                                      (("1"
                                                                        (inst
                                                                         -1
                                                                         "ww"
                                                                         "Qs(ss,eps)")
                                                                        (("1"
                                                                          (replaces
                                                                           -1)
                                                                          (("1"
                                                                            (lemma
                                                                             "dot_comm")
                                                                            (("1"
                                                                              (inst
                                                                               -1
                                                                               "ww"
                                                                               "perpR(Qs(ss,eps))")
                                                                              (("1"
                                                                                (replaces
                                                                                 -1)
                                                                                (("1"
                                                                                  (lemma
                                                                                   "Q_eq_Qs_perp")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -1
                                                                                     "eps"
                                                                                     "ss")
                                                                                    (("1"
                                                                                      (replaces
                                                                                       -1)
                                                                                      (("1"
                                                                                        (case
                                                                                         "(D / sqrt(sqv(ss) - sq(D))) > 0")
                                                                                        (("1"
                                                                                          (name-replace
                                                                                           "dd"
                                                                                           "(D / sqrt(sqv(ss) - sq(D)))")
                                                                                          (("1"
                                                                                            (name-replace
                                                                                             "bb"
                                                                                             "det(ss, Qs(ss, eps))")
                                                                                            (("1"
                                                                                              (case-replace
                                                                                               "-eps * dd * perpR(Qs(ss, eps)) * ww = dd*(-eps*(perpR(Qs(ss, eps)) * ww))")
                                                                                              (("1"
                                                                                                (hide
                                                                                                 -1)
                                                                                                (("1"
                                                                                                  (name-replace
                                                                                                   "aa"
                                                                                                   "(perpR(Qs(ss, eps)) * ww)")
                                                                                                  (("1"
                                                                                                    (name-replace
                                                                                                     "cc"
                                                                                                     "ss * Qs(ss, eps)")
                                                                                                    (("1"
                                                                                                      (hide
                                                                                                       -4
                                                                                                       -5)
                                                                                                      (("1"
                                                                                                        (case-replace
                                                                                                         "(2 * (pk * cc * (pk * -aa) * (pk * bb)) / sq(sqv(pk * Qs(ss, eps)))) = ((2*pk*pk*pk)/sq(sqv(pk * Qs(ss, eps))))*(cc*-aa*bb)")
                                                                                                        (("1"
                                                                                                          (hide
                                                                                                           -1)
                                                                                                          (("1"
                                                                                                            (case-replace
                                                                                                             "((2 * pk * pk * pk) / sq(sqv(pk * Qs(ss, eps)))) > 0")
                                                                                                            (("1"
                                                                                                              (name-replace
                                                                                                               "ee"
                                                                                                               " ((2 * pk * pk * pk) / sq(sqv(pk * Qs(ss, eps))))")
                                                                                                              (("1"
                                                                                                                (grind)
                                                                                                                (("1"
                                                                                                                  (grind-reals)
                                                                                                                  (("1"
                                                                                                                    (neg-formula
                                                                                                                     1)
                                                                                                                    (("1"
                                                                                                                      (neg-formula
                                                                                                                       -6)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (neg-formula
                                                                                                                     1)
                                                                                                                    (("2"
                                                                                                                      (neg-formula
                                                                                                                       -6)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (grind-reals)
                                                                                                                  (("1"
                                                                                                                    (neg-formula
                                                                                                                     1)
                                                                                                                    (("1"
                                                                                                                      (neg-formula
                                                                                                                       -6)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (neg-formula
                                                                                                                     1)
                                                                                                                    (("2"
                                                                                                                      (neg-formula
                                                                                                                       -6)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (hide
                                                                                                               2)
                                                                                                              (("2"
                                                                                                                (cross-mult
                                                                                                                 1)
                                                                                                                (("2"
                                                                                                                  (grind-reals)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil)
                                                                                                         ("2"
                                                                                                          (hide
                                                                                                           2)
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (hide
                                                                                                 2)
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (hide
                                                                                           2)
                                                                                          (("2"
                                                                                            (grind-reals)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (inst -1 "r1") nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (inst -1 "r1") nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((horizontal_sq_dtca_deriv formula-decl nil horizontal_sq_dtca nil)
    (horizontal_sq_dtca_deriv_simpl formula-decl nil horizontal_sq_dtca
     nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (V skolem-const-decl
     "(LAMBDA (V: [real -> Vect2]): derivable_rv?(V))"
     horizontal_sq_dtca nil)
    (r1 skolem-const-decl "real" horizontal_sq_dtca nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (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)
    (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/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (dir_parallel? const-decl "bool" vectors_2D "vectors/")
    (dot_scal_right formula-decl nil vectors_2D "vectors/")
    (s_dot_Qs_lt_0 formula-decl nil tangent_line nil)
    (det_s_Qs_lt_0 formula-decl nil tangent_line nil)
    (det_perpR formula-decl nil det_2D "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (perpR const-decl "Vect2" perpendicular_2D "vectors/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (Q_eq_Qs_perp formula-decl nil tangent_line nil)
    (pos_div_gt formula-decl nil real_props nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (sign_neg_clos application-judgement "Sign" sign "reals/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
    (neg_times_lt formula-decl nil real_props nil)
    (neg_gt formula-decl nil real_props nil)
    (neg_times_gt formula-decl nil real_props nil)
    (pos_times_gt formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (dot_scal_left formula-decl nil vectors_2D "vectors/")
    (perpR_nz application-judgement "Nz_vect2" perpendicular_2D
     "vectors/")
    (det const-decl "real" det_2D "vectors/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (dot_comm formula-decl nil vectors_2D "vectors/")
    (det_asym formula-decl nil det_2D "vectors/")
    (det_scal_right formula-decl nil det_2D "vectors/")
    (Qs_nzv application-judgement "Nz_vect2" horizontal_sq_dtca nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (det_scal_left formula-decl nil det_2D "vectors/")
    (Qs const-decl "Vect2" tangent_line nil)
    (deriv_rv const-decl "Vect2" deriv_real_vect2 "vect_analysis/")
    (parallel_nzv_Qs formula-decl nil tangent_line nil)
    (line_solution_eps formula-decl nil line_solutions nil)
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (D formal-const-decl "posreal" horizontal_sq_dtca nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (> const-decl "bool" reals nil)
    (derivable_rv? const-decl "bool" deriv_real_vect2 "vect_analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)))

¤ Dauer der Verarbeitung: 0.28 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht 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.