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:   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

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

¤ Dauer der Verarbeitung: 0.47 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
sprechenden Kalenders

Eigene Datei ansehen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff