Quelle distance_3D.prf Sprache: Lisp

(distance_3D
(dist_eq_args 0
  (dist_eq_args-1 nil 3285687290
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "dist")
        (("" (expand "sq_dist") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (dist const-decl "nnreal" distance_3D nil))
   shostak))
(dist_zero_l 0
  (dist_zero_l-1 nil 3285687305
   ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_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)
    (norm const-decl "nnreal" vectors_3D nil)
    (sqv const-decl "nnreal" vectors_3D nil)
    (* const-decl "real" vectors_3D nil)
    (dist const-decl "nnreal" distance_3D nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (zero const-decl "Vector" vectors_3D nil))
   shostak))
(dist_zero_r 0
  (dist_zero_r-1 nil 3285687329 ("" (grind) nil nil)
   ((zero const-decl "Vector" vectors_3D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nnreal" distance_3D nil)
    (dist const-decl "nnreal" distance_3D nil)
    (* const-decl "real" vectors_3D nil)
    (sqv const-decl "nnreal" vectors_3D nil)
    (norm const-decl "nnreal" vectors_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
(dist_sym 0
  (dist_sym-1 nil 3255275743 ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nnreal" distance_3D nil)
    (dist const-decl "nnreal" distance_3D nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
(dist_eq_0 0
  (dist_eq_0-3 nil 3285687359
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "dist")
        (("1" (expand "sq_dist")
          (("1" (rewrite "sq_eq" :dir rl)
            (("1" (rewrite "sq_sqrt")
              (("1"
                (case "sq(p1!1`x - p2!1`x) = 0 AND sq(p1!1`y - p2!1`y) = 0 AND sq(p1!1`z - p2!1`z) = 0")
                (("1" (flatten)
                  (("1" (hide -4)
                    (("1" (apply-extensionality 1 :hide? t)
                      (("1" (rewrite "sq.sq_eq_0") nil nil)
                       ("2" (hide -1)
                        (("2" (rewrite "sq.sq_eq_0") nil nil)) nil)
                       ("3" (hide -1 -2)
                        (("3" (rewrite "sq.sq_eq_0") nil nil)) nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (replace -1) (("2" (rewrite "dist_eq_args") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sq_eq_0 formula-decl nil sq "reals/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (sq_0 formula-decl nil sq "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (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)
    (sq_eq formula-decl nil sq "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (dist const-decl "nnreal" distance_3D nil)
    (dist_eq_args formula-decl nil distance_3D nil))
   nil)
  (dist_eq_0-2 nil 3256562733
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "dist")
        (("1" (expand "sq_dist")
          (("1" (rewrite "sq_eq" :dir rl)
            (("1" (rewrite "sq_sqrt")
              (("1" (rewrite "sq_0")
                (("1"
                  (case "sq(p1!1`x - p2!1`x) = 0 AND sq(p1!1`y - p2!1`y) = 0 AND sq(p1!1`z - p2!1`z) = 0")
                  (("1" (flatten)
                    (("1" (hide -4)
                      (("1" (apply-extensionality 1 :hide? t)
                        (("1" (rewrite "sq.sq_eq_0") nil nil)
                         ("2" (hide -1)
                          (("2" (rewrite "sq.sq_eq_0") nil nil)) nil)
                         ("3" (hide -1 -2)
                          (("3" (rewrite "sq.sq_eq_0") nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (replace -1) (("2" (rewrite "dist_refl") nil nil)) nil))
        nil))
      nil))
    nil)
   ((sq_sqrt formula-decl nil sqrt "reals/")
    (sq_eq_0 formula-decl nil sq "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sq_eq formula-decl nil sq "reals/"))
   nil)
  (dist_eq_0-1 nil 3255275743
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "dist")
        (("1" (expand "sq_dist")
          (("1" (rewrite "sq_eq" :dir rl)
            (("1" (rewrite "sq_sqrt")
              (("1" (rewrite "sq_0")
                (("1"
                  (case "sq(v1!1`x - v2!1`x) = 0 AND sq(v1!1`y - v2!1`y) = 0")
                  (("1" (hide -2)
                    (("1" (flatten)
                      (("1" (apply-extensionality 1 :hide? t)
                        (("1" (rewrite "sq.sq_eq_0") nil nil)
                         ("2" (hide -1)
                          (("2" (rewrite "sq.sq_eq_0") nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide 2) (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (replace -1) (("2" (rewrite "dist_refl") nil nil)) nil))
      nil))
    nil)
   ((sq_sqrt formula-decl nil sqrt "reals/")
    (sq_eq_0 formula-decl nil sq "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sq_eq formula-decl nil sq "reals/"))
   nil))
(dist_norm 0
  (dist_norm-1 nil 3255275743
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "norm")
        (("" (expand "sq_dist")
          (("" (expand "sq")
            (("" (assert)
              (("" (expand "sqv")
                (("" (expand "*")
                  (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (* const-decl "real" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (sqv const-decl "nnreal" vectors_3D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (norm const-decl "nnreal" vectors_3D nil))
   nil))
(dist_rel 0
  (dist_rel-1 nil 3255275743 ("" (skosimp*) (("" (grind) nil nil)) 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dist const-decl "nnreal" distance_3D nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ const-decl "Vector" vectors_3D nil))
   nil))
(sq_dist_is_dist_sq 0
  (sq_dist_is_dist_sq-1 nil 3255275743 ("" (grind) nil nil)
   ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nnreal" distance_3D nil)
    (dist const-decl "nnreal" distance_3D nil)
    (real_times_real_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))
   nil))
(sq_dist_norm 0
  (sq_dist_norm-1 nil 3255717113
   ("" (skosimp*)
    (("" (rewrite "sq_dist_is_dist_sq")
      (("" (rewrite "dist_norm") nil nil)) nil))
    nil)
   ((sq_dist_is_dist_sq formula-decl nil distance_3D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (dist_norm formula-decl nil distance_3D nil))
   shostak))
(sq_dist_sym 0
  (sq_dist_sym-1 nil 3255277056
   ("" (skosimp*)
    (("" (rewrite "sq_dist_is_dist_sq")
      (("" (rewrite "sq_dist_is_dist_sq")
        (("" (rewrite "dist_sym") nil nil)) nil))
      nil))
    nil)
   ((sq_dist_is_dist_sq formula-decl nil distance_3D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (dist_sym formula-decl nil distance_3D nil))
   shostak))
(sq_dist_le 0
  (sq_dist_le-1 nil 3256052713
   ("" (skosimp*)
    (("" (expand "dist") (("" (rewrite "sqrt_le") nil nil)) nil)) nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vect3 type-eq-decl nil vectors_3D_def 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)
    (sqrt_le formula-decl nil sqrt "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(sq_dist_lt 0
  (sq_dist_lt-1 nil 3256052727
   ("" (skosimp*)
    (("" (expand "dist") (("" (rewrite "sqrt_lt") nil nil)) nil)) nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vect3 type-eq-decl nil vectors_3D_def 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)
    (sqrt_lt formula-decl nil sqrt "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(dist_ge_x 0
  (dist_ge_x-2 nil 3256562809
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case "sqrt(sq(p1!1`x - p2!1`x) + sq(p1!1`y - p2!1`y)+ sq(p1!1`z - p2!1`z)) >= sqrt(sq(p1!1`x - p2!1`x))")
          (("1" (rewrite "sqrt_sq_abs") nil nil)
           ("2" (hide 2)
            (("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (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)
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (dist_ge_x-1 nil 3256552897
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case "sqrt(sq(v1!1`x - v2!1`x) + sq(v1!1`y - v2!1`y)) >= sqrt(sq(v1!1`x - v2!1`x))")
          (("1" (rewrite "sqrt_sq_abs") nil nil)
           ("2" (hide 2)
            (("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/"))
   nil))
(dist_ge_y 0
  (dist_ge_y-3 nil 3256920758
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case "sqrt(sq(p1!1`x - p2!1`x) + sq(p1!1`y - p2!1`y) + sq(p1!1`z - p2!1`z)) >= sqrt(sq(p1!1`y - p2!1`y))")
          (("1" (rewrite "sqrt_sq_abs") nil nil)
           ("2" (hide 2)
            (("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (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)
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (dist_ge_y-2 nil 3256562825
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case "sqrt(sq(p1!1`x - p2!1`x) + sq(p1!1`y - p2!1`y)) >= sqrt(sq(p1!1`y - p2!1`y))")
          (("1" (rewrite "sqrt_sq_abs") nil nil)
           ("2" (hide 2)
            (("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/"))
   nil)
  (dist_ge_y-1 nil 3256552923
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case "sqrt(sq(v1!1`x - v2!1`x) + sq(v1!1`y - v2!1`y)) >= sqrt(sq(v1!1`y - v2!1`y))")
          (("1" (rewrite "sqrt_sq_abs") nil nil)
           ("2" (hide 2)
            (("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/"))
   nil))
(dist_ge_z 0
  (dist_ge_z-1 nil 3256920786
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case "sqrt(sq(p1!1`x - p2!1`x) + sq(p1!1`y - p2!1`y) + sq(p1!1`z - p2!1`z)) >= sqrt(sq(p1!1`z - p2!1`z))")
          (("1" (rewrite "sqrt_sq_abs") nil nil)
           ("2" (hide 2)
            (("2" (rewrite "sqrt_ge") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (+ 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (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)
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(sq_dist_dist 0
  (sq_dist_dist-1 nil 3445159578
   ("" (skosimp*)
    (("" (lemma "sq_norm_dist")
      (("" (inst -1 "p0!1" "p1!1" "p2!1")
        (("" (assert)
          (("" (assert)
            (("" (rewrite "dist_norm")
              (("" (rewrite "dist_norm")
                (("" (rewrite "dist_norm") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_norm_dist formula-decl nil vectors_3D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (dot_scal_left formula-decl nil vectors_3D nil)
    (dist_norm formula-decl nil distance_3D nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (real nonempty-type-from-decl nil reals nil))
   nil))
(dist_triangle 0
  (dist_triangle-1 nil 3445159647
   ("" (skeep)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        ((""
          (case-replace
           "sq(p0`x - p2`x) = sq(p0`x - p1`x + p1`x - p2`x)")
          (("1" (hide -1)
            (("1"
              (case-replace
               "sq(p0`y - p2`y) = sq(p0`y - p1`y + p1`y - p2`y)")
              (("1" (hide -1)
                (("1"
                  (case-replace
                   "sq(p0`z - p2`z) = sq(p0`z - p1`z + p1`z - p2`z)")
                  (("1" (lemma "schwarz_cor")
                    (("1" (inst - "p0-p1" "p1-p2")
                      (("1" (grind) nil nil)) nil))
                    nil)
                   ("2" (hide 2) (("2" (assert) nil nil)) nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil)
           ("2" (hide 2) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance_3D nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (sq const-decl "nonneg_real" sq "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vector" vectors_3D nil)
    (Vector type-eq-decl nil vectors_3D nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sqv const-decl "nnreal" vectors_3D nil)
    (* const-decl "real" vectors_3D nil)
    (+ const-decl "Vector" vectors_3D nil)
    (schwarz_cor formula-decl nil vectors_3D nil)
    (sq_dist const-decl "nnreal" distance_3D nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   nil))
(dist_tri_sub 0
  (dist_tri_sub-1 nil 3445160015
   ("" (skeep)
    (("" (lemma "dist_triangle")
      (("" (inst-cp - "p0" "p1" "p2")
        (("" (inst - "p1" "p0" "p2")
          (("" (expand "abs")
            (("" (lift-if)
              (("" (ground)
                (("" (lemma "dist_sym")
                  (("" (inst - "p0" "p1") (("" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist_triangle formula-decl nil distance_3D nil)
    (dist_sym formula-decl nil distance_3D nil)
    (minus_real_is_real application-judgement "real" reals 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)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
(on_segment_beg 0
  (on_segment_beg-1 nil 3255349846
   ("" (skosimp*)
    (("" (expand "on_segment?")
      (("" (inst + "0")
        (("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((on_segment? const-decl "bool" distance_3D nil)
    (+ const-decl "Vector" vectors_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_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)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (<= const-decl "bool" reals nil)
    (nnreal 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))
   shostak))
(on_segment_end 0
  (on_segment_end-1 nil 3255349879
   ("" (skosimp*)
    (("" (expand "on_segment?")
      (("" (inst + "1")
        (("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((on_segment? const-decl "bool" distance_3D nil)
    (+ const-decl "Vector" vectors_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_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)
    (Vect3 type-eq-decl nil vectors_3D_def nil)
    (<= const-decl "bool" reals nil)
    (nnreal 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))
   shostak))
(on_line_beg 0
  (on_line_beg-1 nil 3255689996
   ("" (skosimp*)
    (("" (expand "on_line?")
      (("" (inst + "0")
        (("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((on_line? const-decl "bool" distance_3D nil)
    (+ const-decl "Vector" vectors_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_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)
    (Vect3 type-eq-decl nil vectors_3D_def 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))
   shostak))
(on_line_end 0
  (on_line_end-1 nil 3255690905
   ("" (skosimp*)
    (("" (expand "on_line?")
      (("" (inst + "1")
        (("" (grind) (("" (apply-extensionality 1 :hide? t) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((on_line? const-decl "bool" distance_3D nil)
    (+ const-decl "Vector" vectors_3D nil)
    (* const-decl "Vector" vectors_3D nil)
    (- const-decl "Vector" vectors_3D nil)
    (real_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)
    (Vect3 type-eq-decl nil vectors_3D_def 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))
   shostak))
(on_segment_on_line 0
  (on_segment_on_line-1 nil 3255349896
   ("" (skosimp*)
    (("" (expand "on_segment?")
      (("" (expand "on_line?")
        (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
      nil))
    nil)
   ((on_segment? const-decl "bool" distance_3D nil)
    (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)
    (nnreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (on_line? const-decl "bool" distance_3D nil))
   shostak)))

quality93%

¤ Dauer der Verarbeitung: 0.20 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.