(vect_trig_2D
 (sin_range 0
  (sin_range-3 nil 3403544907
   ("" (skeep)
    (("" (expand "sin")
      (("" (split)
        (("1" (lemma "det_norm")
          (("1" (inst -1 "v" "u")
            (("1" (rewrite "det_asym")
              (("1" (cross-mult 1) (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (lemma "det_norm")
          (("2" (inst?)
            (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin const-decl "real" vect_trig_2D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (det_norm formula-decl nil det_2D nil)
    (det_asym formula-decl nil det_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types 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)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (det const-decl "real" det_2D nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (real nonempty-type-from-decl nil reals nil))
   nil)
  (sin_range-2 nil 3403542975
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "sin")
        (("1" (cross-mult 1)
          (("1" (case-replace "outer_prod(u!1,v!1) >= 0")
            (("1" (assert) nil nil)
             ("2" (mult-by 2 "-1" - -)
              (("2" (assert)
                (("2" (lemma "sq_le")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (hide 3)
                        (("2" (rewrite "sq_times")
                          (("2" (rewrite "sq_times")
                            (("2" (rewrite "sq_norm")
                              (("2"
                                (rewrite "sq_norm")
                                (("2"
                                  (expand "outer_prod")
                                  (("2"
                                    (expand "sq")
                                    (("2"
                                      (expand "*")
                                      (("2"
                                        (real-props)
                                        (("2"
                                          (rewrite "sq_rew")
                                          (("2"
                                            (rewrite "sq_rew")
                                            (("2"
                                              (case-replace
                                               "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)")
                                              (("1"
                                                (case-replace
                                                 "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)")
                                                (("1"
                                                  (hide -1 -2)
                                                  (("1"
                                                    (case-replace
                                                     "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)")
                                                    (("1"
                                                      (case-replace
                                                       "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)")
                                                      (("1"
                                                        (hide -)
                                                        (("1"
                                                          (move-terms
                                                           1
                                                           l
                                                           1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (move-terms
                                                               1
                                                               l
                                                               1)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (move-terms
                                                                   1
                                                                   l
                                                                   1)
                                                                  (("1"
                                                                    (case-replace
                                                                     "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) -
                                     2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 2 3)
                                                      (("2"
                                                        (ground)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2 3)
                                                  (("2"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide 2 3)
                                                (("2" (grind) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "sin")
        (("2" (cross-mult 1)
          (("2" (case-replace "outer_prod(u!1,v!1) >= 0")
            (("1" (lemma "sq_le")
              (("1" (inst?)
                (("1" (assert)
                  (("1" (hide 2)
                    (("1" (rewrite "sq_times")
                      (("1" (rewrite "sq_times")
                        (("1" (rewrite "sq_norm")
                          (("1" (rewrite "sq_norm")
                            (("1" (expand "outer_prod")
                              (("1"
                                (expand "sq")
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (real-props)
                                    (("1"
                                      (rewrite "sq_rew")
                                      (("1"
                                        (rewrite "sq_rew")
                                        (("1"
                                          (case-replace
                                           "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)")
                                          (("1"
                                            (case-replace
                                             "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)")
                                            (("1"
                                              (hide -1 -2)
                                              (("1"
                                                (case-replace
                                                 "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)")
                                                (("1"
                                                  (case-replace
                                                   "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)")
                                                  (("1"
                                                    (hide -)
                                                    (("1"
                                                      (move-terms
                                                       1
                                                       l
                                                       1)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (move-terms
                                                           1
                                                           l
                                                           1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (move-terms
                                                               1
                                                               l
                                                               1)
                                                              (("1"
                                                                (case-replace
                                                                 "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) -
                                                   2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   2)
                                                                  (("2"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2 3)
                                                  (("2"
                                                    (ground)
                                                    (("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2 3)
                                              (("2" (grind) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 2 3)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Vector type-eq-decl nil vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (sq_le formula-decl nil sq "reals/")
    (sq_times formula-decl nil sq "reals/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_norm formula-decl nil vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (sq_rew formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_1 formula-decl nil sq "reals/"))
   nil)
  (sin_range-1 nil 3403523657
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "sin")
        (("1" (cross-mult 1)
          (("1" (case-replace "cross(u!1,v!1) >= 0")
            (("1" (assert) nil nil)
             ("2" (mult-by 2 "-1" - -)
              (("2" (assert)
                (("2" (lemma "sq_le")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (hide 3)
                        (("2" (rewrite "sq_times")
                          (("2" (rewrite "sq_times")
                            (("2" (rewrite "sq_norm")
                              (("2"
                                (rewrite "sq_norm")
                                (("2"
                                  (expand "cross")
                                  (("2"
                                    (expand "sq")
                                    (("2"
                                      (expand "*")
                                      (("2"
                                        (real-props)
                                        (("2"
                                          (rewrite "sq_rew")
                                          (("2"
                                            (rewrite "sq_rew")
                                            (("2"
                                              (case-replace
                                               "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)")
                                              (("1"
                                                (case-replace
                                                 "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)")
                                                (("1"
                                                  (hide -1 -2)
                                                  (("1"
                                                    (case-replace
                                                     "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)")
                                                    (("1"
                                                      (case-replace
                                                       "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)")
                                                      (("1"
                                                        (hide -)
                                                        (("1"
                                                          (move-terms
                                                           1
                                                           l
                                                           1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (move-terms
                                                               1
                                                               l
                                                               1)
                                                              (("1"
                                                                (assert)
                                                                (("1"
                                                                  (move-terms
                                                                   1
                                                                   l
                                                                   1)
                                                                  (("1"
                                                                    (case-replace
                                                                     "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) -
                       2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)")
                                                                    (("1"
                                                                      (assert)
                                                                      nil
                                                                      nil)
                                                                     ("2"
                                                                      (hide
                                                                       2)
                                                                      (("2"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide 2 3)
                                                      (("2"
                                                        (ground)
                                                        (("2"
                                                          (grind)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2 3)
                                                  (("2"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide 2 3)
                                                (("2" (grind) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "sin")
        (("2" (cross-mult 1)
          (("2" (case-replace "cross(u!1,v!1) >= 0")
            (("1" (lemma "sq_le")
              (("1" (inst?)
                (("1" (assert)
                  (("1" (hide 2)
                    (("1" (rewrite "sq_times")
                      (("1" (rewrite "sq_times")
                        (("1" (rewrite "sq_norm")
                          (("1" (rewrite "sq_norm")
                            (("1" (expand "cross")
                              (("1"
                                (expand "sq")
                                (("1"
                                  (expand "*")
                                  (("1"
                                    (real-props)
                                    (("1"
                                      (rewrite "sq_rew")
                                      (("1"
                                        (rewrite "sq_rew")
                                        (("1"
                                          (case-replace
                                           "sq(u!1`x) * v!1`y * v!1`y = sq(u!1`x) * sq(v!1`y)")
                                          (("1"
                                            (case-replace
                                             "sq(u!1`x) * v!1`x * v!1`x = sq(u!1`x) * sq(v!1`x)")
                                            (("1"
                                              (hide -1 -2)
                                              (("1"
                                                (case-replace
                                                 "sq(u!1`y) * v!1`x * v!1`x = sq(u!1`y) * sq(v!1`x)")
                                                (("1"
                                                  (case-replace
                                                   "sq(u!1`y) * v!1`y * v!1`y = sq(u!1`y) * sq(v!1`y)")
                                                  (("1"
                                                    (hide -)
                                                    (("1"
                                                      (move-terms
                                                       1
                                                       l
                                                       1)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (move-terms
                                                           1
                                                           l
                                                           1)
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (move-terms
                                                               1
                                                               l
                                                               1)
                                                              (("1"
                                                                (case-replace
                                                                 "sq(u!1`x) * sq(v!1`x) + sq(u!1`y) * sq(v!1`y) -
                                     2 * (u!1`y * v!1`x * v!1`y * -u!1`x) = sq(u!1`x*v!1`x + u!1`y*v!1`y)")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   2)
                                                                  (("2"
                                                                    (grind)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide 2)
                                                    (("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2 3)
                                                  (("2"
                                                    (ground)
                                                    (("2"
                                                      (grind)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2 3)
                                              (("2" (grind) nil nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide 2 3)
                                            (("2" (grind) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_1 formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_rew formula-decl nil sq "reals/")
    (* const-decl "real" vectors_2D nil)
    (sq_norm formula-decl nil vectors_2D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (sq_times formula-decl nil sq "reals/")
    (sq_le formula-decl nil sq "reals/")
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (Vector type-eq-decl nil vectors_2D nil))
   nil))
 (cos_range 0
  (cos_range-1 nil 3403523657
   ("" (skeep)
    (("" (expand "cos")
      (("" (lemma "dot_norm")
        (("" (inst?)
          (("" (flatten)
            (("" (prop)
              (("1" (assert)
                (("1" (cross-mult 1) (("1" (assert) nil nil)) nil))
                nil)
               ("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos const-decl "real" vect_trig_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (* const-decl "real" vectors_2D nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (div_mult_pos_le1 formula-decl nil real_props nil)
    (dot_norm formula-decl nil vectors_2D nil))
   nil))
 (sin2_cos2 0
  (sin2_cos2-1 nil 3403523663
   ("" (skeep)
    (("" (expand "sin")
      (("" (expand "cos")
        (("" (rewrite "sq_div")
          (("" (rewrite "sq_div")
            (("" (rewrite "sq_times")
              (("" (rewrite "sq_norm")
                (("" (rewrite "sq_norm")
                  (("" (rewrite "sq_det") (("" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin const-decl "real" vect_trig_2D nil)
    (sq_div formula-decl nil sq "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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 nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_times formula-decl nil sq "reals/")
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_det formula-decl nil det_2D nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (sq_norm formula-decl nil vectors_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (det const-decl "real" det_2D nil)
    (cos const-decl "real" vect_trig_2D nil))
   shostak))
 (sin_asym 0
  (sin_asym-1 nil 3427043758
   ("" (skeep)
    (("" (expand "sin")
      (("" (rewrite "det_asym") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((sin const-decl "real" vect_trig_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (real nonempty-type-from-decl nil reals nil)
    (det_asym formula-decl nil det_2D nil))
   shostak))
 (cos_symm 0
  (cos_symm-1 nil 3427044299
   ("" (skeep)
    (("" (expand "cos")
      (("" (lemma "dot_comm")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((cos const-decl "real" vect_trig_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (boolean nonempty-type-decl nil booleans nil)
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Nz_vector type-eq-decl nil vectors_2D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (dot_comm formula-decl nil vectors_2D nil))
   shostak)))