Quelle  closest_approach_relative_2D.prf   Sprache: unbekannt

(closest_approach_relative_2D
 (divergent_lem 0
  (divergent_lem-1 nil 3474796853
   ("" (skosimp*)
    (("" (expand "divergent?")
      (("" (expand "dist")
        (("" (expand "norm")
          (("" (expand "sqv")
            (("" (expand "sq_dist")
              (("" (assert) (("" (grind) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((divergent? const-decl "bool" closest_approach_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (add_zero_left formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (dist const-decl "nnreal" distance_2D nil))
   shostak))
 (dot_pos_comm 0
  (dot_pos_comm-1 nil 3479037640
   ("" (skosimp*)
    (("" (expand "dot_pos?")
      (("" (ground) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
      nil))
    nil)
   ((dot_pos? const-decl "bool" closest_approach_relative_2D nil)
    (* const-decl "real" vectors_2D nil)
    (- const-decl "Vector" vectors_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (dot_pos_divergent 0
  (dot_pos_divergent-2 nil 3479037612
   ("" (skeep)
    (("" (lemma "dot_nneg_divergent")
      (("" (inst?)
        (("" (assert)
          (("" (expand "dot_pos?")
            (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dot_nneg_divergent formula-decl nil closest_approach_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (* const-decl "real" vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (dot_pos? const-decl "bool" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D 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)
  (dot_pos_divergent-1 nil 3479037596 ("" (postpone) nil nil) nil
   shostak))
 (divergent_lt 0
  (divergent_lt-1 nil 3474798522
   ("" (skeep)
    (("" (lemma "divergent_t1_lt_t2")
      (("" (inst?)
        (("" (replaces -1)
          (("" (expand "dist")
            (("" (assert)
              (("" (expand "sq_dist_at")
                (("" (split)
                  (("1" (flatten)
                    (("1" (skeep)
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (rewrite "sqrt_lt") nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (flatten)
                    (("2" (skeep)
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (rewrite "sqrt_lt") nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((divergent_t1_lt_t2 formula-decl nil closest_approach_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (real_lt_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)
    (* const-decl "Vector" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (sqrt_lt formula-decl nil sqrt "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)
    (sq_dist_at const-decl "nnreal" closest_approach_relative_2D nil)
    (dist const-decl "nnreal" distance_2D nil)
    (zero const-decl "Vector" vectors_2D 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))
 (divergent_dot_pos 0
  (divergent_dot_pos-1 nil 3479037588
   ("" (skosimp*)
    (("" (lemma "divergent_dot_nneg")
      (("" (inst - "s!1" "zero" "v!1" "zero")
        (("" (assert)
          (("" (expand "dot_pos?") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((divergent_dot_nneg formula-decl nil closest_approach_2D nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (real_gt_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)
    (dot_pos? const-decl "bool" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D 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))
 (diverg_dot_nneg 0
  (diverg_dot_nneg-1 nil 3474890469
   ("" (skosimp*)
    (("" (expand "dot_nneg?")
      (("" (lemma "divergent_dot_nneg")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((dot_nneg? const-decl "bool" closest_approach_relative_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (divergent_dot_nneg formula-decl nil closest_approach_2D nil))
   nil))
 (divergent_v_neq_0 0
  (divergent_v_neq_0-1 nil 3474797479
   ("" (skosimp*)
    (("" (lemma "divergent_u_neq_v")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((divergent_u_neq_v formula-decl nil closest_approach_2D nil)
    (zero const-decl "Vector" vectors_2D 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))
   shostak))
 (dot_nneg_divergent_nzv 0
  (dot_nneg_divergent_nzv-1 nil 3474797504
   ("" (skosimp*)
    (("" (lemma "dot_nneg_divergent")
      (("" (inst?)
        (("" (assert)
          (("" (expand "dot_nneg?")
            (("" (lemma "divergent_dot_nneg")
              (("" (inst?) (("" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dot_nneg_divergent formula-decl nil closest_approach_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (divergent_dot_nneg formula-decl nil closest_approach_2D nil)
    (dot_nneg? const-decl "bool" closest_approach_relative_2D nil)
    (Nz_vect2 type-eq-decl nil vectors_2D nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (zero const-decl "Vector" vectors_2D 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))
   shostak))
 (tau_TCC1 0
  (tau_TCC1-1 nil 3475859208
   ("" (skosimp*)
    (("" (lemma "sqv_eq_0") (("" (inst?) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((sqv_eq_0 formula-decl nil vectors_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (real nonempty-type-from-decl nil reals nil))
   nil))
 (tau_is_min 0
  (tau_is_min-2 nil 3475859357
   ("" (skosimp*)
    (("" (lemma "time_cpa")
      (("" (skoletin 1)
        (("" (inst - "s!1" "zero" "Tau" "nzv!1" "zero")
          (("" (split -2)
            (("1" (hide -2)
              (("1"
                (case-replace
                 "(LAMBDA t: sq_dist(s!1 + t * nzv!1, zero + t * zero)) =
     (LAMBDA t: sq(norm(s!1 + t * nzv!1)))")
                (("1" (apply-extensionality 1 :hide? t)
                  (("1" (hide -1 2)
                    (("1" (rewrite "dot_sq_norm" :dir rl)
                      (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (expand "tau_2D")
                (("2" (expand "time_closest")
                  (("2" (lift-if)
                    (("2" (assert)
                      (("2" (ground)
                        (("2" (rewrite "dot_sq_norm" :dir rl)
                          (("2" (expand "sqv") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((time_cpa formula-decl nil closest_approach_2D nil)
    (time_closest const-decl "real" closest_approach_2D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (tau_2D const-decl "real" closest_approach_relative_2D 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)
    (Nz_vect2 type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (/= const-decl "boolean" notequal 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil))
   nil)
  (tau_is_min-1 nil 3474890758
   ("" (skosimp*)
    (("" (lemma "time_cpa")
      (("" (skoletin 1)
        (("" (inst - "s!1" "zero" "tau" "nzv!1" "zero")
          (("" (split -2)
            (("1" (hide -2)
              (("1"
                (case-replace
                 "(LAMBDA t: sq_dist(s!1 + t * nzv!1, zero + t * zero)) = 
(LAMBDA t: sq(norm(s!1 + t * nzv!1)))")
                (("1" (apply-extensionality 1 :hide? t)
                  (("1" (hide -1 2)
                    (("1" (rewrite "dot_sq_norm" :dir rl)
                      (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (expand "tau_2D")
                (("2" (expand "time_closest")
                  (("2" (lift-if)
                    (("2" (assert)
                      (("2" (ground)
                        (("2" (rewrite "dot_sq_norm" :dir rl)
                          (("2" (expand "sqv") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Nz_vect2 type-eq-decl nil vectors_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (norm const-decl "nnreal" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D nil)
    (sq_dist const-decl "nnreal" distance_2D nil)
    (comp_zero_x formula-decl nil vectors_2D nil)
    (comp_zero_y formula-decl nil vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (dot_sq_norm formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (add_zero_left formula-decl nil vectors_2D nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D nil)
    (sqv const-decl "nnreal" vectors_2D nil)
    (sub_zero_right formula-decl nil vectors_2D nil)
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (time_closest const-decl "real" closest_approach_2D nil)
    (time_cpa formula-decl nil closest_approach_2D nil))
   shostak))
 (dist_tau_min 0
  (dist_tau_min-1 nil 3475859369
   ("" (skosimp*)
    (("" (expand "dist_tau")
      (("" (expand "tau")
        (("" (lift-if)
          (("" (split +)
            (("1" (flatten)
              (("1" (assert)
                (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (flatten)
              (("2" (lemma "tau_is_min")
                (("2" (inst - "v!1" "s!1")
                  (("1" (assert)
                    (("1" (expand "is_minimum?")
                      (("1" (expand "tau_2D")
                        (("1" (inst - "t!1")
                          (("1" (assert)
                            (("1" (lemma "sq_le")
                              (("1"
                                (inst?)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist_tau const-decl "real" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D nil)
    (v!1 skolem-const-decl "Vect2" closest_approach_relative_2D nil)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Nz_vect2 type-eq-decl nil vectors_2D nil)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (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)
    (sq_le formula-decl nil sq "reals/")
    (sqv const-decl "nnreal" vectors_2D nil)
    (* const-decl "real" vectors_2D nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "Vector" vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (norm const-decl "nnreal" vectors_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (tau_2D const-decl "real" closest_approach_relative_2D nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (tau_is_min formula-decl nil closest_approach_relative_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (add_zero_right formula-decl nil vectors_2D nil)
    (scal_0 formula-decl nil vectors_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (tau const-decl "real" closest_approach_relative_2D nil))
   shostak))
 (tau_sqv_min 0
  (tau_sqv_min-1 nil 3475860222
   ("" (skosimp*)
    (("" (expand "tau")
      (("" (lift-if)
        (("" (split +)
          (("1" (flatten)
            (("1" (assert)
              (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (flatten)
            (("2" (lemma "tau_is_min")
              (("2" (inst - "v!1" "s!1")
                (("1" (assert)
                  (("1" (expand "is_minimum?")
                    (("1" (expand "tau_2D")
                      (("1" (inst - "t!1")
                        (("1" (rewrite "sq_norm")
                          (("1" (rewrite "sq_norm") nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tau const-decl "real" closest_approach_relative_2D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (add_zero_right formula-decl nil vectors_2D nil)
    (scal_0 formula-decl nil vectors_2D nil)
    (scal_zero formula-decl nil vectors_2D nil)
    (tau_is_min formula-decl nil closest_approach_relative_2D nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (tau_2D const-decl "real" closest_approach_relative_2D nil)
    (sq_norm formula-decl nil vectors_2D nil)
    (+ const-decl "Vector" vectors_2D nil)
    (* const-decl "Vector" vectors_2D 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)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_2D nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D 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)
    (is_minimum? const-decl "bool" quad_minmax "reals/")
    (Nz_vect2 type-eq-decl nil vectors_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)
    (Vect2 type-eq-decl nil vectors_2D_def nil)
    (v!1 skolem-const-decl "Vect2" closest_approach_relative_2D nil)
    (zero const-decl "Vector" vectors_2D nil))
   nil)))