products/Sources/formale Sprachen/PVS/trig/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: patch-107.lisp   Sprache: Lisp

Original von: PVS©
(law_cosines
 (distance_refl 0
  (distance_refl-1 nil 3269434431
   ("" (grind) (("" (rewrite "sqrt_0") nil nil)) nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (dist const-decl "nonneg_real" law_cosines nil))
   nil))
 (distance_symm 0
  (distance_symm-1 nil 3269434431
   ("" (skolem 1 ("x0" "y0" "x1" "y1"))
    (("" (expand "dist")
      (("" (expand "sq_dist") (("" (grind) nil nil)) nil)) nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil))
   nil))
 (distance_trans 0
  (distance_trans-1 nil 3269668543
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil))
   shostak))
 (distance_scale 0
  (distance_scale-1 nil 3269668008
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (lemma "sq_times")
          (("" (inst-cp - "pz!1" "x0!1-x1!1")
            (("" (inst - "pz!1" "y0!1-y1!1")
              (("" (lemma "sqrt_times")
                ((""
                  (inst - "sq(pz!1)"
                   "sq(x0!1 - x1!1) + sq(y0!1 - y1!1)")
                  (("" (rewrite "sqrt_sq") (("" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nonneg_real" law_cosines nil)
    (sq_times formula-decl nil sq "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_times formula-decl nil sqrt "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (distance_rot 0
  (distance_rot-1 nil 3269668867
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (name "KX" "x0!1 - x1!1")
          (("" (name "KY" "y0!1 - y1!1")
            ((""
              (case "(cos(ac!1) * x0!1 + sin(ac!1) * y1!1 - cos(ac!1) * x1!1 -
                sin(ac!1) * y0!1) = cos(ac!1)*KX - sin(ac!1)*KY")
              (("1" (replace -1)
                (("1"
                  (case "(cos(ac!1) * y0!1 + sin(ac!1) * x0!1 - cos(ac!1) * y1!1 -
                 sin(ac!1) * x1!1) = sin(ac!1)*KX +cos(ac!1)*KY")
                  (("1" (replace -1)
                    (("1" (replace -3)
                      (("1" (replace -4)
                        (("1" (hide-all-but 1)
                          (("1" (lemma "sin2_cos2" ("a" "ac!1"))
                            (("1" (name-replace "SIN" "sin(ac!1)")
                              (("1"
                                (name-replace "COS" "cos(ac!1)")
                                (("1"
                                  (expand "sq")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2 -1)
                    (("2" (expand "KX")
                      (("2" (expand "KY") (("2" (propax) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (expand "KY")
                (("2" (expand "KX") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sin_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (dist const-decl "nonneg_real" law_cosines 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (cos const-decl "real" trig_basic nil)
    (sin const-decl "real" trig_basic nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (trig_range type-eq-decl nil trig_basic nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sin2_cos2 formula-decl nil trig_basic nil)
    (KX skolem-const-decl "real" law_cosines nil)
    (KY skolem-const-decl "real" law_cosines nil)
    (sq_dist const-decl "nonneg_real" law_cosines nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (Law_Cosines 0
  (Law_Cosines-1 nil 3269434431
   ("" (expand "dist")
    (("" (expand "sq_dist")
      (("" (ground)
        (("" (expand "sq")
          (("" (ground) (("" (skosimp*) (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_dist const-decl "nonneg_real" law_cosines nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (dist const-decl "nonneg_real" law_cosines nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (triangle 0
  (triangle-1 nil 3269434431
   (""
    (case "FORALL (x,y:real): dist(0,0,0,1) <= dist(x,y,0,1) + dist(x,y,0,0)")
    (("1"
      (case "FORALL (x,y:real,pz:posreal): dist(0, 0, 0, pz) <= dist(x, y, 0, pz) + dist(x, y, 0, 0)")
      (("1" (hide -2)
        (("1"
          (case "FORALL (x,y,a,b:real): dist(0, 0, a,b) <= dist(x, y, a,b) + dist(x, y, 0, 0)")
          (("1" (hide -2)
            (("1" (skosimp*)
              (("1"
                (lemma "distance_trans" ("x2" "-x0!1" "y2" "-y0!1"))
                (("1" (inst-cp - "x0!1" "x1!1" "y0!1" "y1!1")
                  (("1" (inst-cp - "x2!1" "x1!1" "y2!1" "y1!1")
                    (("1" (inst - "x2!1" "x0!1" "y2!1" "y0!1")
                      (("1"
                        (inst - "x2!1-x0!1" "y2!1-y0!1" "x1!1-x0!1"
                         "y1!1-y0!1")
                        (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (skosimp*)
              (("2" (case "a!1=0")
                (("1" (replace -1)
                  (("1" (lemma "trichotomy" ("x" "b!1"))
                    (("1" (split -1)
                      (("1" (inst - "x!1" "y!1" "b!1")
                        (("1" (assert) nil nil)) nil)
                       ("2" (replace -1)
                        (("2" (expand "dist")
                          (("2" (expand "sq_dist")
                            (("2" (rewrite "sq_0")
                              (("2"
                                (rewrite "sqrt_0")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("3" (inst - "x!1" "-y!1" "-b!1")
                        (("1" (expand "dist")
                          (("1" (expand "sq_dist")
                            (("1" (rewrite "sq_neg")
                              (("1"
                                (lemma "sq_neg" ("a" "y!1-b!1"))
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (assert)
                                    (("1"
                                      (lemma "sq_neg" ("a" "-1*b!1"))
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (name "theta" "atan2(b!1,a!1)")
                  (("1" (lemma "distance_rot" ("ac" "theta"))
                    (("1" (lemma "sin_atan2" ("x" "b!1" "y" "a!1"))
                      (("1" (lemma "cos_atan2" ("x" "b!1" "y" "a!1"))
                        (("1" (assert)
                          (("1" (replace -4)
                            (("1" (inst-cp - "0" "a!1" "0" "b!1")
                              (("1"
                                (simplify -4)
                                (("1"
                                  (case
                                   "cos(theta) * a!1 - sin(theta) * b!1 = 0")
                                  (("1"
                                    (case
                                     "cos(theta) * b!1 + sin(theta) * a!1 = sqrt(sq(a!1)+sq(b!1))")
                                    (("1"
                                      (inst-cp - "x!1" "0" "y!1" "0")
                                      (("1"
                                        (inst
                                         -
                                         "x!1"
                                         "a!1"
                                         "y!1"
                                         "b!1")
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (replace -2)
                                            (("1"
                                              (replace -5)
                                              (("1"
                                                (replace -6)
                                                (("1"
                                                  (replace -7)
                                                  (("1"
                                                    (simplify 2)
                                                    (("1"
                                                      (inst
                                                       -
                                                       "cos(theta) * x!1 - sin(theta) * y!1"
                                                       "cos(theta) * y!1 + sin(theta) * x!1"
                                                       "sqrt(sq(a!1) + sq(b!1))")
                                                      (("1"
                                                        (hide
                                                         -3
                                                         -4
                                                         -5
                                                         -6
                                                         -7
                                                         -8
                                                         3)
                                                        (("1"
                                                          (lemma
                                                           "sqrt_pos"
                                                           ("px"
                                                            "sq(a!1) + sq(b!1)"))
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (hide
                                                             -1
                                                             -2
                                                             2)
                                                            (("2"
                                                              (lemma
                                                               "sq_nz_pos"
                                                               ("nz"
                                                                "a!1"))
                                                              (("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide -1 -4 -5 -6 -7 3)
                                      (("2"
                                        (case "b!1=0")
                                        (("1"
                                          (replace -1)
                                          (("1"
                                            (rewrite "sq_0")
                                            (("1"
                                              (simplify 1)
                                              (("1"
                                                (case "a!1>0")
                                                (("1"
                                                  (rewrite "sqrt_sq")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (lemma
                                                   "sq_neg"
                                                   ("a" "a!1"))
                                                  (("2"
                                                    (replace -1 2 rl)
                                                    (("2"
                                                      (rewrite
                                                       "sqrt_sq")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (case
                                             "1 + sq(a!1 / b!1) = (sq(a!1)+sq(b!1))/sq(b!1)")
                                            (("1"
                                              (replace -1)
                                              (("1"
                                                (rewrite "sqrt_div")
                                                (("1"
                                                  (case "b!1>0")
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (rewrite
                                                       "sqrt_sq")
                                                      (("1"
                                                        (rewrite
                                                         "div_div1")
                                                        (("1"
                                                          (rewrite
                                                           "div_div1")
                                                          (("1"
                                                            (lemma
                                                             "div_cancel2"
                                                             ("x"
                                                              "a!1"
                                                              "n0z"
                                                              "b!1"))
                                                            (("1"
                                                              (replace
                                                               -1
                                                               -5)
                                                              (("1"
                                                                (replace
                                                                 -4)
                                                                (("1"
                                                                  (replace
                                                                   -5)
                                                                  (("1"
                                                                    (lemma
                                                                     "div_cancel3"
                                                                     ("x"
                                                                      "b!1*b!1+a!1*a!1"
                                                                      "n0z"
                                                                      "sqrt(sq(a!1) + sq(b!1))"
                                                                      "y"
                                                                      "sqrt(sq(a!1) + sq(b!1))"))
                                                                    (("1"
                                                                      (replace
                                                                       -1
                                                                       2)
                                                                      (("1"
                                                                        (rewrite
                                                                         "sq_rew"
                                                                         2)
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_rew"
                                                                           2)
                                                                          (("1"
                                                                            (rewrite
                                                                             "sq_rew"
                                                                             2)
                                                                            (("1"
                                                                              (rewrite
                                                                               "sq_sqrt")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (assert)
                                                    (("2"
                                                      (rewrite
                                                       "div_div1")
                                                      (("2"
                                                        (rewrite
                                                         "div_div1")
                                                        (("2"
                                                          (lemma
                                                           "sq_neg"
                                                           ("a" "b!1"))
                                                          (("2"
                                                            (replace
                                                             -1
                                                             *
                                                             rl)
                                                            (("2"
                                                              (rewrite
                                                               "sqrt_sq")
                                                              (("2"
                                                                (case
                                                                 "-((a!1 / b!1 * -b!1) / sqrt((sq(a!1) + sq(-b!1)))) = a!1/ sqrt((sq(a!1) + sq(-b!1)))")
                                                                (("1"
                                                                  (replace
                                                                   -1)
                                                                  (("1"
                                                                    (case
                                                                     "-1*-b!1=b!1")
                                                                    (("1"
                                                                      (replace
                                                                       -1)
                                                                      (("1"
                                                                        (hide
                                                                         -1
                                                                         -2
                                                                         -4)
                                                                        (("1"
                                                                          (replace
                                                                           -2)
                                                                          (("1"
                                                                            (replace
                                                                             -3)
                                                                            (("1"
                                                                              (replace
                                                                               -1)
                                                                              (("1"
                                                                                (hide
                                                                                 (-1
                                                                                  -2
                                                                                  -3))
                                                                                (("1"
                                                                                  (lemma
                                                                                   "div_cancel3")
                                                                                  (("1"
                                                                                    (inst
                                                                                     -
                                                                                     "sqrt(sq(a!1) + sq(b!1))"
                                                                                     "b!1*b!1+a!1*a!1"
                                                                                     "sqrt(sq(a!1) + sq(b!1))")
                                                                                    (("1"
                                                                                      (replace
                                                                                       -1
                                                                                       3)
                                                                                      (("1"
                                                                                        (rewrite
                                                                                         "sq_rew")
                                                                                        (("1"
                                                                                          (rewrite
                                                                                           "sq_rew")
                                                                                          (("1"
                                                                                            (rewrite
                                                                                             "sq_rew")
                                                                                            (("1"
                                                                                              (rewrite
                                                                                               "sq_sqrt")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (assert)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   4
                                                                   -3
                                                                   -4)
                                                                  (("2"
                                                                    (assert)
                                                                    nil
                                                                    nil))
                                                                  nil)
                                                                 ("3"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (lemma
                                                   "sq_nz_pos"
                                                   ("nz" "b!1"))
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (rewrite "sq_div")
                                              (("2" (assert) nil nil))
                                              nil)
                                             ("3"
                                              (lemma
                                               "sq_nz_pos"
                                               ("nz" "b!1"))
                                              (("3" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide -3 -4 -5 -6 3)
                                    (("2"
                                      (case "b!1=0")
                                      (("1" (assert) nil nil)
                                       ("2"
                                        (case "b!1>0")
                                        (("1" (assert) nil nil)
                                         ("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "b!1=0")
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skosimp*)
          (("2" (lemma "distance_scale" ("pz" "pz!1"))
            (("2" (inst-cp - "0" "0" "0" "1")
              (("2" (inst-cp - "x!1/pz!1" "0" "y!1/pz!1" "1")
                (("2" (inst - "x!1/pz!1" "0" "y!1/pz!1" "0")
                  (("2" (inst - "x!1/pz!1" "y!1/pz!1")
                    (("2"
                      (lemma "both_sides_times_pos_le1"
                       ("x" "dist(0, 0, 0, 1)" "y"
                        "dist(x!1/pz!1, y!1/pz!1, 0, 1) + dist(x!1/pz!1, y!1/pz!1, 0, 0)"
                        "pz" "pz!1"))
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (hide 2)
      (("2" (skosimp*)
        (("2" (expand "dist")
          (("2" (expand "sq_dist")
            (("2" (rewrite "sq_neg")
              (("2" (rewrite "sq_0")
                (("2" (rewrite "sq_1")
                  (("2" (rewrite "sqrt_1")
                    (("2" (name-replace "K1" "sq(x!1)")
                      (("2" (rewrite "sq_le" :dir rl)
                        (("2" (rewrite "sq_1")
                          (("2" (rewrite "sq_plus")
                            (("2" (rewrite "sq_sqrt")
                              (("2"
                                (rewrite "sq_sqrt")
                                (("2"
                                  (rewrite "sq_minus")
                                  (("2"
                                    (rewrite "sq_1")
                                    (("2"
                                      (lemma "trichotomy" ("x" "y!1"))
                                      (("2"
                                        (split -1)
                                        (("1"
                                          (case
                                           "sq(y!1) - 2 * y!1 + K1 + (sq(y!1) + K1) >=0")
                                          (("1" (assert) nil nil)
                                           ("2"
                                            (case
                                             "y!1-sq(y!1)-K1 <= (sqrt(1 + sq(y!1) - 2 * y!1 + K1) * sqrt(sq(y!1) + K1))")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (hide 3)
                                              (("2"
                                                (rewrite
                                                 "sqrt_times"
                                                 :dir
                                                 rl)
                                                (("2"
                                                  (rewrite
                                                   "sq_le"
                                                   :dir
                                                   rl)
                                                  (("2"
                                                    (rewrite "sq_sqrt")
                                                    (("2"
                                                      (expand "sq" 1)
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (replace -1)
                                          (("2"
                                            (rewrite "sq_0")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("3" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_1 formula-decl nil sq "reals/")
    (sq_minus formula-decl nil sq "reals/")
    (sqrt_times formula-decl nil sqrt "reals/")
    (sq_plus formula-decl nil sq "reals/")
    (sq_le formula-decl nil sq "reals/")
    (sqrt_1 formula-decl nil sqrt "reals/")
    (cos const-decl "real" trig_basic nil)
    (sin const-decl "real" trig_basic nil)
    (sq_div formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (sqrt_div formula-decl nil sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_pos judgement-tcc nil sqrt "reals/")
    (sq_nz_pos judgement-tcc nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sq_neg formula-decl nil sq "reals/"))
   nil)))


¤ Dauer der Verarbeitung: 0.23 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff