Quelle distance.prf
Sprache: Lisp
(distancenil 3255973523"" (assert ) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3255973523"" (assert ) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil 3255973523"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))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 )"nnreal" distance nil )nil sq "reals/" )"int" integers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nat" vectors nil )"nnreal" vectors nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )"int" integers nil )nil sigma "reals/" )nil sqrt "reals/" )"nnreal" distance nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil ))nil )nil 3285687404"" (skosimp*)"" (expand "dist" )"" (expand "sq_dist" )"" (assert ) (("" (postpone) nil nil )) nil )) nil ))nil ))nil )nil shostak))nil 3285687470 ("" (grind) nil nil )"Vector" vectors nil )"nonneg_real" sq "reals/" )"nnreal" distance nil )"nnreal" distance nil )"real" vectors nil )"nnreal" vectors nil )"nnreal" vectors nil )"int" integers nil ))nil 3285687540 ("" (grind) nil nil )"Vector" vectors nil )"nonneg_real" sq "reals/" )"nnreal" distance nil )"nnreal" distance nil )"real" vectors nil )"nnreal" vectors nil )"nnreal" vectors nil )"int" integers nil ))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 )"nnreal" distance nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"nnreal" vectors nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" sq "reals/" )"[T, T -> boolean]" equalities nil )"real" reals nil )"nnreal" distance nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" ))nil )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 )"nonneg_real" sq "reals/" )nil vectors nil )nil sqrt "reals/" ))nil ))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 )"nnreal" distance nil )nil sqrt "reals/" )nil sigma "reals/" )nil sq "reals/" )nil sq "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil vectors nil )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )nil vectors nil )nil naturalnumbers nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sq "reals/" )"nnreal" vectors nil )"real" reals nil )"int" integers nil )"nnreal" distance nil )nil distance nil ))nil )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 )nil sqrt "reals/" )nil sq "reals/" )nil sigma "reals/" )nil sq "reals/" )"nonneg_real" sq "reals/" )"real" sigma "reals/" )nil vectors nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sq "reals/" ))nil ))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 )"nnreal" distance nil )"nnreal" distance nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"real" vectors nil ) (- const-decl "real" vectors nil )"nnreal" vectors nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"nnreal" vectors nil ))nil ))nil 3255275743 ("" (skosimp*) (("" (grind) nil nil )) nil )"real" vectors nil )"nonneg_real" sq "reals/" )"nnreal" distance nil )"nnreal" distance nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )"nnreal" vectors nil ))nil ))nil 3255275743 ("" (grind) nil nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"nonneg_real" sq "reals/" )"nnreal" distance nil )"nnreal" distance nil )"real" reals nil )"int" integers nil )"real" reals nil ))nil ))nil 3255717113"" (skosimp*)"" (rewrite "sq_dist_is_dist_sq" )"" (rewrite "dist_norm" ) nil nil )) nil ))nil )nil distance nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" distance nil )nil vectors nil )nil vectors nil )nil distance nil ))nil 3255277056"" (skosimp*)"" (rewrite "sq_dist_is_dist_sq" )"" (rewrite "sq_dist_is_dist_sq" )"" (rewrite "dist_sym" ) nil nil )) nil ))nil ))nil )nil distance nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" distance nil )nil vectors nil )nil vectors nil )nil distance nil ))nil 3256052813"" (skosimp*)"" (expand "dist" ) (("" (rewrite "sqrt_le" ) nil nil )) nil )) nil )"nnreal" distance nil )"nnreal" distance nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" )"(total_order?[real])" nil ))nil 3256052824"" (skosimp*)"" (expand "dist" ) (("" (rewrite "sqrt_lt" ) nil nil )) nil )) nil )"nnreal" distance nil )"nnreal" distance nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" )"(strict_total_order?[real])" real_props nil ))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 )"nnreal" distance nil )nil naturalnumbers nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )"real" sigma "reals/" )"(total_order?[real])" nil )"nnreal" vectors nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"nonneg_real" sq "reals/" )nil vectors nil )nil real_types nil )"int" integers nil )"nnreal" distance nil )"real" reals nil ))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 )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil )"real" reals nil )"real" reals nil )"nnreal" nil )nil vectors nil )nil distance nil )nil vectors nil )nil vectors nil )"bool" reals nil )nil naturalnumbers nil ))nil ))nil 3255349846"" (skosimp*)"" (expand "on_segment?" )"" (inst + "0" )"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil )"bool" distance nil )nil vectors nil )nil vectors nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3255349879"" (skosimp*)"" (expand "on_segment?" )"" (inst + "1" )"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil )"bool" distance nil )nil vectors nil )nil vectors nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" reals nil )"real" reals nil )nil vectors nil )"real" vectors nil ) (- const-decl "real" vectors nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3255689996"" (skosimp*)"" (expand "on_line?" )"" (inst + "0" )"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil )"bool" distance nil )nil vectors nil )nil vectors nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3255690905"" (skosimp*)"" (expand "on_line?" )"" (inst + "1" )"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil ))nil ))nil )"bool" distance nil )nil vectors nil )nil vectors nil )"posnat" distance nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" reals nil )"real" reals nil )"real" vectors nil ) (+ const-decl "real" vectors nil )nil vectors nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3255349896"" (skosimp*)"" (expand "on_segment?" )"" (expand "on_line?" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil )"bool" distance nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"bool" distance nil ))quality 100%
¤ 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.0.18Bemerkung:
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
