SSL vectors_2D.prf
Sprache: Lisp
(vectors_2Dnil 3254160320 ("" (subtype-tcc) nil nil )"real" vectors_2D nil )"real" reals nil ))nil ))nil 3440239073 ("" (grind) nil nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"real" reals nil ))nil 3602098877 ("" (grind) nil nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"nonneg_real" sq "reals/" )"nnreal" vectors_2D nil )"real" reals nil ))nil 3430835111 ("" (subtype-tcc) nil nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )nil sqrt "reals/" )"nnreal" vectors_2D nil ))nil ))nil 3430835111 ("" (subtype-tcc) nil nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )nil sqrt "reals/" )"nnreal" vectors_2D nil ))nil ))nil 3428691871 ("" (grind) nil nil )"Normalized" vectors_2D nil )"Vector" vectors_2D nil )"Normalized" vectors_2D nil )"Vector" vectors_2D nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3256995680 ("" (grind) nil nil )"Vector" vectors_2D nil )) shostak))nil 3256995684 ("" (grind) nil nil )"Vector" vectors_2D nil )) shostak))nil 3467129742 ("" (grind) nil nil )"Vector" vectors_2D nil )) shostak))nil 3467129756 ("" (grind) nil nil )"Vector" vectors_2D nil )) shostak))nil 3268398885"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3268398889"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3440253283"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil reals nil )nil vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3428184293"" (skeep)"" (expand "norm" )"" (split)"1" (lemma "sqrt_eq_0" )"1" (inst -1 "sqv(v)" )"1" (split -1)"1" (rewrite "sqv_sos" )"1" (expand "sos" )"1" (rewrite "sq_plus_eq_0" )"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (rewrite "sqv_sos" )"2" (expand "sos" )"2" (replaces -) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )"nnreal" vectors_2D nil )"nnreal" nil )nil sq "reals/" )nil vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )nil vectors_2D 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 3428186268"" (skeep)"" (expand "norm" )"" (ground) (("" (replaces -1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )nil sqrt "reals/" ))nil ))nil 3430054210"" (skeep)"" (lemma "norm_xy_eq_0" )"" (inst?)"" (replaces -1)"" (grind) (("" (decompose-equality) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil reals nil ))nil ))nil 3430759050"" (lemma "norm_eq_0" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil )nil reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil ))nil ))nil 3254160320"" (skeep)"" (lemma "norm_sqv_eq_0" )"" (inst?)"" (replaces -1 :dir rl)"" (lemma "norm_eq_0" ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil reals nil ))nil ))nil 3428185676"" (skeep)"" (lemma "sqv_eq_0" ) (("" (inst?) (("" (ground) nil nil )) nil ))nil ))nil )nil vectors_2D nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )nil reals nil ))nil 3428790623"" (skeep)"" (lemma "v_neq_zero" )"" (inst?)"" (expand "sqv" )"" (ground) (("" (replaces -1) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )"nnreal" vectors_2D nil )"real" vectors_2D nil )"Vector" vectors_2D nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )nil reals nil ))nil ))nil 3430757168"" (skeep)"" (expand "nz_vector?" )"" (lemma "norm_eq_0" )"" (inst?)"" (lemma "norm_xy_eq_0" )"" (inst?)"" (replaces -1) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil reals nil ))nil 3430589561"" (skeep :preds? t)"" (expand "nz_vector?" )"" (flatten)"" (lemma "norm_eq_0" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_2D nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )"Vector" vectors_2D nil )"boolean" notequal nil )nil booleans nil )nil vectors_2D nil )nil reals nil ))nil ))nil 3430589561"" (skeep :preds? t)"" (lemma "v_neq_zero" )"" (inst?)"" (expand "nz_vector?" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil vectors_2D nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )"Vector" vectors_2D nil )"boolean" notequal nil )nil booleans nil )nil vectors_2D nil )nil reals nil ))nil ))nil 3430835111 ("" (judgement-tcc) nil nil )"Vector" vectors_2D nil )) nil ))nil 3430835111 ("" (judgement-tcc) nil nil )"Vector" vectors_2D nil )) nil ))nil 3430590288"" (skeep :preds? t)"" (assert )"" (lemma "norm_eq_0" )"" (inst?)"" (expand "nz_vector?" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil reals nil )nil vectors_2D nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil ))nil ))nil 3431076610"" (grind) (("" (decompose-equality 1) nil nil )) nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D nil )"boolean" notequal nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3431179123"" (grind)"" (decompose-equality 2)"1" (grind-reals) nil nil ) ("2" (grind-reals) nil nil )) nil ))nil )nil real_props nil )nil real_props nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil reals nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3462009581 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil 3254160320"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )) nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3268401003"" (skosimp*)"" (grind)"1" (apply-extensionality 1 :hide? t) nil nil )"2" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil )nil reals nil )nil vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D_def nil ))nil 3254160320"" (grind)"1" (apply-extensionality 1 :hide? t) nil nil )"2" (apply-extensionality :hide? t) nil nil ))nil )nil vectors_2D_def nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )nil reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320"" (grind)"1" (apply-extensionality :hide? t) nil nil )"2" (apply-extensionality :hide? t) nil nil ))nil )nil vectors_2D nil )nil reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )"[numfield -> numfield]" number_fields nil )nil vectors_2D_def nil )nil reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3255191564"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil 3255191572"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil 3268401026"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil reals nil )nil vectors_2D nil )"Vector" vectors_2D nil ))nil 3268401043"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil reals nil )nil vectors_2D nil )"Vector" vectors_2D nil ))nil 3467130470"" (grind) (("" (decompose-equality 1) nil nil )) nil )nil reals nil )nil vectors_2D nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil 3467130477"" (grind)"1" (decompose-equality 1) nil nil )"2" (decompose-equality 1) nil nil ))nil )nil vectors_2D_def nil )nil reals nil )nil vectors_2D nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"Vector" vectors_2D nil ))nil 3430753136"" (grind) (("" (decompose-equality 1) nil nil )) nil )nil vectors_2D nil )nil reals nil )"real" reals nil )"Vector" vectors_2D nil ))nil 3430753152"" (skeep) (("" (grind) (("" (decompose-equality 1) nil nil )) nil ))nil )"Vector" vectors_2D nil )"real" reals nil )nil reals nil )nil vectors_2D nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_2D nil )nil reals nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil vectors_2D nil )nil reals nil )nil vectors_2D_def nil )"real" reals nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3429977937 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" vectors_2D nil )"real" reals nil ))nil ))nil 3440244987 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3440244991 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3477648453 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil ))nil 3268401067"" (skosimp*)"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil )"Vector" vectors_2D nil )"real" reals nil )nil vectors_2D nil )nil reals nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil ))nil ))nil 3440245242 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil ))nil 3430579398 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3440245250 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3256912742 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil ))nil 3254656786 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil ))nil 3254656137 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3254656141 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3430578793 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil ))nil 3430578824"" (skeep)"" (split)"1" (flatten)"1" (replaces -1 :dir rl)"1" (decompose-equality 1)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil )"2" (flatten)"2" (replaces -1)"2" (decompose-equality 1)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )nil reals nil )nil vectors_2D nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )"Vector" vectors_2D nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nzreal" nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil ))nil 3430578421"" (skeep)"" (decompose-equality)"1" (grind) nil nil ) ("2" (grind) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil reals nil )"real" reals nil ))nil 3467130399 ("" (grind) nil nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"odd_int" integers nil ))nil 3255949385"" (skeep)"" (grind)"" (mult-by 1 "nzv`x" )"" (mult-by 1 "nzv`y" )"" (typepred "nzv" )"" (lemma "norm_xy_eq_0" )"" (inst?) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_2D nil )"real" reals nil )nil vectors_2D nil )"posreal" vectors_2D nil )"Nz_vector" vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"boolean" notequal nil )nil vectors_2D nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil real_props nil ))nil ))nil 3440245792"" (grind) (("" (apply-extensionality 2 :hide? t) nil nil )) nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil vectors_2D nil )nil vectors_2D_def nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"real" reals nil )"Vector" vectors_2D nil ))nil ))nil 3440245801"" (grind) (("" (apply-extensionality 2 :hide? t) nil nil )) nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil vectors_2D nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"real" reals nil )"Vector" vectors_2D nil ))nil 3440250246"" (skosimp*)"" (grind)"" (apply-extensionality 2 :hide? t)"1" (mult-cases -1) nil nil ) ("2" (mult-cases -2) nil nil ))nil ))nil ))nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )nil reals nil )nil vectors_2D nil ))nil ))nil 3413210572 ("" (grind) nil nil )"(total_order?[real])" nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3413210595 ("" (grind) nil nil )"(strict_total_order?[real])" real_props nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3254160320"" (skosimp*)"" (prop)"1" "(a!1 * v!1)`x = v!1`x AND (a!1 * v!1)`y = v!1`y" )"1" (flatten)"1" (expand "zero" )"1" (expand "*" )"1" (apply-extensionality 2 :hide? t) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (replace -1)"2" (grind) (("2" (apply-extensionality :hide? t) nil nil ))nil ))nil )"3" (replace -1) (("3" (grind) nil nil )) nil ))nil ))nil )"real" reals nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil vectors_2D_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"nonneg_real" sq "reals/" )"real" reals nil ))nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3430754293"" (skeep)"" (rewrite "sqv_sub" )"" (rewrite "sqv_scal" )"" (assert ) (("" (neg-formula 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )nil reals nil )nil vectors_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vector" vectors_2D nil )"nnreal" nil )"nnreal" nil )"real" reals nil )"real" reals nil )"real" reals nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )"real" vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )"odd_int" integers nil )nil vectors_2D nil ))nil 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3255193306"" (skosimp*)"" (lemma "sqrt_square" )"" (inst -1 "sqv(v!1)" ) (("" (rewrite "sqrt_times" ) nil nil ))nil ))nil ))nil )nil sqrt "reals/" )"nnreal" nil )nil sqrt "reals/" )"nnreal" vectors_2D nil )nil real_types nil )nil vectors_2D 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 3254160320"" (skosimp*)"" (expand "norm" )"" (rewrite "sqrt_eq" ) (("" (rewrite "sqv_sym" ) nil nil )) nil ))nil ))nil )"nnreal" vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )nil vectors_2D 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 3254160320 ("" (grind) nil nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"nnreal" vectors_2D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160320"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" ) (("" (grind) nil nil )) nil )) nil ))nil )"nnreal" vectors_2D nil )"real" vectors_2D nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" vectors_2D nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil vectors_2D 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 3403523995 ("" (grind) nil nil )"nnreal" nil )"real" reals nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"nnreal" vectors_2D nil )"nonneg_real" sq "reals/" )"real" reals nil ))nil 3528011984"" (skeep)"" (rewrite "sq_eq" 1 :dir rl) (("" (rewrite "sq_norm" ) nil nil ))nil ))nil )nil sq "reals/" )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 )nil vectors_2D nil )nil real_types nil )"nnreal" vectors_2D nil )nil vectors_2D nil ))nil 3528012044"" (skeep)"" (rewrite "sq_eq" :dir rl) (("" (rewrite "sq_norm" ) nil nil ))nil ))nil )nil sq "reals/" )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 )nil vectors_2D nil )nil real_types nil )"nnreal" vectors_2D nil )nil vectors_2D nil ))nil 3254160320"" (skosimp*) (("" (expand "norm" ) (("" (propax) nil nil )) nil ))nil )"nnreal" vectors_2D nil )) nil ))nil 3425027609"" (skeep)"" (lemma "sq_eq" )"" (inst?)"" (assert )"" (replace -1 * rl)"" (hide -1)"" (rewrite "sq_norm" )"" (rewrite "sq_norm" )"" (expand "sqv" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sq "reals/" )"nnreal" vectors_2D nil )nil vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )nil vectors_2D 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 ))nil 3602098864"" (skeep)"" (rewrite "norms_eq_sqv" )"" (rewrite "sqv_sos" )"" (rewrite "sqv_sos" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil vectors_2D nil )nil reals nil )nil vectors_2D nil )nil vectors_2D nil ))nil ))nil 3475936955"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_le" ) (("" (inst?) nil nil )) nil )) nil ))nil )"nnreal" vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )nil vectors_2D 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 3475936939"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_lt" ) (("" (inst?) nil nil )) nil )) nil ))nil )"nnreal" vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )nil vectors_2D 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 3254160320"" (skosimp*)"" (expand "norm" )"" (rewrite "sqv_scal" )"" (rewrite "sqrt_times" )"" (rewrite "sqrt_sq_abs" ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )nil sqrt "reals/" )nil booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_2D nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sqrt "reals/" )"nnreal" nil )nil vectors_2D 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_2D nil ))nil ))nil 3256053219"" (skeep)"" (rewrite "norm_scal" )"" (expand "abs" ) (("" (grind-reals) nil nil )) nil )) nil ))nil )"posreal" vectors_2D nil )"posreal" nil )nil vectors_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil vectors_2D nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )"{y: posreal | y >= x}" nil )"posreal" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil 3560353108"" (skeep) (("" (typepred "^(nzv)" ) (("" (propax) nil nil )) nil ))nil )"Normalized" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"boolean" notequal nil )"nnreal" vectors_2D nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil vectors_2D nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3255949078"" (skosimp*)"" (expand "^" )"" (assert )"" (rewrite "dot_scal_right" )"" (assert )"" (rewrite "dot_scal_left" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"Normalized" vectors_2D nil )nil vectors_2D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil vectors_2D nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )nil vectors_2D nil )"Nz_vector" vectors_2D nil )"posreal" nil )"posreal" vectors_2D nil )"real" reals nil )"posreal" nil ))nil ))nil 3268401413"" (skosimp*)"" (expand "^" )"" (rewrite "norm_scal" )"" (expand "abs" )"" (case "1 / norm(nzv!1) >= 0" )"1" (assert )"1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"Normalized" vectors_2D nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_props nil )"nnreal" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"Nz_vector" vectors_2D nil )"(total_order?[real])" nil )"Vector" vectors_2D nil )"real" reals nil )"posreal" nil )"{y: posreal | y >= x}" nil )nil vectors_2D nil )"Vector" vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil vectors_2D nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields 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_2D nil )"posreal" nil )"posreal" vectors_2D nil ))nil )nil 3268401324"" (skosimp*)"" (expand "^" )"" (rewrite "norm_scal" ) (("" (postpone) nil nil )) nil )) nil ))nil )nil shostak))nil 3445611572"" (skeep)"" (expand "^" )"" (rewrite "scal_assoc" )"" (grind-reals) (("" (rewrite "scal_1" ) nil nil )) nil ))nil ))nil ))nil )"Normalized" vectors_2D nil )nil real_props nil )nil vectors_2D nil )"Nz_vector" vectors_2D nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil vectors_2D nil )"Vector" vectors_2D nil )"boolean" notequal nil )"nnreal" vectors_2D nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil vectors_2D 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_2D nil )"posreal" nil )"posreal" vectors_2D nil ))nil 3560354232"" (skeep)"" (expand "^" )"" (rewrite "norm_scal" )"" (rewrite "sign_abs" )"" (rewrite "scal_assoc" )"" (rewrite "scal_assoc" )"" (grind-reals)"" "nza / (sign(nza) * norm(nzv) * nza) = sign(nza) / norm(nzv)" )"" (hide 2) (("" (grind :exclude "norm" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"Normalized" vectors_2D nil )nil sign "reals/" )quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.43Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
2026-03-28
