products/sources/formale Sprachen/PVS/ACCoRD/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: opaqueproof.mli   Sprache: Lisp

Original von: PVS©
(track
 (trkgs2vect_TCC1 0
  (trkgs2vect_TCC1-1 nil 3460311979
   ("" (skeep)
    (("" (use "scal_eq_zero")
      (("" (assert)
        (("" (hide -2)
          (("" (lemma "sqv_eq_0")
            (("" (inst?)
              (("" (assert)
                (("" (hide -2)
                  (("" (rewrite "sqv_sos")
                    (("" (expand "sos")
                      (("" (use "sin2_cos2") (("" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((scal_eq_zero formula-decl nil vectors_2D "vectors/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (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)
    (sos const-decl "nnreal" vectors_2D "vectors/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
    (sqv_sos formula-decl nil vectors_2D "vectors/")
    (sqv_eq_0 formula-decl nil vectors_2D "vectors/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/"))
   nil))
 (track_TCC1 0
  (track_TCC1-1 nil 3460312047
   ("" (skeep)
    (("" (typepred "v")
      (("" (flatten) (("" (decompose-equality 1) nil nil)) nil)) nil))
    nil)
   ((Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (comp_zero_x formula-decl nil vectors_2D "vectors/")
    (comp_zero_y formula-decl nil vectors_2D "vectors/"))
   nil))
 (sin_track 0
  (sin_track-1 nil 3460330771
   ("" (skeep)
    (("" (expand "track")
      (("" (rewrite "sin_atan2")
        (("1" (lift-if)
          (("1" (ground)
            (("1" (field 1)
              (("1" (both-sides-f 1 "sq")
                (("1" (rewrite "sq_norm")
                  (("1" (rewrite "sqv_sos")
                    (("1" (expand "sos")
                      (("1" (replaces -2) (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (rewrite "sq_eq") nil nil))
                nil))
              nil)
             ("2" (field 2)
              (("2" (neg-formula 2)
                (("2" (both-sides-f 2 "sq")
                  (("1" (rewrite "sq_norm")
                    (("1" (rewrite "sq_neg")
                      (("1" (rewrite "sqv_sos")
                        (("1" (expand "sos")
                          (("1" (replaces -1) (("1" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "sq_eq") nil nil))
                  nil))
                nil))
              nil)
             ("3" (field)
              (("3" (cancel-by 1 "v`x")
                (("3" (both-sides-f 2 "sq")
                  (("1" (rewrite "sq_norm")
                    (("1" (rewrite "sq_times")
                      (("1" (rewrite "sq_div")
                        (("1" (real-props)
                          (("1" (rewrite "sqv_sos")
                            (("1" (expand "sos")
                              (("1" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "sq_eq")
                    (("2" (mult-cases 1) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("4" (field 2)
              (("4" (cancel-by 2 "v`x")
                (("4" (neg-formula 3)
                  (("4" (both-sides-f 3 "sq")
                    (("1" (rewrite "sq_norm")
                      (("1" (rewrite "sq_neg")
                        (("1" (rewrite "sq_times")
                          (("1" (rewrite "sq_div")
                            (("1" (real-props)
                              (("1"
                                (rewrite "sqv_sos")
                                (("1"
                                  (expand "sos")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (rewrite "sq_eq")
                      (("2" (neg-formula 1 :auto-step (grind-reals))
                        nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (typepred "v")
            (("2" (flatten) (("2" (decompose-equality 1) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((track const-decl "nnreal_lt_2pi" track nil)
    (comp_zero_y formula-decl nil vectors_2D "vectors/")
    (comp_zero_x formula-decl nil vectors_2D "vectors/")
    (FDX_75 skolem-const-decl "posreal" track nil)
    (FDX_74 skolem-const-decl "real" track nil)
    (FDX_73 skolem-const-decl
     "{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (neg_times_ge formula-decl nil real_props nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (both_sides_times_neg_ge1 formula-decl nil real_props nil)
    (CBD_76 skolem-const-decl "real" track nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (nonzero_times3 formula-decl nil real_props nil)
    (FDX_71 skolem-const-decl "posreal" track nil)
    (FDX_70 skolem-const-decl "real" track nil)
    (FDX_69 skolem-const-decl
     "{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
    (v skolem-const-decl "Nz_vect2" track nil)
    (sq_times formula-decl nil sq "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (div_cancel1 formula-decl nil real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sq_div formula-decl nil sq "reals/")
    (pos_times_ge formula-decl nil real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (CBD_72 skolem-const-decl "real" track nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (sq_neg formula-decl nil sq "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (neg_one_times formula-decl nil extra_tegies nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (mult_neg formula-decl nil extra_tegies nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (div_cancel2 formula-decl nil real_props nil)
    (bijective? const-decl "bool" functions nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (TRUE const-decl "bool" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_eq formula-decl nil sq "reals/")
    (sq_norm formula-decl nil vectors_2D "vectors/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (sos const-decl "nnreal" vectors_2D "vectors/")
    (sq_0 formula-decl nil sq "reals/")
    (sqv_sos formula-decl nil vectors_2D "vectors/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "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)
    (sin_atan2 formula-decl nil atan2 "trig_fnd/"))
   nil))
 (cos_track 0
  (cos_track-2 nil 3602107493
   ("" (skeep)
    (("" (expand "track")
      (("" (rewrite "cos_atan2")
        (("1" (lift-if)
          (("1" (split)
            (("1" (flatten) (("1" (assert) nil nil)) nil)
             ("2" (flatten)
              (("2" (split 2)
                (("1" (flatten)
                  (("1" (field 1)
                    (("1" (both-sides-f 1 "sq")
                      (("1" (rewrite "sq_norm")
                        (("1" (rewrite "sq_times")
                          (("1" (rewrite "sq_div")
                            (("1" (real-props)
                              (("1"
                                (rewrite "sqv_sos")
                                (("1"
                                  (expand "sos")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (rewrite "sq_eq")
                        (("2" (mult-cases 1) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (field 2)
                    (("2" (neg-formula 2)
                      (("2" (both-sides-f 2 "sq")
                        (("1" (rewrite "sq_norm")
                          (("1" (rewrite "sq_neg")
                            (("1" (rewrite "sq_times")
                              (("1"
                                (rewrite "sq_div")
                                (("1"
                                  (real-props)
                                  (("1"
                                    (rewrite "sqv_sos")
                                    (("1"
                                      (expand "sos")
                                      (("1" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "sq_eq")
                          (("2"
                            (neg-formula 1 :auto-step (grind-reals))
                            nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (typepred "v")
            (("2" (flatten) (("2" (decompose-equality 1) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((track const-decl "nnreal_lt_2pi" track nil)
    (comp_zero_y formula-decl nil vectors_2D "vectors/")
    (comp_zero_x formula-decl nil vectors_2D "vectors/")
    (mult_neg formula-decl nil extra_tegies nil)
    (neg_neg formula-decl nil extra_tegies nil)
    (neg_one_times formula-decl nil extra_tegies nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (neg_times_ge formula-decl nil real_props nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (both_sides_times_neg_ge1 formula-decl nil real_props nil)
    (sq_neg formula-decl nil sq "reals/")
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (FDX_79 skolem-const-decl
     "{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
    (FDX_80 skolem-const-decl "posreal" track nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_times formula-decl nil sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (div_cancel1 formula-decl nil real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sos const-decl "nnreal" vectors_2D "vectors/")
    (sqv_sos formula-decl nil vectors_2D "vectors/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_div formula-decl nil sq "reals/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (sq_norm formula-decl nil vectors_2D "vectors/")
    (pos_times_ge formula-decl nil real_props nil)
    (sq_eq formula-decl nil sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (v skolem-const-decl "Nz_vect2" track nil)
    (FDX_77 skolem-const-decl
     "{nnz: nnreal | nnz * nnz = 1 + sq(v`x / v`y)}" track nil)
    (FDX_78 skolem-const-decl "posreal" track nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nonzero_times3 formula-decl nil real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (sq const-decl "nonneg_real" sq "reals/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posreal_plus_nnreal_is_posreal application-judgement "posreal"
     real_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "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)
    (cos_atan2 formula-decl nil atan2 "trig_fnd/"))
   nil)
  (cos_track-1 nil 3460312258
   ("" (skeep)
    (("" (expand "track")
      (("" (rewrite "cos_atan2")
        (("1" (lift-if)
          (("1" (split)
            (("1" (flatten) (("1" (assert) nil nil)) nil)
             ("2" (flatten)
              (("2" (split 2)
                (("1" (flatten)
                  (("1" (field 1)
                    (("1" (both-sides-f 1 "sq")
                      (("1" (rewrite "sq_norm")
                        (("1" (rewrite "sq_times")
                          (("1" (rewrite "sq_div")
                            (("1" (real-props)
                              (("1" (rewrite "sqv_sq") nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (rewrite "sq_eq")
                        (("2" (mult-cases 1) nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (field 2)
                    (("2" (neg-formula 2)
                      (("2" (both-sides-f 2 "sq")
                        (("1" (rewrite "sq_norm")
                          (("1" (rewrite "sq_neg")
                            (("1" (rewrite "sq_times")
                              (("1"
                                (rewrite "sq_div")
                                (("1"
                                  (real-props)
                                  (("1" (rewrite "sqv_sq") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "sq_eq")
                          (("2"
                            (neg-formula 1 :auto-step (grind-reals))
                            nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (typepred "v")
            (("2" (flatten) (("2" (decompose-equality 1) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((comp_zero_y formula-decl nil vectors_2D "vectors/")
    (comp_zero_x formula-decl nil vectors_2D "vectors/")
    (sq_neg formula-decl nil sq "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_times formula-decl nil sq "reals/")
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_div formula-decl nil sq "reals/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (sq_norm formula-decl nil vectors_2D "vectors/")
    (sq_eq formula-decl nil sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (cos_atan2 formula-decl nil atan2 "trig_fnd/"))
   nil))
 (norm_id 0
  (norm_id-2 nil 3602107517
   ("" (skeep)
    (("" (expand "trkgs2vect")
      (("" (expand "norm")
        (("" (rewrite "sqv_scal")
          (("" (sq-simp)
            (("" (rewrite "sqv_sos")
              (("" (expand "sos")
                (("" (lemma "sin2_cos2")
                  (("" (inst?)
                    (("" (replaces -1) (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((trkgs2vect const-decl "Nz_vect2" track nil)
    (sqv_scal formula-decl nil vectors_2D "vectors/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqv_sos formula-decl nil vectors_2D "vectors/")
    (sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_1 formula-decl nil sqrt "reals/")
    (sos const-decl "nnreal" vectors_2D "vectors/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/"))
   nil)
  (norm_id-1 nil 3464478912
   ("" (skeep)
    (("" (expand "trkgs2vect")
      (("" (expand "norm")
        (("" (rewrite "sqv_scal")
          (("" (rewrite "sqv_sq")
            (("" (lemma "sin2_cos2")
              (("" (inst?)
                (("" (replaces -1) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sqv_scal formula-decl nil vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (cos const-decl "real" sincos_def "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_sq formula-decl nil sqrt "reals/")
    (norm const-decl "nnreal" vectors_2D "vectors/"))
   shostak))
 (track_id 0
  (track_id-1 nil 3460311988
   ("" (skeep)
    (("" (expand "trkgs2vect")
      (("" (expand "track")
        (("" (expand "*")
          (("" (lemma "atan2_cancel_pos")
            (("" (inst -1 "gsp" "cos(trk)" "sin(trk)")
              (("" (split -1)
                (("1" (replaces -1)
                  (("1" (lemma "atan2_cos_sin")
                    (("1" (inst -1 "to2pi(trk)")
                      (("1" (rewrite "cos_id_to2pi")
                        (("1" (rewrite "sin_id_to2pi") nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (flatten)
                    (("2" (lemma "sin2_cos2")
                      (("2" (inst? -1)
                        (("2" (replaces (-2 -3))
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((trkgs2vect const-decl "Nz_vect2" track nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (cos const-decl "real" sincos_def "trig_fnd/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (sin2_cos2 formula-decl nil trig_basic "trig_fnd/")
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_0 formula-decl nil sq "reals/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
    (pi const-decl "posreal" atan "trig_fnd/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sin_id_to2pi formula-decl nil to2pi "trig_fnd/")
    (cos_id_to2pi formula-decl nil to2pi "trig_fnd/")
    (atan2_cos_sin formula-decl nil atan2 "trig_fnd/")
    (atan2_cancel_pos formula-decl nil atan2 "trig_fnd/")
    (track const-decl "nnreal_lt_2pi" track nil))
   nil))
 (trkgs2vect_id 0
  (trkgs2vect_id-1 nil 3460330284
   ("" (skeep)
    (("" (expand "trkgs2vect")
      (("" (expand "*")
        (("" (rewrite "sin_track")
          (("" (rewrite "cos_track")
            (("" (decompose-equality 1) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((trkgs2vect const-decl "Nz_vect2" track nil)
    (sin_track formula-decl nil track nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos_track formula-decl nil track nil)
    (* const-decl "Vector" vectors_2D "vectors/"))
   shostak))
 (ordered_eps_1_TCC1 0
  (ordered_eps_1_TCC1-1 nil 3461513175 ("" (subtype-tcc) nil nil)
   ((real_div_nzreal_is_real application-judgement "real" reals nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Integral const-decl "real" integral_def "analysis/")
    (atan_value const-decl "real" atan "trig_fnd/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 "trig_fnd/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
    (pi const-decl "posreal" atan "trig_fnd/")
    (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 "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" 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)
    (number nonempty-type-decl nil numbers nil)
    (det const-decl "real" det_2D "vectors/")
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (track const-decl "nnreal_lt_2pi" track nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/"))
   nil))
 (ordered_eps_1 0
  (ordered_eps_1-2 "" 3505030827
   ("" (skeep)
    (("" (skoletin* 1)
      ((""
        (case-replace
         "det(nvo,s) = norm(nvo)*norm(s)*sin(track(nvo)-track(s))")
        (("1" (hide -1)
          (("1"
            (case-replace
             "norm(nvo) * norm(s) * sin(track(nvo) - track(s)) > det(vi, s) IFF
                         sin(track(nvo) - track(s)) > det(vi, s) / (norm(nvo)*norm(s))")
            (("1" (hide -1)
              (("1" (both-sides-f -3 "sin")
                (("1" (rewrite "sin_asin")
                  (("1" (replaces -1 :dir rl)
                    (("1" (lemma "sin_gt_to2pi")
                      (("1" (inst -1 "track(nvo)-track(s)" "psi")
                        (("1" (assert)
                          (("1" (replaces -1)
                            (("1"
                              (case-replace
                               "psi < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
                                      to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 < pi - psi IFF 0 < to2pi(track(nvo) - track(s) - psi) AND
                                      to2pi(track(nvo) - track(s) - psi) < pi - 2*psi")
                              (("1"
                                (hide -1)
                                (("1"
                                  (replaces (-1 -2 -3))
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (case
                                   "to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi < 0")
                                  (("1"
                                    (case
                                     "psi < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2")
                                    (("1"
                                      (hide 1)
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (case
                                       "to2pi(track(nvo) - track(s) - psi) < pi - 2 * psi")
                                      (("1"
                                        (hide 1 2)
                                        (("1"
                                          (lemma "to2pi_neg")
                                          (("1"
                                            (inst
                                             -1
                                             "to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (lemma "to2pi_to2pi")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "track(nvo) + pi / 2 - track(s)"
                                                   "-pi/2 - psi")
                                                  (("1"
                                                    (replaces -1)
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (case-replace
                                     "psi < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
                                                         to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 < pi - psi IFF 0 < to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi AND  to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi < pi - 2*psi")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (lemma "to2pi_id")
                                        (("1"
                                          (inst
                                           -1
                                           "to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
                                          (("1"
                                            (lemma "to2pi_to2pi")
                                            (("1"
                                              (inst
                                               -1
                                               "track(nvo) + pi / 2 - track(s)"
                                               "-pi/2 - psi")
                                              (("1"
                                                (replaces -1)
                                                (("1"
                                                  (ground)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 3)
                                            (("2" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but 1)
                                      (("2" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (hide-all-but 1)
                (("2" (grind-reals)
                  (("1" (mult-by 1 "(norm(nvo) * norm(s))")
                    (("1" (assert) nil nil)) nil)
                   ("2" (mult-by -1 "(norm(nvo) * norm(s))")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide-all-but 1)
          (("2" (lemma "trkgs2vect_id")
            (("2" (inst-cp -1 "nvo")
              (("2" (inst -1 "s")
                (("2" (expand "trkgs2vect")
                  (("2" (rewrite "sin_minus")
                    (("2" (name-replace "ts" "track(s)")
                      (("2" (name-replace "tnvo" "track(nvo)")
                        (("2" (expand "det")
                          (("2" (name-replace "nnvo" "norm(nvo)")
                            (("2" (name-replace "ns" "norm(s)")
                              (("2"
                                (replaces (-1 -2) :dir rl)
                                (("2"
                                  (expand "*")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan "trig_fnd/")
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (track const-decl "nnreal_lt_2pi" track nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (det const-decl "real" det_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/")
    (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/")
    (asin const-decl "real_abs_le_pi2" asin "trig_fnd/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (trkgs2vect const-decl "Nz_vect2" track nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_minus formula-decl nil trig_basic "trig_fnd/")
    (trkgs2vect_id formula-decl nil track nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel2 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (trig_range type-eq-decl nil sincos_def "trig_fnd/")
    (sin_asin formula-decl nil sincos_def "trig_fnd/")
    (sin_gt_to2pi formula-decl nil to2pi "trig_fnd/")
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (to2pi_neg formula-decl nil to2pi "trig_fnd/")
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (to2pi_to2pi formula-decl nil to2pi "trig_fnd/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nvo skolem-const-decl "Nz_vect2" track nil)
    (s skolem-const-decl "Nz_vect2" track nil)
    (psi skolem-const-decl "real_abs_le_pi2" track nil)
    (to2pi_id formula-decl nil to2pi "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   shostak))
 (ordered_det_ge 0
  (ordered_det_ge-1 nil 3461513312
   ("" (skeep)
    (("" (skoletin* 1)
      ((""
        (case-replace
         "det(nvo,s) = norm(nvo)*norm(s)*sin(track(nvo)-track(s))")
        (("1" (hide -1)
          (("1"
            (case-replace
             "norm(nvo) * norm(s) * sin(track(nvo) - track(s)) >= det(vi, s) IFF
                         sin(track(nvo) - track(s)) >= det(vi, s) / (norm(nvo)*norm(s))")
            (("1" (hide -1)
              (("1" (both-sides-f -3 "sin")
                (("1" (rewrite "sin_asin")
                  (("1" (replaces -1 :dir rl)
                    (("1" (lemma "sin_ge_to2pi")
                      (("1" (inst -1 "track(nvo)-track(s)" "psi")
                        (("1" (assert)
                          (("1" (replaces -1)
                            (("1"
                              (case-replace
                               "psi <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
                                      to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 <= pi - psi IFF 0 <= to2pi(track(nvo) - track(s) - psi) AND
                                      to2pi(track(nvo) - track(s) - psi) <= pi - 2*psi")
                              (("1"
                                (hide -1)
                                (("1"
                                  (replaces (-1 -2 -3))
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (case
                                   "to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi < 0")
                                  (("1"
                                    (case
                                     "psi <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2")
                                    (("1"
                                      (hide 1)
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (case
                                       "to2pi(track(nvo) - track(s) - psi) <= pi - 2 * psi")
                                      (("1"
                                        (hide 1 2)
                                        (("1"
                                          (lemma "to2pi_neg")
                                          (("1"
                                            (inst
                                             -1
                                             "to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (lemma "to2pi_to2pi")
                                                (("1"
                                                  (inst
                                                   -1
                                                   "track(nvo) + pi / 2 - track(s)"
                                                   "-pi/2 - psi")
                                                  (("1"
                                                    (replaces -1)
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (case-replace
                                     "psi <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 AND
                                                         to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 <= pi - psi IFF 0 <= to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi AND  to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi <= pi - 2*psi")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (lemma "to2pi_id")
                                        (("1"
                                          (inst
                                           -1
                                           "to2pi(track(nvo) + pi / 2 - track(s)) - pi / 2 - psi")
                                          (("1"
                                            (lemma "to2pi_to2pi")
                                            (("1"
                                              (inst
                                               -1
                                               "track(nvo) + pi / 2 - track(s)"
                                               "-pi/2 - psi")
                                              (("1"
                                                (replaces -1)
                                                (("1"
                                                  (ground)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 3)
                                            (("2" (ground) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide-all-but 1)
                                      (("2" (ground) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1) (("2" (grind-reals) nil nil)) nil))
            nil))
          nil)
         ("2" (hide-all-but 1)
          (("2" (lemma "trkgs2vect_id")
            (("2" (inst-cp -1 "nvo")
              (("2" (inst -1 "s")
                (("2" (expand "trkgs2vect")
                  (("2" (rewrite "sin_minus")
                    (("2" (name-replace "ts" "track(s)")
                      (("2" (name-replace "tnvo" "track(nvo)")
                        (("2" (expand "det")
                          (("2" (name-replace "nnvo" "norm(nvo)")
                            (("2" (name-replace "ns" "norm(s)")
                              (("2"
                                (replaces (-1 -2) :dir rl)
                                (("2"
                                  (expand "*")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan "trig_fnd/")
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 "trig_fnd/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (track const-decl "nnreal_lt_2pi" track nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (det const-decl "real" det_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/")
    (to2pi const-decl "nnreal_lt_2pi" to2pi "trig_fnd/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/")
    (asin const-decl "real_abs_le_pi2" asin "trig_fnd/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (trkgs2vect const-decl "Nz_vect2" track nil)
    (* const-decl "Vector" vectors_2D "vectors/")
    (cos_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin_minus formula-decl nil trig_basic "trig_fnd/")
    (trkgs2vect_id formula-decl nil track nil)
    (div_mult_pos_ge2 formula-decl nil real_props nil)
    (trig_range type-eq-decl nil sincos_def "trig_fnd/")
    (sin_asin formula-decl nil sincos_def "trig_fnd/")
    (sin_ge_to2pi formula-decl nil to2pi "trig_fnd/")
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (to2pi_neg formula-decl nil to2pi "trig_fnd/")
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (to2pi_to2pi formula-decl nil to2pi "trig_fnd/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nvo skolem-const-decl "Nz_vect2" track nil)
    (s skolem-const-decl "Nz_vect2" track nil)
    (psi skolem-const-decl "real_abs_le_pi2" track nil)
    (to2pi_id formula-decl nil to2pi "trig_fnd/")
    (sin_range application-judgement "trig_range" sincos_def
     "trig_fnd/")
    (sin const-decl "real" sincos_def "trig_fnd/")
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
 (ordered_eps_neg_1 0
  (ordered_eps_neg_1-1 nil 3460980839
   ("" (skeep)
    (("" (lemma "ordered_det_ge")
      (("" (inst -1 "nvo" "s" "vi")
        (("" (ground) (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((ordered_det_ge formula-decl nil track nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx "trig_fnd/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   nil))
 (ordered_eps_1_dot_gt_0 0
  (ordered_eps_1_dot_gt_0-1 nil 3461500351
   ("" (skeep)
    (("" (skoletin* 1)
      ((""
        (case-replace
         "nvo*s = norm(nvo)*norm(s)*cos(track(nvo)-track(s))")
        (("1" (hide -1)
          (("1"
            (case-replace
             "norm(nvo) * norm(s) * cos(track(nvo) - track(s)) > 0 IFF cos(track(nvo) - track(s)) > 0")
            (("1" (hide -1)
              (("1" (lemma "cos_pos_to2pi")
                (("1" (inst?)
                  (("1" (replaces -1)
                    (("1"
                      (case-replace
                       "-pi / 2 < to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 AND
                                       to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 < pi / 2 IFF -pi / 2 - psi < to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi AND
                                       to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi < pi/2 - psi")
                      (("1" (hide -1)
                        (("1"
                          (case "to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi >= 0")
                          (("1" (lemma "to2pi_id")
                            (("1"
                              (inst -1
                               "to2pi(track(nvo) - track(s) + pi / 2) - pi / 2 - psi")
                              (("1"
                                (replaces -1 :dir rl)
                                (("1"
                                  (lemma "to2pi_to2pi")
                                  (("1"
                                    (inst
                                     -1
                                     "track(nvo) - track(s) + pi / 2"
                                     "-pi/2 - psi")
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (real-props)
                                          (("1"
                                            (lemma "ordered_eps_1")
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (replaces -5 :dir rl)
                                                  (("1"
                                                    (replaces -1)
                                                    (("1"
                                                      (replaces -3)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (replaces
                                                           -3
                                                           :dir
                                                           rl)
                                                          (("1"
                                                            (name-replace
                                                             "xx"
                                                             "to2pi(track(nvo) - phi - psi)")
                                                            (("1"
                                                              (hide -3)
                                                              (("1"
--> --------------------

--> maximum size reached

--> --------------------

¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.152Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff