products/Sources/formale Sprachen/PVS/vectors/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: distance.prf   Sprache: Lisp

Original von: PVS©
(distance
 (sq_dist_TCC1 0
  (sq_dist_TCC1-1 nil 3255973523
   ("" (assert) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (sq_dist_TCC2 0
  (sq_dist_TCC2-1 nil 3255973523
   ("" (assert) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (sq_dist_TCC3 0
  (sq_dist_TCC3-1 nil 3255973523
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
 (dist_eq_args 0
  (dist_eq_args-2 nil 3285687462
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (case-replace "sq_dist(p!1, p!1) = 0")
        (("1" (rewrite "sqrt_0") nil nil)
         ("2" (hide 2)
          (("2" (expand "sq_dist")
            (("2" (rewrite "sq_0")
              (("2" (lemma "sigma_const[Index[n]]")
                (("1" (inst?)
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (assert) nil nil))
                  nil)
                 ("2" (skosimp*) (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance nil)
    (sq_0 formula-decl nil sq "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (sigma_nat application-judgement "nat" vectors nil)
    (sigma_nnreal application-judgement "nnreal" vectors nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (sigma_const formula-decl nil sigma "reals/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sq_dist const-decl "nnreal" distance nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)
  (dist_eq_args-1 nil 3285687404
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (assert) (("" (postpone) nil nil)) nil)) nil))
      nil))
    nil)
   nil shostak))
 (dist_zero_l 0
  (dist_zero_l-1 nil 3285687470 ("" (grind) nil nil)
   ((zero const-decl "Vector" vectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nnreal" distance nil)
    (dist const-decl "nnreal" distance nil)
    (* const-decl "real" vectors nil)
    (sqv const-decl "nnreal" vectors nil)
    (norm const-decl "nnreal" vectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (dist_zero_r 0
  (dist_zero_r-1 nil 3285687540 ("" (grind) nil nil)
   ((zero const-decl "Vector" vectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nnreal" distance nil)
    (dist const-decl "nnreal" distance nil)
    (* const-decl "real" vectors nil)
    (sqv const-decl "nnreal" vectors nil)
    (norm const-decl "nnreal" vectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (dist_sym 0
  (dist_sym-2 nil 3256922339
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (rewrite "sqrt_eq")
        (("" (expand "sq_dist")
          ((""
            (case "(LAMBDA i: sq(p2!1(i) - p1!1(i))) = (LAMBDA i: sq(p1!1(i) - p2!1(i)))")
            (("1" (assert) nil nil)
             ("2" (hide 2)
              (("2" (apply-extensionality 1 :hide? t)
                (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance nil)
    (real_times_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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sigma_nnreal application-judgement "nnreal" vectors nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sq_dist const-decl "nnreal" distance nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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_eq formula-decl nil sqrt "reals/"))
   nil)
  (dist_sym-1 nil 3255275743
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (rewrite "sqrt_eq")
        (("" (expand "sq_dist")
          ((""
            (case "(LAMBDA i: sq(v2!1(i) - v1!1(i))) = (LAMBDA i: sq(v1!1(i) - v2!1(i)))")
            (("1" (assert) nil nil)
             ("2" (hide 2)
              (("2" (apply-extensionality 1 :hide? t)
                (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (Index type-eq-decl nil vectors nil)
    (sqrt_eq formula-decl nil sqrt "reals/"))
   nil))
 (dist_eq_0 0
  (dist_eq_0-2 nil 3285687929
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "dist")
        (("1" (expand "sq_dist")
          (("1" (rewrite "sq_eq" :dir rl)
            (("1" (rewrite "sq_sqrt")
              (("1" (apply-extensionality 1 :hide? t)
                (("1" (lemma "sigma_nonneg_eq_0[Index[n]]")
                  (("1" (inst?)
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (rewrite "sq_eq_0") nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -1)
                (("2" (lemma "sigma_nonneg[Index[n]]")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (hide 2)
                        (("2" (skosimp*) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (replace -1) (("2" (rewrite "dist_eq_args") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((sq_dist const-decl "nnreal" distance nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sigma_nonneg_eq_0 formula-decl nil sigma "reals/")
    (sq_eq_0 formula-decl nil sq "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Vector type-eq-decl nil vectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sigma def-decl "real" sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (Index type-eq-decl nil vectors nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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/")
    (sigma_nnreal application-judgement "nnreal" vectors nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (dist const-decl "nnreal" distance nil)
    (dist_eq_args formula-decl nil distance nil))
   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" (apply-extensionality 1 :hide? t)
                  (("1" (lemma "sigma_nonneg_eq_0[Index[n]]")
                    (("1" (inst?)
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (rewrite "sq_eq_0") nil nil)) nil))
                        nil))
                      nil)
                     ("2" (skosimp*) (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*) (("2" (assert) nil nil)) nil))
              nil)
             ("2" (skosimp*) (("2" (assert) 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/")
    (sigma_nonneg_eq_0 formula-decl nil sigma "reals/")
    (sq_0 formula-decl nil sq "reals/")
    (sq const-decl "nonneg_real" sq "reals/")
    (sigma def-decl "real" sigma "reals/")
    (Index type-eq-decl nil vectors nil)
    (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 nil)
    (sq_dist const-decl "nnreal" distance 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" vectors nil) (- const-decl "real" vectors nil)
    (sqv const-decl "nnreal" vectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (norm const-decl "nnreal" vectors nil))
   nil))
 (dist_rel 0
  (dist_rel-1 nil 3255275743 ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((+ const-decl "real" vectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq_dist const-decl "nnreal" distance nil)
    (dist const-decl "nnreal" distance nil)
    (real_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)
    (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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sigma_nnreal application-judgement "nnreal" vectors nil))
   nil))
 (sq_dist_is_dist_sq 0
  (sq_dist_is_dist_sq-1 nil 3255275743 ("" (grind) nil 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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 nil)
    (dist const-decl "nnreal" distance nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers 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 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" distance nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (dist_norm formula-decl nil distance 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 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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (n formal-const-decl "posnat" distance nil)
    (Index type-eq-decl nil vectors nil)
    (Vector type-eq-decl nil vectors nil)
    (dist_sym formula-decl nil distance nil))
   shostak))
 (sq_dist_le 0
  (sq_dist_le-1 nil 3256052813
   ("" (skosimp*)
    (("" (expand "dist") (("" (rewrite "sqrt_le") nil nil)) nil)) nil)
   ((dist const-decl "nnreal" distance nil)
    (sq_dist const-decl "nnreal" distance nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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 3256052824
   ("" (skosimp*)
    (("" (expand "dist") (("" (rewrite "sqrt_lt") nil nil)) nil)) nil)
   ((dist const-decl "nnreal" distance nil)
    (sq_dist const-decl "nnreal" distance nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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_gt_comp 0
  (dist_gt_comp-1 nil 3255974076
   ("" (skosimp*)
    (("" (expand "dist")
      (("" (expand "sq_dist")
        (("" (lemma "sigma_nn_ge_comps[below(n)]")
          (("1" (inst?)
            (("1" (inst?)
              (("1" (assert)
                (("1" (lemma "sqrt_ge")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (rewrite "sqrt_sq_abs") nil nil)) nil)
                     ("2" (skosimp*) (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((dist const-decl "nnreal" distance nil)
    (below type-eq-decl nil naturalnumbers nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (sigma_nn_ge_comps formula-decl nil sigma "reals/")
    (sqrt_ge formula-decl nil sqrt "reals/")
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (sigma def-decl "real" sigma "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_nnreal application-judgement "nnreal" vectors nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (Vector type-eq-decl nil vectors nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (Index type-eq-decl nil vectors nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sq_dist const-decl "nnreal" distance nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (sq_dist_dist 0
  (sq_dist_dist-1 nil 3445159685
   ("" (skosimp*)
    (("" (lemma "sq_norm_dist[n]")
      (("" (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)
   ((n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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_norm_dist formula-decl nil vectors 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 nil)
    (dist_norm formula-decl nil distance nil)
    (Vector type-eq-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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 nil)
    (scal_0 formula-decl nil vectors nil)
    (add_zero_right formula-decl nil vectors 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 nil)
    (scal_1 formula-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (Vector type-eq-decl nil vectors nil)
    (+ const-decl "real" vectors nil) (- const-decl "real" vectors 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 nil)
    (scal_0 formula-decl nil vectors nil)
    (add_zero_right formula-decl nil vectors 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 nil)
    (scal_1 formula-decl nil vectors nil)
    (Index type-eq-decl nil vectors nil)
    (n formal-const-decl "posnat" distance nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (< const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "real" vectors nil) (+ const-decl "real" vectors nil)
    (Vector type-eq-decl nil vectors 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 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 nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.59 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff