SSL vectors_2D.prf
Interaktion und
(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/" )"(total_order?[real])" nil )"nzreal" nil )"posreal" nil )nil real_props nil )"odd_int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )nil real_props nil )nil real_props nil )"Nz_vector" vectors_2D nil )"nnreal" vectors_2D nil )nil real_types nil )"bool" reals nil )"Sign" sign "reals/" )nil sign "reals/" )"[numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil vectors_2D nil )"nzreal" nil )"posreal" nil )"{y: posreal | y >= x}" nil )"posreal" vectors_2D nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil reals nil )"boolean" notequal 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 3254234016"" (skosimp*)"" (case "sqv(v!1) = 0" )"1" (rewrite "sqv_eq_0" ) (("1" (grind) nil nil )) nil )"2" (case "(FORALL (t:real): sqv(u!1-t*v!1) >= 0)" )"1" (inst -1 "(u!1*v!1)/sqv(v!1)" )"1" (rewrite "sqv_sub_scal" )"1" (name-replace UDOTV "u!1 * v!1" )"1" "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * sq(UDOTV) / sqv(v!1) " )"1" (hide -1)"1" "sq(UDOTV / sqv(v!1)) * sqv(v!1) = sq(UDOTV) / sqv(v!1) " )"1" (hide -1)"1" (assert )"1" "sqv(u!1) + sq(UDOTV) / sqv(v!1) - 2 * sq(UDOTV) / sqv(v!1) = sqv(u!1) - sq(UDOTV) / sqv(v!1)" )"1" (hide -1)"1" (assert )"1" "sqv(v!1)" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide -2 2)"2" (lemma "sqv_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "sq_div" )"2" (expand "sq" 1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide -1 3)"2" (reveal -2)"2" "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * (UDOTV / sqv(v!1)) * (u!1 * v!1)" )"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" expand "sq" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 3) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )nil real_types nil )"bool" reals nil )nil booleans 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 booleans nil )nil numbers nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nonneg_real" sq "reals/" )"nnreal" nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )nil vectors_2D nil )"real" reals nil )"boolean" notequal nil )"Vector" vectors_2D nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nnreal" nil )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )"(total_order?[real])" nil )"odd_int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"real" reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )"Vector" vectors_2D nil ))nil )nil 3254233962"" (skosimp*)"" (case "sqv(v!1) = 0" )"1" (rewrite "sqv_eq_0" ) (("1" (grind) nil )))"2" (case "(FORALL (t:real): sqv(u!1-t*v!1) >= 0)" )"1" (inst -1 "(u!1*v!1)/sqv(v!1)" )"1" (rewrite "sqv_minus_dot" )"1" (name-replace udotv "u!1 * v!1" )"1" "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * sq(UDOTV) / sqv(v!1) " )"1" (hide -1)"1" "sq(UDOTV / sqv(v!1)) * sqv(v!1) = sq(UDOTV) / sqv(v!1) " )"1" (hide -1)"1" (assert )"1" "sqv(u!1) + sq(UDOTV) / sqv(v!1) - 2 * sq(UDOTV) / sqv(v!1) = sqv(u!1) - sq(UDOTV) / sqv(v!1)" )"1" (hide -1)"1" (assert )"1" "sqv(v!1)" )"1" (assert ) nil )))))))"2" (hide -2 2)"2" (lemma "sqv_eq_0" )"2" "2" (assert ) nil )))))))))))))"2" (rewrite "sq_div" )"2" (expand "sq" 1) (("2" (assert ) nil )))))"3" (assert ) nil )))))"2" (assert )"2" (hide -1 3)"2" (reveal -2)"2" "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * (UDOTV / sqv(v!1)) * (u!1 * v!1)" )"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" expand "sq" )"1" (assert ) nil )))))))))"2" (hide -1 2 3)"2" (grind) nil )))))))))))"3" (assert ) nil )))))))"2" (assert ) nil )))"2" (skosimp*) (("2" (assert ) nil ))))))))nil )nil nil )nil 3254160320"" (skosimp*)"" (case "sqv(v!1) = 0" )"1" (rewrite "sqv_eq_0" ) (("1" (grind) nil nil )) nil )"2" (case "(FORALL (t:real): sqv(u!1-t*v!1) >= 0)" )"1" (inst -1 "(u!1*v!1)/sqv(v!1)" )"1" (rewrite "dot_sqv_minus" )"1" (name-replace udotv "u!1 * v!1" )"1" "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * sq(UDOTV) / sqv(v!1) " )"1" (hide -1)"1" "sq(UDOTV / sqv(v!1)) * sqv(v!1) = sq(UDOTV) / sqv(v!1) " )"1" (hide -1)"1" (assert )"1" "sqv(u!1) + sq(UDOTV) / sqv(v!1) - 2 * sq(UDOTV) / sqv(v!1) = sqv(u!1) - sq(UDOTV) / sqv(v!1)" )"1" (hide -1)"1" (assert )"1" "sqv(v!1)" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide -2 2)"2" (lemma "sqv_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "sq_div" )"2" (expand "sq" 1) (("2" (assert ) nil nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (hide -1 3)"2" (reveal -2)"2" "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * (UDOTV / sqv(v!1)) * (u!1 * v!1)" )"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" expand "sq" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 3) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil nil ))nil 3254160320"" (skosimp*)"" (lemma "cauchy_schwarz" )"" (inst?)"" (lemma "sqrt_le" )"" (inst?)"" (assert )"" (hide -2)"" (lemma "sqrt_sq_abs" )"" (inst?)"" (assert )"" (replace -1)"" (hide -1)"" (rewrite "sqrt_times" )"" (expand "norm" )"" expand "abs" )"" "" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )nil sqrt "reals/" )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sqrt "reals/" )"nnreal" vectors_2D nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )"nnreal" vectors_2D nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" vectors_2D nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" nil )nil vectors_2D nil )nil reals nil ))nil ))nil 3445088618"" (skeep)"" (lemma "dot_norm" )"" (inst?)"" (expand "abs" )"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_2D nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" reals nil )"nnreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D nil )nil reals nil )"real" reals nil ))nil 3529243890"" case "FORALL (nzv: Nz_vector, u: Vector): norm(u) = 1 AND norm(nzv) = 1 AND ") "1" (skeep)"1" (case "u = zero" )"1" (inst + "0" )"1" (replace -1)"1" (assert )"1" (hide -)"1" (expand "zero" )"1" (expand "*" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (case "norm(u)>0" )"1" (inst - "1/norm(nzv)*nzv" "1/norm(u)*u" )"1" (assert )"1" (split -)"1" (skeep -1)"1" (inst + "norm(u)*cr/norm(nzv)" )"1" (hide -3)"1" case "norm(u)*(cr * (1 / norm(nzv) * nzv)) = norm(u)*(1/norm(u)*u)" )"1" (assert )"1" (case "norm(u)*(1/norm(u)*u) = u" )"1" (assert )"1" case "norm(u) * (cr * (1 / norm(nzv) * nzv)) = norm(u) * cr / norm(nzv) * nzv" )"1" (assert ) nil nil )"2" "2" "norm" )nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "norm_scal" )"2" (rewrite "abs_div" )"2" (expand "abs" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"3" (rewrite "norm_scal" )"3" (rewrite "abs_div" )"3" (expand "abs" ) (("3" (assert ) nil nil )) nil ))nil ))nil )"4" (rewrite "norm_scal" )"4" (rewrite "norm_scal" )"4" (rewrite "abs_div" )"4" (rewrite "abs_div" )"4" (assert )"4" case "1 / norm(u) * u * (1 / norm(nzv) * nzv) = (1/norm(u))*(1/norm(nzv))*(u*nzv)" )"1" (replace -1)"1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" rewrite "abs_div" )"1" expand "abs" + 1)"1" expand "abs" + 1)"1" expand "abs" + 1)"1" expand "abs" + 1)"1" expand "abs" + 2)"1" expand "abs" + 2)"1" expand "abs" + 2)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "norm_eq_0" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil )"2" (lemma "norm_eq_0" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (name "nzvp" "(# x:=nzv`y,y:=-nzv`x #)" )"2" (case "nzv*nzvp = 0 AND norm(nzvp) = 1" )"1" (flatten)"1" (case "u = (u*nzv)*nzv + (u*nzvp)*nzvp" )"1" (case "sqv(u) = sq(u*nzv) + sq(u*nzvp)" )"1" (case "sq(u*nzv) = sqv(u)*sqv(nzv)" )"1" (replace -1)"1" (case "sqv(u) = 1 AND sqv(nzv) = 1" )"1" (flatten)"1" (replace -1)"1" (replace -2)"1" assert )"1" "sq_eq_0" )"1" "u*nzvp" )"1" assert )"1" replace -1)"1" assert )"1" replace -6 +)"1" "u*nzv" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split +)"1" (rewrite "sqrt_eq" + :dir rl)"1" (rewrite "sqrt_sqv_norm" ) nil nil ))nil )"2" (rewrite "sqrt_eq" + :dir rl)"2" (rewrite "sqrt_sqv_norm" ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "sqrt_eq" 1 :dir rl)"2" (rewrite "sqrt_times" )"2" (rewrite "sqrt_sqv_norm" )"2" (rewrite "sqrt_sqv_norm" )"2" (rewrite "sqrt_sq_abs" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (name "aac" "sqv(u)" )"2" (replace -1)"2" (replace -2 -1)"2" (replace -1 :dir rl)"2" (hide -1)"2" case "sqv(nzvp) = 1 AND sqv(nzv) = 1" )"1" "1" "sq(u*nzvp)" )"1" "sq(u*nzv)" )"1" "(u*nzv)*(u*nzvp)" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1" rewrite "sqrt_eq" 1 :dir rl)"1" rewrite "sqrt_sqv_norm" )nil nil ))nil )"2" rewrite "sqrt_eq" 1 :dir rl)"2" rewrite "sqrt_sqv_norm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT FORALL (e1, e2, w: Vect2): AND e2 /= zero AND e1*e2=0 IMPLIES") "1" (hide-all-but 1)"1" (skosimp*)"1" (lemma "posreal_times_posreal_is_posreal" )"1" (inst - "sqv(e1!1)" "sqv(e2!1)" )"1" case "sqv(e1!1)*sqv(e2!1)*w!1 = (w!1*e1!1*sqv(e2!1))*e1!1 + (w!1*e2!1*sqv(e1!1))*e2!1" )"1" (decompose-equality 3)"1" "sqv(e1!1)*sqv(e2!1)" )"1" (grind :exclude "sqv" ) nil nil ))nil )"2" "sqv(e1!1)*sqv(e2!1)" )"2" (grind :exclude "sqv" ) nil nil ))nil ))nil )"2" (hide 4) (("2" (grind) nil nil ))nil ))nil )"2" (hide 4)"2" (lemma "sqv_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" (lemma "sqv_eq_0" )"3" (inst?) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "nzv" "nzvp" "u" )"2" (assert )"2" (split -)"1" (case "sqv(nzv) = 1 AND sqv(nzvp) =1 " )"1" (flatten)"1" (replaces -1)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" (split +)"1" (rewrite "sqrt_eq" 1 :dir rl)"1" (rewrite "sqrt_sqv_norm" ) nil nil ))nil )"2" (rewrite "sqrt_eq" 1 :dir rl)"2" (rewrite "sqrt_sqv_norm" ) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1)"2" (assert )"2" "2" expand "zero" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (skeep)"3" (lemma "sqv_eq_0" )"3" (inst?) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"4" (hide-all-but 1)"4" (skeep)"4" (lemma "sqv_eq_0" )"4" (inst?) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (split +)"1" (hide-all-but 1)"1" (expand "nzvp" ) (("1" (grind) nil nil )) nil ))nil )"2" (hide-all-but (-3 1))"2" (expand "nzvp" ) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"[# x: real, y: real #]" vectors_2D nil )NOT const-decl "[bool -> bool]" booleans nil )nil vectors_2D_def nil )"Vect2" vectors_2D nil )"Vect2" vectors_2D nil )nil real_types nil )nil real_props nil )nil vectors_2D nil )nil real_types nil )nil sqrt "reals/" )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil sqrt "reals/" )nil vectors_2D nil )nil sqrt "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )"posreal" nil )nil extra_real_props nil )"Vector" vectors_2D nil )"bool" reals nil )nil vectors_2D nil )"(strict_total_order?[real])" real_props nil )"posreal" sqrt "reals/" )"posreal" vectors_2D nil )nil real_props nil )"nzreal" nil )"posreal" nil )nil vectors_2D nil )"{y: posreal | y >= x}" nil )"{j: posint | j >= i}" nil )"{j: nonneg_int | j >= i}" nil )"{r: posrat | r >= q}" nil )nil real_props nil )nil reals nil )"real" reals nil )"nnreal" vectors_2D nil )"real" reals nil )"real" reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"Vector" vectors_2D nil )"posreal" nil )"Nz_vector" vectors_2D nil )"nzreal" nil )"posreal" vectors_2D nil )"nnreal" nil )nil reals nil )nil vectors_2D nil )nil booleans nil )"boolean" notequal nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_2D nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" vectors_2D nil )"Vector" vectors_2D nil ))nil 3445157327"" (skeep)"" (lemma "sq_le" )"" (inst?)"" (assert )"" (hide 2)"" (rewrite "sqv_add" )"" (rewrite "sq_plus" )"" (move-terms 1 r (1 2))"" (case "u*v <= sqrt(sqv(u)) * sqrt(sqv(v))" )"1" (assert )"1" (rewrite "dot_scal_left" )"1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (lemma "schwarz" )"2" (inst?)"2" (expand "norm" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sq "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil vectors_2D nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"nnreal" vectors_2D nil )nil vectors_2D nil )"real" reals nil )nil vectors_2D nil )"nnreal" nil )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors_2D nil )"nnreal" vectors_2D nil )nil vectors_2D 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 )"nnreal" nil ))nil )nil 3445156310"" (skeep)"" (auto-rewrite "dot_zero_left" )"" (auto-rewrite "dot_zero_right" )"" (auto-rewrite "scal_zero" )"" (case-replace "sqv(u + v) = u*u + 2*u*v + v*v" )"1" (hide -1)"1" case "u * u + 2 * u * v + v * v <= u * u + 2 * norm(u) * norm(v) + v * v" )"1" (case-replace "u = zero" )"1" (assert ) nil nil )"2" (case-replace "v = zero" )"1" (assert ) nil nil )"2" (lemma "sqv_eq_0" )"2" (inst?)"2" (assert )"2" (lemma "sqv_eq_0" )"2" (inst - "u" )"2" assert )"2" "u * u + 2 * norm(u) * norm(v) + v * v = sq(sqrt(u * u) + sqrt(v * v))" )"1" "1" "sqrt_le" )"1" "1" rewrite "sqrt_sq" )"1" (assert ) nil nil ))nil )"2" assert )"2" rewrite "sqv_rew" )"2" "sqv_eq_0" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" rewrite "sqv_rew" )"3" (assert ) nil nil ))nil )"4" "2 * u * v + u*u + v * v = sqv(u+v)" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" rewrite "sq_plus" )"1" rewrite "sq_sqrt" )"1" rewrite "sq_sqrt" )"1" expand "norm" )"1" assert )"1" expand "sqv" )"1" nil nil ))nil ))nil ))nil )"2" "v = zero" )"1" (assert ) nil nil )"2" assert )"2" rewrite "sqv_rew" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "sqv_rew" )"2" (assert ) nil nil ))nil ))nil )"2" rewrite "sqv_rew" )"2" (assert ) nil nil ))nil )"3" rewrite "sqv_rew" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" rewrite "sqv_rew" )"3" (assert ) nil nil ))nil )"4" rewrite "sqv_rew" )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (assert )"2" (lemma "dot_norm" )"2" (inst - "u" "v" )"2" (flatten)"2" (assert )"2" (mult-by -2 "2" )"2" assert )"2" case "2 * (u * v) = 2 * u * v" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )"nonneg_real" sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sqrt "reals/" ))nil ))nil 3445157224"" (skeep)"" (rewrite "sqrt_sqv_norm" :dir rl)"" (rewrite "sqrt_sqv_norm" :dir rl)"" (rewrite "sqrt_sqv_norm" :dir rl)"" (rewrite "sqv_sq" )"" (rewrite "sqv_sq" )"" (rewrite "sqv_sq" )"" (expand "-" )"" "sq(u`x - w`x) = sq(u`x - v`x + v`x - w`x)" )"1" (hide -1)"1" "sq(u`y - w`y) = sq(u`y - v`y + v`y - w`y)" )"1" (hide -1)"1" (lemma "schwarz_cor" )"1" (inst - "u-v" "v-w" )"1" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )nil reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )"real" reals 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 )"nonneg_real" sq "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )"Vector" vectors_2D nil )"real" vectors_2D nil )"nnreal" vectors_2D nil )"nnreal" nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil ))nil )nil 3445104261"" (skeep)"" (rewrite "sqrt_sqv_norm" :dir rl)"" (rewrite "sqrt_sqv_norm" :dir rl)"" (rewrite "sqrt_sqv_norm" :dir rl)"" (rewrite "sqv_sq" )"" (rewrite "sqv_sq" )"" (rewrite "sqv_sq" )"" (expand "-" )"" "sq(u`x - w`x) = sq(u`x - v`x + v`x - w`x)" )"1" (hide -1)"1" "sq(u`y - w`y) = sq(u`y - v`y + v`y - w`y)" )"1" (hide -1)"1" (lemma "schwarz_corollary" )"1" (inst - "u-v" "v-w" )"1" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_real" sq "reals/" )) nil )nil 3445104189"" (skeep) (("" (postpone) nil nil )) nil ) nil shostak))nil 3255192386"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_le" )"" "sqv(u!1 + v!1)" "sq(sqrt(sqv(u!1)) + sqrt(sqv(v!1)))" )"" (rewrite "sqrt_sq" )"" (assert )"" (hide 2)"" (rewrite "sqv_add" )"" (expand "sq" )"" (rewrite "sqrt_sqv_sq" )"" (rewrite "sqrt_sqv_sq" )"" (rewrite "sqrt_sqv_norm" )"" (rewrite "sqrt_sqv_norm" )"" (lemma "dot_norm" )"" "u!1" "v!1" )"" "" rewrite "dot_scal_left" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )"nnreal" 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 )nil vectors_2D nil )nil real_types nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )"nonneg_real" sq "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"(total_order?[real])" nil )nil vectors_2D nil )"real" reals nil )nil vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"real" reals nil )"real" reals nil )nil vectors_2D nil )"nnreal" nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil sqrt "reals/" ))nil )nil 3255191805"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_le" )"" "sqv(u!1 + v!1)" "sq(sqrt(sqv(u!1)) + sqrt(sqv(v!1)))" )"" (assert )"" (rewrite "sqv_add" )"" (expand "sq" )"" (assert )"" (lemma "sqrt_times" )"" (inst?)"" (hide -1)"" (rewrite "sqrt_sqv_norm" )"" (rewrite "sqrt_sqv_norm" )"" (lemma "dot_norm" )"" "" "" assert )"" "vectors_2D" )"" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3254160320"" (skosimp*)"" (expand "norm" )"" (lemma "sq_le" )"" (inst?)"" (assert )"" (hide 2)"" (rewrite "sq_sqrt" )"" (expand "sq" )"" (rewrite "sq_rew" )"" (rewrite "sq_rew" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (rewrite "sqv_sub" )"" (assert )"" rewrite "sqrt_sqv_norm" )"" rewrite "sqrt_sqv_norm" )"" assert )"" "dot_norm" )"" "-u!1" "v!1" )"" "" rewrite "norm_neg" )"" rewrite "dot_neg_left" )"" "2" )"" assert )"" "" rewrite "dot_scal_left" )"" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )"nnreal" 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 )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil vectors_2D nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil sq "reals/" )nil vectors_2D nil )"real" reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )"real" reals nil )nil extra_real_propsnil )"[numfield -> numfield]" number_fields nil )"real" vectors_2D nil )nil vectors_2D nil )"real" reals nil )nil vectors_2D nil )nil vectors_2D nil )"nonneg_real" sq "reals/" )"nnreal" nil )nil sqrt "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sq "reals/" ))nil ))nil 3255265184"" (skosimp*)"" (lemma "norm_add_le" )"" (inst -1 "u!1-v!1" "v!1" )"" (assert )"" (rewrite "add_cancel2" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil )"(total_order?[real])" nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )nil reals nil ))nil )nil 3255193133"" (skosimp*)"" (lemma "norm_add_le" )"" (inst -1 "u!1-v!1" "v!1" )"" (assert )"" (auto-rewrite-theory "vectors_2D" )"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil nil ))nil 3256553970"" (skosimp*)"" (prop)"1" (expand "norm" )"1" (expand "sqv" )"1" (expand "*" )"1" "sqrt(u!1`x * u!1`x + u!1`y * u!1`y) >= sqrt(u!1`x * u!1`x)" )"1" (rewrite "sq_rew" )"1" (rewrite "sqrt_sq_abs" ) nil nil )) nil )"2" (hide 2) (("2" (rewrite "sqrt_ge" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "norm" )"2" (expand "sqv" )"2" (expand "*" )"2" "sqrt(u!1`x * u!1`x + u!1`y * u!1`y) >= sqrt(u!1`y * u!1`y)" )"1" (rewrite "sq_rew" )"1" (rewrite "sq_rew" )"1" (rewrite "sqrt_sq_abs" ) nil nil )) nil ))nil )"2" (hide 2) (("2" (rewrite "sqrt_ge" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors_2D nil )"(total_order?[real])" nil )"real" reals 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 )nil real_types nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D nil )nil sqrt "reals/" )nil sq "reals/" )nil sqrt "reals/" )"real" vectors_2D nil )"real" reals nil )"nnreal" vectors_2D nil ))nil 3256550488"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"nnreal" nil )"nnreal" vectors_2D nil )"odd_int" integers nil )"real" vectors_2D nil )"Vector" vectors_2D nil )"real" reals nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )nil vectors_2D_def nil )"Vector" vectors_2D 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 3430578246"" (skeep)"" (expand "parallel?" )"" (inst 1 "1" ) (("" (rewrite "scal_1" ) nil nil )) nil )) nil ))nil )"bool" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3430578570"" (skeep)"" (expand "parallel?" )"" (split)"1" (flatten)"1" (skeep -1)"1" (inst 1 "1/nzk" )"1" (lemma "scal_cross" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (skeep -1)"2" (inst 1 "1/nzk" )"2" (lemma "scal_cross" )"2" (inst? -1) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vectors_2D nil )"nzreal" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil vectors_2D nil )nil vectors_2D nil ))nil 3430579137"" (skeep)"" (expand "parallel?" )"" (skolem -1 "k1" )"" (skolem -2 "k2" )"" (replaces -1)"" (replaces -2)"" (replaces -1)"" (inst 1 "k1*k2" )"" (rewrite "scal_assoc" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vectors_2D nil )nil vectors_2D nil )nil vectors_2D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nzreal" nil ))nil 3430579523"" (skeep)"" (expand "parallel?" )"" (split)"1" (flatten)"1" (skeep -1) (("1" (rewrite "scal_zero" ) nil nil )) nil ))nil )"2" (flatten)"2" (replaces -1) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" vectors_2D nil )"Vector" vectors_2D nil )"Vector" 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 )"boolean" notequal nil )nil reals nil ))nil 3430577698"" (skeep)"" (expand * "parallel?" "dir_parallel?" )"" (skeep -1) (("" (inst 1 "pk" ) nil nil )) nil )) nil ))nil )"bool" vectors_2D nil )"bool" 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 )"boolean" notequal nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil 3447773168"" (skeep)"" (expand "orthogonal?" )"" (rewrite "sqv_add" )"" (assert )"" (rewrite "dot_scal_left" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" 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 vectors_2D nil )"real" reals nil )"nnreal" nil )nil vectors_2D nil )nil reals nil )nil vectors_2D nil ))nil 3447773735"" (skeep)"" (both-sides-f 1 "sq" )"1" (rewrite "sq_norm" )"1" (rewrite "sq_norm" )"1" (rewrite "pythagorean" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (rewrite "sq_ge" ) nil nil ))nil ))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 )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )nil vectors_2D nil )nil real_types nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"nnreal" nil )nil vectors_2D nil )nil vectors_2D nil )nil sq "reals/" ))nil 3447773741"" (skeep)"" (rewrite "add_comm" )"" (rewrite "norm_add_ge_left" )"" (expand "orthogonal?" ) (("" (rewrite "dot_comm" ) nil nil ))nil ))nil ))nil ))nil )nil vectors_2D nil )nil reals nil )nil vectors_2D nil )"bool" vectors_2D nil )nil vectors_2D nil )"(total_order?[real])" nil )nil vectors_2D nil ))nil 3601218451"" case "FORALL (M: posnat, RS: [nat -> real]): AND ") "1" (skeep)"1" (inst-cp - "M" "LAMBDA (i:nat): VS(i)`x" )"1" (split -)"1" (skeep)"1" (inst -3 "M" "LAMBDA (i:nat): VS(ns(i))`y" )"1" (split -)"1" (skolem - ("nnss" "acpry" ))"1" (name "acp" "(# x:=acpr,y:=acpry #)" )"1" "ns o " " acp") "1" (expand "o" +)"1" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (skeep)"1" "j" )"1" "nnss(j)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replaces -1)"2" (flatten)"2" case "NOT %1" ) (! 1 1))"1" "1" "1" "epsil/2" )"1" "epsil/2" )"1" "1" "max(K!1,K!2)+1" )"1" "1" "j" )"1" "nnss(j)" )"1" assert )"1" "j" )"1" assert )"1" "W" "VS(ns(nnss(j)))" )"1" replace "1" assert )"1" "Ax" "(# x:= W`x-acpr,y:=0 #)" )"1" "Ay" "(# x:=0,y:=W`y-acpry #)" )"1" case "NOT W-acp = Ax+Ay" )"1" "1" expand "Ax" )"1" expand "Ay" )"1" expand "-" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "norm_add_le" )"2" "2" case "norm(Ax)<epsil/2 AND norm(Ay)<epsil/2" )"1" nil nil )"2" "2" "1" case "norm(Ax) = abs(W`x-acpr)" )"1" assert )nil nil )"2" "2" rewrite "sq_eq" "2" rewrite "sq_norm" )"2" expand "Ax" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "norm(Ay) = abs(W`y-acpry)" )"1" assert )nil nil )"2" "2" rewrite "sq_eq" "2" rewrite "sq_norm" )"2" expand "Ay" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "norm(acp)-M" )"1" "1" "K!1" )"1" assert )"1" "ns(nnss(K!1))" )"1" "W" "VS(ns(nnss(K!1)))" )"1" replace -1)"1" "1" "norm_neg" )"1" "W-acp" )"1" case "-(W-acp) = acp-W" )"1" "1" assert )"1" "1" "norm_add_le" )"1" "acp-W" "W" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst -3 "ns(i!1)" )"2" (name "W" "VS(ns(i!1))" )"2" (replace -1)"2" (hide (-1 -2 -3))"2" (rewrite "sq_le" 1 :dir rl)"2" rewrite "sq_le" -1 :dir rl)"2" rewrite "sq_norm" )"2" expand "sqv" )"2" expand "*" )"2" "sq(W`y)" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (skosimp*)"2" (inst - "i!1" )"2" (rewrite "sq_le" 1 :dir rl)"2" (rewrite "sq_le" -1 :dir rl)"2" (rewrite "sq_norm" )"2" (typepred "sq(VS(i!1)`x)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" case "EXISTS (acpr:real): FORALL (epsil:posreal,K:nat): EXISTS (j:nat): j>=K AND abs(RS(j)-acpr)<epsil" )"1" (skeep -1)"1" "ns" "LAMBDA (i:nat): choose({j:nat | j>i+2 AND abs(RS(j)-acpr)<1/(i+2)})" )"1" (inst + "ns" "acpr" )"1" (split)"1" (skeep) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (lemma "archimedean" )"2" (inst - "epsil" )"2" (skeep)"2" (inst + "n+1" )"2" (skeep)"2" "ns(j)" )"2" case "1/(2+j) <1/n" )"1" (assert ) nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (inst - "1/(2+i)" "8+i" )"2" (skeep)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "j" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "S" "LAMBDA (x:real): EXISTS (K:nat): FORALL (i:nat): i>=K IMPLIES RS(i)>=x" )"2" (case "nonempty?[real](S) AND bounded_above?(S)" )"1" (flatten)"1" (name "acpr" "lub(S)" )"1" (typepred "acpr" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" (inst + "acpr" )"1" (skeep)"1" case "S(acpr-epsil/2)" )"1" expand "upper_bound?" -2)"1" "acpr + epsil/2" )"1" (assert ) nil nil )"2" expand "S" -1)"2" "K1" )"2" expand "S" 1)"2" "K + K1 + 1" )"2" "2" "i" )"2" "i" )"2" assert )"2" expand "abs" +)"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "S" 1)"2" "acpr-epsil/2" )"2" assert )"2" expand "upper_bound?" +)"2" "2" "s" )"2" expand "S" -1)"2" "2" "K!1" )"2" "2" "i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (hide 2)"2" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (expand "member" )"1" (inst - "-M-1" )"1" (expand "S" 1)"1" "0" )"1" "1" "i" )"1" expand "abs" )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bounded_above?" )"2" (inst + "M+1" )"2" (expand "upper_bound?" )"2" (skeep)"2" (typepred "s" )"2" expand "S" )"2" "2" "K!1" )"2" "K!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )"posrat" nil )set type-eq-decl nil sets nil )"bool" sets nil )"(p)" sets nil )nil real_props nil )nil real_props nil )nil reals nil )nil real_props nil )"(divides(m))" divides nil )nil real_props nil )"bool" sets nil )"bool" sets nil )"nzint" integers nil )"int" integers nil )"bool" bounded_real_defs nil )"nonneg_int" nil )"{x | least_upper_bound?(x, S)}" vectors_2Dnil )"posreal" vectors_2D nil )"[real -> boolean]" vectors_2D nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )nil sq "reals/" )"posreal" sq "reals/" )"(divides(n))" divides nil )"posint" nil )"T3" function_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil vectors_2D nil )"Vector" vectors_2D nil )nil vectors_2D nil )"posnat" vectors_2D nil )"[# x: real, y: real #]" vectors_2D nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil sq "reals/" )nil sq "reals/" )"real" vectors_2D nil )"nnreal" vectors_2D nil )"nonneg_real" sq "reals/" )"real" reals nil )"posreal" vectors_2D nil )nil vectors_2D nil )"nnreal" nil )"(total_order?[real])" nil )nil vectors_2D nil )"[# x: naturalnumber, y: real #]" vectors_2Dnil )"real" reals nil )"[# x: real, y: naturalnumber #]" vectors_2Dnil )"Vector" vectors_2D nil )nil naturalnumbers nil )"{k: posint | i <= k AND j <= k}" nil )"{s: posrat | s >= q AND s >= r}" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"posint" nil )nil vectors_2D nil )nil real_types nil )"nnreal" vectors_2D nil )"Vector" vectors_2D nil )"[T, T -> boolean]" equalities nil )nil vectors_2D_def nil )"real" reals 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 integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )nil 3601213760"" case "FORALL (M: posnat, RS: [nat -> real]): AND ") "1" (skeep)"1" (inst-cp - "M" "LAMBDA (i:nat): VS(i)`x" )"1" (split -)"1" (skeep)"1" (inst -3 "M" "LAMBDA (i:nat): VS(ns(i))`y" )"1" (split -)"1" (skolem - ("nnss" "acpry" ))"1" (name "acp" "(# x:=acpr,y:=acpry #)" )"1" "ns o " " acp") "1" (expand "o" +)"1" (invoke (case "NOT %1" ) (! 1 1))"1" (hide 2)"1" (skeep)"1" "j" )"1" "nnss(j)" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replaces -1)"2" (flatten)"2" case "NOT %1" ) (! 1 1))"1" "1" "1" "epsil/2" )"1" "epsil/2" )"1" "1" "max(K!1,K!2)+1" )"1" "1" "j" )"1" "nnss(j)" )"1" assert )"1" "j" )"1" assert )"1" "W" "VS(ns(nnss(j)))" )"1" replace "1" assert )"1" "Ax" "(# x:= W`x-acpr,y:=0 #)" )"1" "Ay" "(# x:=0,y:=W`y-acpry #)" )"1" case "NOT W-acp = Ax+Ay" )"1" "1" expand "Ax" )"1" expand "Ay" )"1" expand "-" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "norm_add_le" )"2" "2" case "norm(Ax)<epsil/2 AND norm(Ay)<epsil/2" )"1" nil nil )"2" "2" "1" case "norm(Ax) = abs(W`x-acpr)" )"1" assert )nil nil )"2" "2" rewrite "sq_eq" "2" rewrite "sq_norm" )"2" expand "Ax" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "norm(Ay) = abs(W`y-acpry)" )"1" assert )nil nil )"2" "2" rewrite "sq_eq" "2" rewrite "sq_norm" )"2" expand "Ay" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "norm(acp)-M" )"1" "1" "K!1" )"1" assert )"1" "ns(nnss(K!1))" )"1" "W" "VS(ns(nnss(K!1)))" )"1" replace -1)"1" "1" "norm_neg" )"1" "W-acp" )"1" case "-(W-acp) = acp-W" )"1" "1" assert )"1" "1" "norm_add_le" )"1" "acp-W" "W" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst -3 "ns(i!1)" )"2" (name "W" "VS(ns(i!1))" )"2" (replace -1)"2" (hide (-1 -2 -3))"2" (rewrite "sq_le" 1 :dir rl)"2" rewrite "sq_le" -1 :dir rl)"2" rewrite "sq_norm" )"2" expand "sqv" )"2" expand "*" )"2" "sq(W`y)" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (skosimp*)"2" (inst - "i!1" )"2" (rewrite "sq_le" 1 :dir rl)"2" (rewrite "sq_le" -1 :dir rl)"2" (rewrite "sq_norm" )"2" (typepred "sq(VS(i!1)`x)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" case "EXISTS (acpr:real): FORALL (epsil:posreal,K:nat): EXISTS (j:nat): j>=K AND abs(RS(j)-acpr)<epsil" )"1" (skeep -1)"1" "ns" "LAMBDA (i:nat): choose({j:nat | j>i+2 AND abs(RS(j)-acpr)<1/(i+2)})" )"1" (inst + "ns" "acpr" )"1" (split)"1" (skeep) (("1" (assert ) nil nil )) nil )"2" (skeep)"2" (lemma "archimedean" )"2" (inst - "epsil" )"2" (skeep)"2" (inst + "n+1" )"2" (skeep)"2" "ns(j)" )"2" case "1/(2+j) <1/n" )"1" (assert ) nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (inst - "1/(2+i)" "8+i" )"2" (skeep)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst - "j" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "S" "LAMBDA (x:real): EXISTS (K:nat): FORALL (i:nat): i>=K IMPLIES RS(i)>x" )"2" (case "nonempty?[real](S) AND bounded_above?(S)" )"1" (flatten)"1" (name "acpr" "lub(S)" )"1" (typepred "acpr" )"1" (expand "least_upper_bound?" )"1" (flatten)"1" (inst + "acpr" )"1" (skeep)"1" case "S(acpr-epsil/2)" )"1" expand "upper_bound?" -2)"1" "acpr + epsil/2" )"1" (assert ) nil nil )"2" expand "S" -1)"2" "K1" )"2" expand "S" 1)"2" "K + K1 + 1" )"2" "2" "i" )"2" "i" )"2" assert )"2" expand "abs" +)"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.147 Sekunden
(vorverarbeitet am 2026-04-25)
¤ *© Formatika GbR, Deutschland
2026-05-26
