(vectors_4Dnil 3254160430 ("" (subtype-tcc) nil nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil ))nil ))nil 3440239065"" (skosimp*) (("" (expand "sqv" ) (("" (propax) nil nil )) nil ))nil )"nnreal" vectors_4D nil )) shostak))nil 3602099496 ("" (grind) nil nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"nonneg_real" sq "reals/" )"nnreal" vectors_4D nil )"real" reals nil )"real" reals nil ))nil 3428691906 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430"" (skosimp*) (("" (grind) nil nil )) nil )"real" reals nil )"Vector" vectors_4D nil ))nil ))nil 3601899372 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3601899381 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3256995696 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3256995701 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3256995705 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3601899392 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3467129827 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3467129831 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3467129838 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3601899404 ("" (grind) nil nil )"Vector" vectors_4D nil )) shostak))nil 3268401977"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3268401982"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3268401986"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3601899414 ("" (grind) nil nil ) nil shostak))nil 3440253202"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil reals nil )nil vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3601899453"" (assert ) (("" (expand "zero" ) (("" (propax) nil nil )) nil )) nil )"Vector" vectors_4D nil )) shostak))nil 3428691657"" (skeep)"" (expand "norm" )"" (split)"1" (flatten)"1" (lemma "sqrt_eq_0" )"1" (inst -1 "sqv(v)" )"1" (split -1)"1" (hide -2)"1" (rewrite "sqv_sos" )"1" (expand "sos" )"1" case "sq(v`x)=0 AND sq(v`y)=0 AND sq(v`z)=0" )"1" (flatten)"1" (rewrite "sq_eq_0" )"1" (rewrite "sq_eq_0" )"1" rewrite "sq_eq_0" )"1" assert )"1" replace -1)"1" "1" replace -1)"1" "1" replace -1)"1" "1" assert )"1" rewrite "sq_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil 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_4D nil )nil sqrt "reals/" )"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_4D nil )nil real_types nil )"nnreal" vectors_4D nil )"nnreal" vectors_4D nil )nil sq "reals/" )"nnreal" nil )nil sq "reals/" )"nonneg_real" sq "reals/" )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil vectors_4D nil )nil sqrt "reals/" ))nil )nil 3428691598 ("" (postpone) nil nil ) nil shostak))nil 3428692149"" (skeep)"" (expand "norm" )"" (ground) (("" (replaces -1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors_4D nil )nil sqrt "reals/" ))nil )nil 3428692119 ("" (postpone) nil nil ) nil shostak))nil 3430054265"" (skosimp*)"" (lemma "norm_xyz_eq_0" )"" (inst?)"" (replaces -1)"" (grind) (("" (decompose-equality) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_4D nil )"Vector" vectors_4D nil )nil vectors_4D nil )nil reals nil ))nil ))nil 3428692193 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )nil sqrt "reals/" )"nnreal" vectors_4D nil ))nil )nil 3254160430"" (skosimp*)"" (expand "norm" )"" (prop)"1" (lemma "sqv_eq_0" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (replace -1)"2" (assert )"2" (rewrite "sqv_zero" )"2" (rewrite "sqrt_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sqrt "reals/" )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil ))nil ))nil 3428692246"" (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_4D nil )nil vectors_4D nil )nil vectors_4D nil )nil reals nil ))nil )nil 3254161197"" (grind)"" (apply-extensionality :hide? t)"1" (case-replace "v!1`x * v!1`x = 0" )"1" (mult-cases -1) nil nil )"2" (assert )"2" (rewrite "sq_rew" ) (("2" (assert ) nil nil )) nil )) nil ))nil )"2" (case "v!1`y * v!1`y = 0" )"1" (mult-cases -1) nil nil )"2" (rewrite "sq_rew" )"2" (assert )"2" (rewrite "sq_rew" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (case "v!1`z * v!1`z = 0" )"1" (mult-cases -1) nil nil )"2" (rewrite "sq_rew" )"2" (rewrite "sq_rew" )"2" (rewrite "sq_rew" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil sq "reals/" )) nil )nil 3254160430"" (grind)"" (apply-extensionality :hide? t)"1" (case-replace "v!1`x * v!1`x = 0" )"1" (mult-cases -1) nil nil ) ("2" (assert ) nil nil )) nil )"2" (case "v!1`y * v!1`y = 0" )"1" (mult-cases -1) nil nil ) ("2" (assert ) nil nil )) nil )"3" (case "v!1`z * v!1`z = 0" )"1" (mult-cases -1) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )nil nil ))nil 3428692303"" (skeep)"" (lemma "sqv_eq_0" ) (("" (inst?) (("" (ground) nil nil )) nil ))nil ))nil )nil vectors_4D nil )"(strict_total_order?[real])" real_props nil )nil vectors_4D nil )nil reals nil ))nil ))nil 3428790496"" (skeep)"" (lemma "norm_eq_0" )"" (inst?)"" (replaces -1 :dir rl)"" (case-replace "norm(v)=0 IFF sq(norm(v))=0" )"1" (hide -1)"1" (expand "norm" )"1" (rewrite "sq_sqrt" )"1" (expand "sqv" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "sq_eq_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors_4D nil )nil sq "reals/" )"nnreal" vectors_4D nil )nil sqrt "reals/" )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_4D nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil vectors_4D nil )nil reals nil ))nil ))nil 3430825265"" (skeep)"" (expand "nz_vector?" )"" (lemma "norm_eq_0" )"" (inst?)"" (lemma "norm_xyz_eq_0" )"" (inst?) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil vectors_4D nil )nil vectors_4D nil )nil vectors_4D nil )nil reals nil ))nil 3430825820"" (skeep :preds? t)"" (expand "nz_vector?" )"" (flatten)"" (lemma "norm_eq_0" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors_4D nil )"(strict_total_order?[real])" real_props nil )nil vectors_4D nil )"Vector" vectors_4D nil )"boolean" notequal nil )nil booleans nil )nil vectors_4D nil )nil reals nil ))nil )nil 3430825615 ("" (judgement-tcc) nil nil ) nil nil ))nil 3430825847"" (skeep :preds? t)"" (lemma "v_neq_zero" )"" (inst?)"" (expand "nz_vector?" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil vectors_4D nil )"(strict_total_order?[real])" real_props nil )nil vectors_4D nil )"Vector" vectors_4D nil )"boolean" notequal nil )nil booleans nil )nil vectors_4D nil )nil reals nil ))nil )nil 3430825615 ("" (judgement-tcc) nil nil ) nil nil ))nil 3430825615 ("" (judgement-tcc) nil nil )"Vector" vectors_4D nil )) nil ))nil 3430825615 ("" (judgement-tcc) nil nil )"Vector" vectors_4D nil )) nil ))nil 3430825615 ("" (judgement-tcc) nil nil )"Vector" vectors_4D nil )) nil ))nil 3601898781 ("" (judgement-tcc) nil nil )"Vector" vectors_4D nil )) nil ))nil 3430825870"" (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_4D 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_4D nil )nil vectors_4D nil )nil vectors_4D nil ))nil )nil 3430825615 ("" (judgement-tcc) nil nil ) nil nil ))nil 3431076656"" (judgement-tcc) (("" (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_4D nil )"boolean" notequal nil )nil vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3431179259"" (grind)"" (decompose-equality 2)"1" (grind-reals) nil nil ) ("2" (grind-reals) nil nil )"3" (grind-reals) nil nil ) ("4" (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_4D nil )nil vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3462009607 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil 3254160430"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )nil vectors_4D_def nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )nil vectors_4D_def nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )) nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" reals nil ))nil ))nil 3430827215"" (grind)"1" (decompose-equality 1) nil nil )"2" (decompose-equality 1) nil nil ))nil )nil vectors_4D_def nil )nil reals nil )nil vectors_4D nil )"[numfield, 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_4D nil )"Vector" vectors_4D nil ))nil 3254160430"" (grind)"1" (decompose-equality 1) nil nil )"2" (decompose-equality 1) nil nil ))nil )nil vectors_4D_def nil )nil reals nil )nil vectors_4D nil )"[numfield, 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_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430"" (grind)"1" (apply-extensionality :hide? t) nil nil )"2" (apply-extensionality :hide? t) nil nil ))nil )nil vectors_4D nil )nil reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil ))nil 3254160430"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )nil vectors_4D_def nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430"" (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_4D nil )"[numfield -> numfield]" number_fields nil )nil vectors_4D_def nil )nil reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3255193987"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )nil vectors_4D_def nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil 3255193996"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )nil vectors_4D_def nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil 3430825960"" (grind) (("" (decompose-equality 1) nil nil )) nil )nil vectors_4D nil )nil reals nil )"Vector" vectors_4D nil ))nil 3430825974"" (grind) (("" (decompose-equality 1) nil nil )) nil )nil vectors_4D nil )nil reals nil )"Vector" vectors_4D nil ))nil 3467130099"" (grind) (("" (decompose-equality 1) nil nil )) nil )nil reals nil )nil vectors_4D 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_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil 3467130122"" (grind)"1" (decompose-equality 1) nil nil )"2" (decompose-equality 1) nil nil ))nil )nil vectors_4D_def nil )nil reals nil )nil vectors_4D 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_4D nil ))nil 3430825987"" (skeep) (("" (grind) (("" (decompose-equality 1) nil nil )) nil ))nil )"Vector" vectors_4D nil )"real" reals nil )"real" reals nil )nil vectors_4D nil )nil reals nil ))nil 3430825992"" (skeep) (("" (grind) (("" (decompose-equality 1) nil nil )) nil ))nil )"Vector" vectors_4D nil )"real" reals nil )nil reals nil )nil vectors_4D nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )nil vectors_4D_def nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors_4D nil )nil reals nil )"real" reals nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil ))nil 3254160430"" (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_4D nil )nil reals nil )nil vectors_4D_def nil )"real" reals nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3429977975 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil )"Vector" vectors_4D nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil ))nil ))nil 3440244963 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3440244967 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3268401998"" (grind) (("" (apply-extensionality 2 :hide? t) nil nil )) nil )nil vectors_4D 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 )"Vector" vectors_4D nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3440245220 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil ))nil 3440245228 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3256986195 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil ))nil 3254656778 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil ))nil 3254656147 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3254656151 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3430826304 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3430826316 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil ))nil 3430826379"" (skeep)"" (split)"1" (flatten)"1" (replaces -1 :dir rl)"1" (decompose-equality 1)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ) ("4" (grind) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (replaces -1)"2" (decompose-equality 1)"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil nil ) ("4" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil reals nil )nil vectors_4D nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )"Vector" vectors_4D nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nzreal" nil ))nil )nil 3430826355"" (grind) (("1" (postpone) nil nil ) ("2" (postpone) nil nil )) nil )nil shostak))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3430826453"" (grind) (("" (decompose-equality 1) nil nil )) nil )nil vectors_4D_def nil )nil reals nil )nil vectors_4D nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"Vector" vectors_4D nil ))nil 3467130326 ("" (grind) nil nil )"Vector" vectors_4D nil )"Vector" vectors_4D nil )"odd_int" integers nil ))nil 3430827949"" (skeep)"" (grind)"" (mult-by 1 "nzv`x" )"" (mult-by 1 "nzv`y" )"" (mult-by 1 "nzv`z" )"" (mult-by 1 "nzv`t" )"" (typepred "nzv" )"" (rewrite "nzv_xyz_neq_0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors_4D nil )"real" reals nil )nil vectors_4D nil )"Nz_vector" vectors_4D nil )nil vectors_4D nil )"Vector" vectors_4D nil )"boolean" notequal nil )nil vectors_4D 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 3255949424"" (skosimp*)"" (grind)"" (mult-by 1 "nzv!1`x" )"" (mult-by 1 "nzv!1`y" )"" (mult-by 1 "nzv!1`z" )"" (typepred "nzv!1" )"" (flatten)"" (assert )"" (hide 2)"" (grind) (("" (rewrite "sqrt_0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3255949401 ("" (postpone) nil nil ) nil shostak))nil 3440245830"" (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_4D nil )nil vectors_4D_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_4D nil ))nil 3440245840"" (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_4D 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_4D nil ))nil 3440250284"" (grind)"" (apply-extensionality 2 :hide? t)"1" (mult-cases -2) nil nil ) ("2" (mult-cases -3) nil nil )"3" (mult-cases -4) nil nil ) ("4" (mult-cases -5) nil nil ))nil ))nil )nil vectors_4D nil )nil real_props 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 )"Vector" vectors_4D nil )"Vector" vectors_4D nil ))nil ))nil 3413211084 ("" (grind) nil nil )"(total_order?[real])" nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3413211088 ("" (grind) nil nil )"(strict_total_order?[real])" real_props nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil 3254160430"" (skosimp*)"" (prop)"1" "(a!1 * v!1)`x = v!1`x AND (a!1 * v!1)`y = v!1`y AND (a!1 * v!1)`z = v!1`z" )"1" (flatten)"1" (expand "zero" )"1" (expand "*" )"1" (apply-extensionality 2 :hide? t) nil nil )) nil ))nil ))nil )"2" (replace -1) (("2" (propax) nil 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_4D nil )"Vector" vectors_4D nil )nil vectors_4D 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_4D_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"Vector" vectors_4D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3430826073"" (skeep)"" (rewrite "sqv_sub" )"" (rewrite "sqv_scal" )"" (assert ) (("" (neg-formula 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )nil vectors_4D nil )nil reals nil )nil vectors_4D nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"Vector" vectors_4D 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_4D 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_4D nil ))nil ))nil 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3255194049"" (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_4D nil )nil real_types nil )nil vectors_4D 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 3254160430"" (skosimp*)"" (expand "norm" )"" (rewrite "sqrt_eq" ) (("" (rewrite "sqv_sym" ) nil nil )) nil ))nil ))nil )"nnreal" vectors_4D nil )nil vectors_4D nil )"Vector" vectors_4D nil )"nnreal" vectors_4D nil )nil real_types nil )nil vectors_4D 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 3254160430 ("" (grind) nil nil )"Vector" vectors_4D nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"nnreal" vectors_4D nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3254160430"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" ) (("" (grind) nil nil )) nil )) nil ))nil )"nnreal" vectors_4D nil )"real" vectors_4D nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" vectors_4D nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil vectors_4D 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 3403524082 ("" (grind) nil nil )"nnreal" nil )"real" vectors_4D nil )"nnreal" vectors_4D nil )"nnreal" vectors_4D nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil ))nil ))nil 3254160430"" (skosimp*) (("" (expand "norm" ) (("" (propax) nil nil )) nil ))nil )"nnreal" vectors_4D nil )) nil ))nil 3427102244"" (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_4D nil )nil vectors_4D nil )"nnreal" vectors_4D nil )nil real_types nil )nil vectors_4D 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 3602099537"" (skeep)"" (rewrite "norms_eq_sqv" )"" (rewrite "sqv_sos" )"" (rewrite "sqv_sos" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil vectors_4D nil )nil reals nil )nil vectors_4D nil )nil vectors_4D nil ))nil 3475937541"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_le" ) (("" (inst?) nil nil )) nil )) nil ))nil )"nnreal" vectors_4D nil )"nnreal" vectors_4D nil )nil real_types nil )nil vectors_4D 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 3475937556"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_lt" ) (("" (inst?) nil nil )) nil )) nil ))nil )"nnreal" vectors_4D nil )"nnreal" vectors_4D nil )nil real_types nil )nil vectors_4D 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 3254160430"" (skosimp*)"" (expand "norm" )"" (rewrite "sqv_scal" )"" (rewrite "sqrt_times" )"" (rewrite "sqrt_sq_abs" ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors_4D nil )nil sqrt "reals/" )nil booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors_4D nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sqrt "reals/" )"nnreal" nil )nil vectors_4D 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_4D nil ))nil ))nil 3430828042"" (skeep)"" (rewrite "norm_scal" )"" (expand "abs" ) (("" (grind-reals) nil nil )) nil )) nil ))nil )"posreal" vectors_4D nil )"posreal" nil )nil vectors_4D 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_4D nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" vectors_4D nil )"Vector" vectors_4D nil )nil vectors_4D nil )"{y: posreal | y >= x}" nil )"posreal" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil )nil 3256053649 ("" (subtype-tcc) nil nil ) nil shostak))nil 3560353164"" (skeep) (("" (typepred "^(nzv)" ) (("" (propax) nil nil )) nil ))nil )"Normalized" vectors_4D nil )nil vectors_4D nil )nil vectors_4D nil )"Vector" vectors_4D nil )"boolean" notequal nil )"nnreal" vectors_4D nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil vectors_4D nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )quality 100%
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.26Bemerkung:
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
