Impressum vectors.prf
Interaktion und
(vectorsnil 3254159790 ("" (subtype-tcc) nil nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" ) (("" (rewrite "sigma_nonneg" ) nil nil )) nil ))nil )"real" vectors nil )nil naturalnumbers nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil vectors nil )nil sigma "reals/" )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3440253127 ("" (grind) nil nil )"real" vectors nil )"nnreal" vectors nil )"real" reals nil )"int" integers nil ))nil 3602098415 ("" (grind) nil nil )"real" vectors nil )"nnreal" vectors nil )"nonneg_real" sq "reals/" )"nnreal" vectors nil )"real" reals nil )"int" integers nil ))nil 3254159790"" (skolem 1 "m" )"" (expand "norm" )"" (case "sqv(vectors.zero WITH [m := 1]) = 1" )"1" (expand "zero" )"1" (replace -1) (("1" (rewrite "sqrt_1" ) nil nil )) nil ))nil )"2" (hide 2)"2" (expand "sqv" )"2" (expand "*" )"2" (typepred "m" )"2" (case "m=n-1" )"1" (replace -1 :dir rl)"1" (expand "sigma" )"1" (assert )"1" (lemma "sigma_eq" )"1" "LAMBDA i:(zero WITH [m := 1](i)) * (zero WITH [m := 1](i))" "zero" "m-1" "0" )"1" (split -1)"1" replace -1)"1" "1" expand "zero" )"1" rewrite "sigma_zero" )nil nil ))nil ))nil ))nil )"2" "N" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sigma_split" )"2" "LAMBDA i: (zero WITH [m := 1](i)) * (zero WITH [m := 1](i))" "n-1" "0" "m" )"2" (assert )"2" (replace -1)"2" (hide -1)"2" "sigma(1 + m, n - 1, LAMBDA i: (zero WITH [m := 1](i)) * (zero WITH [m := 1](i))) =0") "1" "1" assert )"1" expand "sigma" )"1" assert )"1" "sigma_eq" )"1" "LAMBDA i:(zero WITH [m := 1](i)) * (zero WITH [m := 1](i))" "zero" "m-1" "0" )"1" "1" replace -1)"1" "1" expand "zero" )"1" rewrite "sigma_zero" )nil nil ))nil ))nil ))nil )"2" "2" "N" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_eq" )"2" "LAMBDA i:(zero WITH [m := 1](i)) * (zero WITH [m := 1](i))" "zero" "n-1" "1+m" )"2" "1" replace -1)"1" "1" expand "zero" )"1" rewrite "sigma_zero" )nil nil ))nil ))nil ))nil )"2" "2" "N" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )"real" vectors nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil naturalnumbers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"real" reals nil )"odd_int" integersnil )nil sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )nil sqrt "reals/" )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 reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil real_types nil )"nnreal" vectors nil )"Vector" vectors nil ))nil ))nil 3254159790 ("" (grind) nil nil )"real" vectors nil )) nil ))nil 3254159790 ("" (grind) nil nil )"real" vectors nil )) nil ))nil 3256995715"" (skosimp*) (("" (grind) nil nil )) nil )"real" reals nil )"Vector" vectors nil ))nil 3467132784"" (skeep) (("" (grind) nil nil )) nil )"real" reals nil )"Vector" vectors nil ))nil 3254159790 ("" (grind) nil nil )"Vector" vectors nil )) nil ))nil 3440253315"" (grind) (("" (apply-extensionality 1 :hide? t) nil nil )) nil )nil vectors 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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil ))nil 3428791579"" (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" (lemma "sigma_nonneg_eq_0" )"1" (inst?)"1" (skeep)"1" (inst -1 "i" )"1" assert )"1" (rewrite "sq_eq_0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (rewrite "sqv_sos" )"2" (expand "sos" )"2" (case-replace "(LAMBDA i:sq(v(i))) = (LAMBDA i:0)" )"1" (hide -)"1" (rewrite "sigma_const" )"1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (decompose-equality 1)"2" (inst?) (("2" (rewrite "sq_eq_0" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )nil sqrt "reals/" )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )nil sigma "reals/" )"[T, T -> boolean]" equalities 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil real_types nil )"nnreal" vectors nil )"nnreal" vectors nil )"int" integers nil )"nonneg_real" sq "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sq "reals/" )"nnreal" vectors nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )nil sigma "reals/" )nil vectors nil )nil sqrt "reals/" ))nil )nil 3428791425";;; Proof norm_xy_eq_0-1 for formula vectors_2D.norm_xy_eq_0" ";;; Proof norm_xy_eq_0-1 for formula vectors_2D.norm_xy_eq_0" expand "norm" )";;; Proof norm_xy_eq_0-1 for formula vectors_2D.norm_xy_eq_0" "1" (flatten)"1" (lemma "sqrt_eq_0" )"1" (inst -1 "sqv(v)" )"1" (split -1)"1" (hide -2)"1" (rewrite "sqv_sq" )"1" (rewrite "sq_plus_eq_0" ) nil )))))"2" (propax) nil )))))))))"2" (flatten)"2" (rewrite "sqv_sq" )"2" (ground)"2" (replaces -) (("2" (assert ) nil ))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3428791377"" (skeep)"" (expand "norm" )"" (ground) (("" (replaces -1) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors nil )nil sqrt "reals/" ))nil ))nil 3430054299"" (skeep)"" (lemma "norm_comp_eq_0" )"" (inst?)"" (replaces -1)"" (split)"1" (flatten)"1" (decompose-equality)"1" (inst?)"1" (expand "zero" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (skeep)"2" (decompose-equality -1)"2" (inst?)"2" (expand "zero" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors nil )"[T, T -> boolean]" equalities nil )"Vector" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3430834190"" (lemma "norm_eq_0" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )nil vectors nil ))nil )nil 3428791139"" (skeep)"" (lemma "norm_comp_eq_0" )"" (inst?)"" (replaces -1)"" (split)"1" (flatten)"1" (decompose-equality)"1" (inst?)"1" (expand "zero" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (skeep)"2" (decompose-equality -1)"2" (inst?)"2" (expand "zero" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3254159790"" (skosimp*)"" (expand "norm" )"" (prop)"1" (lemma "sqv_eq_0" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (replace -1)"2" (rewrite "sqv_zero" ) (("2" (rewrite "sqrt_0" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil sqrt "reals/" )) nil ))nil 3254159790"" (expand "sqv" )"" (expand "*" )"" (expand "zero" ) (("" (rewrite "sigma_const" ) nil nil )) nil ))nil ))nil )"real" vectors nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"(total_order?[real])" nil )"int" integers nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil )"Vector" vectors nil )"nnreal" vectors nil ))nil ))nil 3428790905"" (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 nil )nil vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3254159790"" (skolem 1 "v" )"" (prop)"1" (expand "sqv" )"1" (expand "*" )"1" (lemma "sigma_nonneg_eq_0" )"1" (inst?)"1" (apply-extensionality 1 :hide? t)"1" (inst?)"1" (assert )"1" (hide -2)"1" (grind :theories "real_props" ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (replace -1) (("2" (rewrite "sqv_zero" ) nil nil )) nil ))nil ))nil )nil sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" ))nil ))nil 3428790819"" (skeep)"" (lemma "sqv_eq_0" ) (("" (inst?) (("" (ground) nil nil )) nil ))nil ))nil )nil vectors nil )"(strict_total_order?[real])" real_props nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3412514418"" (skeep)"" (lemma "norm_eq_0" )"" (inst?)"" (assert )"" (expand "norm" )"" (flatten)"" (split +)"1" (flatten)"1" (expand "sqv" )"1" (case-replace "v*v = 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (assert )"2" (expand "*" )"2" (lemma "sigma_Fnnr" )"2" "2" assert )"2" expand "sq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -2)"2" (expand "zero" )"2" (expand "sq" )"2" (lemma "sigma_zero" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )"nnreal" vectors nil )"(strict_total_order?[real])" real_props nil )"Vector" vectors nil )nil sigma "reals/" )"nat" vectors nil )"real" vectors nil )"[T, T -> boolean]" equalities nil )nil sqrt "reals/" )nil sigma "reals/" )nil naturalnumbers nil )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" reals nil )"nnreal" vectors nil )"nnreal" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3428790726"" (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 nil )nil sq "reals/" )"nnreal" vectors nil )nil sqrt "reals/" )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3428790700 nil nil nil )nil 3428790692 ("" (postpone) nil nil ) nil shostak))nil 3430834221"" (skeep)"" (expand "nz_vector?" )"" (lemma "norm_eq_0" )"" (inst?)"" (lemma "norm_comp_eq_0" )"" (inst?)"" (replaces -1)"" (ground)"1" (skeep -1) (("1" (inst? -2) nil nil )) nil )"2" (skeep 4)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors nil )nil vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3430834334"" (skeep :preds? t)"" (expand "nz_vector?" )"" (flatten)"" (lemma "norm_eq_0" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors nil )"(strict_total_order?[real])" real_props nil )nil vectors nil )"Vector" vectors nil )"boolean" notequal nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3430833347 ("" (judgement-tcc) nil nil ) nil nil ))nil 3430834353"" (skeep :preds? t)"" (lemma "v_neq_zero" )"" (inst?)"" (expand "nz_vector?" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil vectors nil )"(strict_total_order?[real])" real_props nil )nil vectors nil )"Vector" vectors nil )"boolean" notequal nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3430833347 ("" (judgement-tcc) nil nil ) nil nil ))nil 3430834369"" (skeep :preds? t)"" (assert )"" (lemma "norm_eq_0" )"" (inst?)"" (expand "nz_vector?" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"nnreal" vectors nil )nil vectors nil )nil vectors nil ))nil )nil 3430833347 ("" (judgement-tcc) nil nil ) nil nil ))nil 3431076704"" (grind)"" (decompose-equality -1)"" (decompose-equality 1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"Vector" vectors 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"boolean" notequal nil ))nil ))nil 3431179313"" (grind)"" (decompose-equality 2)"" (decompose-equality -1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil )"real" reals nil )"Vector" vectors nil )"[T, T -> boolean]" equalities 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 )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"boolean" notequal nil ))nil ))nil 3462009511"" (expand "zero" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"Vector" vectors nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" ))"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" "w" ))"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3430835475"" (skolem 1 ("u" "v" "w" ))"" (ground)"1" (decompose-equality 1)"1" (decompose-equality -1)"1" (inst -1 "x!1" ) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (decompose-equality -1)"2" (decompose-equality 1)"2" (inst -1 "x!1" ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"real" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" "w" ))"" (ground)"1" (decompose-equality 1)"1" (decompose-equality -1)"1" (inst -1 "x!1" ) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (decompose-equality -1)"2" (decompose-equality 1)"2" (inst -1 "x!1" ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"real" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" "w" ))"" (ground)"1" (decompose-equality 1)"1" (decompose-equality -1)"1" (inst -1 "x!1" ) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (decompose-equality -1)"2" (decompose-equality 1)"2" (inst -1 "x!1" ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"real" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" ))"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )"real" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3254159790"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors nil )"real" vectors nil ) (+ const-decl "real" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil ))nil 3255196933"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors nil )"real" vectors nil ) (- const-decl "real" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil 3255196940"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors nil )"real" vectors nil ) (+ const-decl "real" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil 3430834445"" (grind)"" (decompose-equality 1)"" (decompose-equality -1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" vectors nil )"[T, T -> boolean]" equalities nil ))nil 3430834499"" (grind)"" (decompose-equality 1)"" (decompose-equality -1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" vectors nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3467130643"" (skeep)"" (grind)"1" (decompose-equality 1)"1" (decompose-equality -1) (("1" (grind) nil nil )) nil ))nil )"2" (decompose-equality 1) nil nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" vectors nil )"Vector" vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"real" reals nil ))nil 3467130713"" (skeep)"" (grind)"1" (decompose-equality 1) nil nil )"2" (decompose-equality 1)"2" (decompose-equality -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )nil vectors nil )"Vector" vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"[T, T -> boolean]" equalities nil ))nil 3430834506"" (skeep)"" (decompose-equality 1)"" (decompose-equality -1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" vectors nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3430834513"" (skeep)"" (decompose-equality 1)"" (decompose-equality -1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" vectors nil )"[T, T -> boolean]" equalities nil ))nil ))nil 3254159790"" (skosimp*)"" (apply-extensionality 1 :hide? t) (("" (grind) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"Vector" vectors nil )"Vector" vectors nil )"real" vectors nil )nil vectors nil )"real" reals nil )"real" reals nil ))nil ))nil 3254159790"" (skosimp*)"" (apply-extensionality 1 :hide? t) (("" (grind) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )"Vector" vectors nil )"real" vectors nil )nil vectors nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" ))"" (ground)"1" (decompose-equality 1)"1" (decompose-equality -1)"1" (inst -1 "x!1" )"1" (expand "zero" )"1" (expand "-" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (replace -1) (("2" (rewrite "sub_eq_args" ) nil nil )) nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"real" vectors nil )"Vector" vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil vectors nil ))nil ))nil 3254159790"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (grind) (("" (apply-extensionality :hide? t) nil nil )) nil )nil vectors nil )"real" vectors nil ) (- const-decl "real" vectors nil )"Vector" vectors nil )"real" reals nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" ))"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"Vector" vectors nil )"real" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" ))"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"Vector" vectors nil )"real" vectors nil ) (- const-decl "real" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"real" reals nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" )"" (lemma "sigma_scal" )"" (inst?)"1" (inst -1 "-1" )"1" (assert )"1" "(LAMBDA (i_673: below(n)): -1 * ((-u!1)(i_673) * w!1(i_673))) = (LAMBDA (i_673: below(n)): ((u!1)(i_673) * w!1(i_673)))" )"1" (assert ) nil nil )"2" (apply-extensionality 1 :hide? t)"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "sigma" ) (("2" (assert ) nil nil )) nil )"3" (expand "sigma" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"Vector" vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" )"" (lemma "sigma_scal" )"" (inst?)"1" (inst -1 "-1" )"1" (assert )"1" "(LAMBDA (i_673: below(n)): -1 * ((u!1)(i_673) * (-w!1)(i_673))) = (LAMBDA (i_673: below(n)): ((u!1)(i_673) * w!1(i_673)))" )"1" (assert ) nil nil )"2" (apply-extensionality 1 :hide? t)"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "sigma" ) (("2" (assert ) nil nil )) nil )"3" (expand "sigma" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"Vector" vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil ))nil 3429978001"" (skosimp)"" (rewrite "dot_neg_left" )"" (rewrite "dot_neg_right" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )"real" reals nil )nil vectors nil ))nil 3254159790"" (skolem 1 "v" )"" (expand "*" )"" (expand "zero" )"" (lemma "sigma_const" )"" (inst -1 "n-1" "0" "0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" vectors nil )nil naturalnumbers nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma "reals/" )"int" integers nil )"(total_order?[real])" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nat" vectors nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"Vector" vectors nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (expand "*" )"" (expand "zero" )"" (lemma "sigma_const" )"" (inst -1 "n-1" "0" "0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" vectors nil )nil naturalnumbers nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma "reals/" )"int" integers nil )"(total_order?[real])" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nat" vectors nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"Vector" vectors nil ))nil ))nil 3254159790"" (skolem 1 ("u" "v" ))"" (expand "*" ) (("" (assert ) nil nil )) nil )) nil )"real" vectors nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3254159790"" (skolem 1 ("a" "v" "w" ))"" (expand "*" )"" (lemma "sigma_scal" )"" (inst -1 "LAMBDA i: v(i) * w(i)" "a" "n-1" "0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"Vector" vectors nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" ) (("" (rewrite "sigma_nonneg" ) nil nil )) nil ))nil )"real" vectors nil )nil naturalnumbers nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil vectors nil )nil sigma "reals/" )"int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3440253864"" (skosimp*) (("" (expand "+ " ) (("" (propax) nil nil )) nil )) nil )"real" vectors nil )) shostak))nil 3440253876"" (skosimp*) (("" (expand "+ " ) (("" (propax) nil nil )) nil )) nil )"real" vectors nil )) shostak))nil 3254159790"" (skosimp*)"" (expand "*" )"" "(LAMBDA i: u!1(i) * (v!1 + w!1)(i)) = LAMBDA i: u!1(i) * v!1(i) + u!1(i) * w!1(i))") "1" (hide -1) (("1" (rewrite "sigma_sum" ) nil nil )) nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "+ " ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" vectors nil )nil naturalnumbers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" )"" "(LAMBDA i: (v!1 + w!1)(i) * u!1(i)) = LAMBDA i: v!1(i)* u!1(i) + w!1(i) * u!1(i))") "1" (hide -1) (("1" (rewrite "sigma_sum" ) nil nil )) nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "+ " ) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" vectors nil )nil naturalnumbers nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma "reals/" )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skosimp*)"" (rewrite "add_neg_sub" :dir rl)"" (rewrite "dot_add_right" )"" (rewrite "dot_neg_right" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"real" reals nil )"real" reals nil )"Vector" vectors nil )nil vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (rewrite "add_neg_sub" :dir rl)"" (rewrite "dot_add_left" )"" (rewrite "dot_neg_left" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"real" reals nil )"real" reals nil )"Vector" vectors nil )nil vectors nil ))nil ))nil 3268403303"" (skosimp*)"" (grind)"" (expand "*" )"" (apply-extensionality 1 :hide? t)"" (mult-by 1 "nza!1" )"" (assert )"" case "(LAMBDA i: nza!1 * u!1(i))(x!1) = (LAMBDA i: nza!1 * v!1(i))(x!1)" )"1" (assert ) nil nil )"2" (replace -1) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )nil reals nil )nil reals nil )nil real_props nil )"Vector" vectors nil ))nil 3254159790"" (skosimp*)"" (expand "*" )"" (lemma "sigma_scal" )"" (inst?)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"Vector" vectors nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" )"" (lemma "sigma_scal" )"" (inst?)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"Vector" vectors nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil ))nil 3440254239 ("" (grind) nil nil )"Vector" vectors nil )"real" vectors nil )"real" reals nil )"int" integers nil ))nil 3440254259"" (skosimp*)"" (expand "*" ) (("" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil )"Vector" vectors nil )nil number_fields nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3256913714"" (skosimp*)"" (rewrite "dot_scal_left" )"" (rewrite "dot_comm" )"" (rewrite "dot_scal_left" )"" (rewrite "dot_comm" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )"real" reals nil )nil vectors nil ))nil 3254656368"" (skosimp*)"" (expand "*" )"" (expand "+ " )"" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil )"Vector" vectors nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"real" reals 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil number_fields nil )"real" vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "*" )"" (expand "-" )"" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil )"real" reals nil )"Vector" vectors nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil number_fields nil )"real" vectors nil ))nil ))nil 3254656180"" (skosimp*)"" (expand "*" )"" (apply-extensionality 1 :hide? t)"" (expand "+ " ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"Vector" vectors nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"real" vectors nil )nil number_fields nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3254656212"" (skosimp*)"" (expand "*" )"" (expand "-" )"" (apply-extensionality 1 :hide? t) nil nil )) nil ))nil ))nil )"Vector" vectors nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil number_fields nil )"real" vectors nil )"real" reals nil ))nil 3430833357"" (skosimp*)"" (expand "*" ) (("" (apply-extensionality 1 :hide? t) nil nil ))nil ))nil )"Vector" vectors nil )nil number_fields nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3430833544"" (skosimp*)"" (expand "*" )"" (apply-extensionality 1 :hide? t) (("" (grind) nil nil ))nil ))nil ))nil )"Vector" vectors nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"Vector" vectors nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3430834822"" (grind)"1" (decompose-equality 2)"1" (decompose-equality -1)"1" (inst?) (("1" (grind) nil nil )) nil )) nil ))nil )"2" (decompose-equality 2) nil nil ))nil )"real" reals nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"nzreal" 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 3440253505"" (skeep)"" (expand "*" )"" (prop)"1" (apply-extensionality 1 :hide? t)"1" (replace -1 * rl)"1" (hide -1) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (apply-extensionality 1 :hide? t)"2" (lemma "comps_eq" )"2" (inst?)"2" (assert )"2" (hide -2)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"Vector" vectors nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil vectors nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil ))nil 3440254453"" (skeep)"" (expand "*" )"" (prop)"1" (apply-extensionality 1 :hide? t)"1" (replace -1 * lr)"1" (hide -1) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (apply-extensionality 1 :hide? t)"2" (lemma "comps_eq" )"2" (inst?)"2" (assert )"2" (hide -2)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"Vector" vectors nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil number_fields nil )nil vectors nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil ))nil )nil 3440254381"" (skosimp*) (("" (expand "*" ) (("" (postpone) nil nil )) nil ))nil )nil shostak))nil 3254159790"" (skolem 1 "a" )"" (decompose-equality 1)"" (expand "zero" ) (("" (grind) nil nil )) nil )) nil ))nil )nil vectors nil )"Vector" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3254159790"" (skolem 1 "v" )"" (decompose-equality 1) (("" (grind) nil nil )) nil )) nil )nil vectors nil )"Vector" vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3430834875"" (skeep) (("" (decompose-equality 1) (("" (grind) nil nil )) nil ))nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil 3467130571"" (skeep) (("" (decompose-equality 1) (("" (grind) nil nil )) nil ))nil )"odd_int" integers nil )nil vectors nil )"Vector" vectors nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil 3255950584"" (skeep)"" (expand "*" )"" (typepred "nzv" )"" (rewrite "nzv_comp_neq_0" )"" (skeep -1)"" (decompose-equality -1)"" (inst? -1) (("" (mult-by 2 "nzv(i)" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"Vector" vectors nil )nil vectors nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"Nz_vector" vectors nil )"Index" vectors nil )nil reals nil )nil real_props 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"boolean" notequal nil )"Vector" vectors nil )nil vectors nil ))nil ))nil 3268403498"" (skeep)"" (grind)"" (expand "*" )"" (decompose-equality 2)"" (decompose-equality -1)"" (inst?) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"Vector" vectors nil ))nil 3413210939"" (skosimp*)"" (expand "*" )"" (lemma "sigma_minus" )"" "LAMBDA i: w!1(i) * u!1(i)" "LAMBDA i: w!1(i) * v!1(i)" "n-1" "0" )"" (assert )"" (move-terms -1 l 2)"" (replace -1)"" (hide -1)"" (assert )"" "(LAMBDA i: w!1(i) * (u!1 - v!1)(i)) = (LAMBDA (i_1: below(n)): ") "1" (assert ) nil nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (hide -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"real" vectors nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil 3413210946"" (skosimp*)"" (expand "*" )"" (lemma "sigma_minus" )"" "LAMBDA i: w!1(i) * u!1(i)" "LAMBDA i: w!1(i) * v!1(i)" "n-1" "0" )"" (assert )"" (move-terms -1 l 2)"" (replace -1)"" (hide -1)"" (assert )"" "(LAMBDA i: w!1(i) * (u!1 - v!1)(i)) = (LAMBDA (i_1: below(n)): ") "1" (assert ) nil nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (hide -1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" vectors nil )"int" integers nil )"real" reals nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"real" vectors nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil sigma "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil ))nil 3254159790"" (skolem 1 ("a" "v" ))"" (ground)"1" (case "EXISTS (i:below(n)):v(i) /= 0" )"1" (skolem -1 "i" )"1" (decompose-equality -2)"1" (inst -1 "i" )"1" (expand "*" )"1" (lemma "both_sides_times1" )"1" (inst -1 "v(i)" "a" "1" )"1" (ground) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (decompose-equality 2)"2" (inst 2 "x!1" ) (("2" (grind) nil nil )) nil )) nil ))nil ))nil )"2" (expand "*" ) (("2" (decompose-equality 1) nil nil )) nil )"3" (replace -1) (("3" (rewrite "scal_zero" ) nil nil )) nil ))nil ))nil )"Vector" vectors nil )nil real_props nil )"real" reals nil )nil reals nil )"below(n)" vectors nil )"Vector" vectors nil )"Vector" vectors nil )"[T, T -> boolean]" equalities nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil naturalnumbers nil )"boolean" notequal nil )nil vectors nil )nil vectors nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "sqv" )"" (expand "*" )"" (assert ) (("" (expand "-" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"int" integers nil )"real" reals nil )"Vector" vectors nil )"real" vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "sqv" )"" (rewrite "dot_add_left" )"" (rewrite "dot_add_right" )"" (rewrite "dot_add_right" )"" (assert )"" (rewrite "dot_comm" )"" (rewrite "dot_comm" )"" (assert ) (("" (rewrite "dot_assoc" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )nil vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"real" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "sqv" )"" (rewrite "dot_scal_right" )"" (expand "sq" )"" (assert )"" (rewrite "dot_assoc" :dir rl) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )"nonneg_real" sq "reals/" )nil vectors nil )"real" reals nil )"Vector" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "sqv" )"" (rewrite "dot_sub_left" )"" (rewrite "dot_sub_right" )"" (rewrite "dot_sub_right" )"" (assert )"" (rewrite "dot_comm" )"" (rewrite "dot_comm" )"" (assert )"" (rewrite "dot_assoc" :dir rl)"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )nil vectors nil )"odd_int" integers nil )"real" reals nil )nil vectors nil )nil vectors nil )"real" reals nil )"real" reals nil )"real" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil ))nil ))nil 3430834954"" (skeep)"" (rewrite "sqv_sub" )"" (rewrite "sqv_scal" )"" (assert ) (("" (neg-formula 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )"nnreal" nil )"nnreal" nil )"real" reals nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"real" vectors 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 nil ))nil )nil 3430833789"" (skeep)"" (rewrite "sqv_sub" )"" (rewrite "sqv_scal" )"" (assert ) (("" (neg-formula 1) (("" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )nil nil ))nil 3254159790"" (skosimp*)"" (expand "sqv" )"" (expand "*" )"" "(LAMBDA i: (v!1 - u!1)(i) * (v!1 - u!1)(i)) = (LAMBDA i: (u!1 - v!1)(i) * (u!1 - v!1)(i))" )"" (hide 2)"" (apply-extensionality 1 :hide? t)"" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"real" vectors nil )"real" reals nil )"real" vectors nil ))nil ))nil 3255194068"" (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 nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "norm" )"" (rewrite "sqrt_eq" ) (("" (rewrite "sqv_sym" ) nil nil )) nil ))nil ))nil )"nnreal" vectors nil )nil vectors nil )"real" vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" ))nil ))nil 3254159790"" (skosimp*)"" (expand "norm" ) (("" (rewrite "sqv_neg" ) nil nil )) nil )) nil )"nnreal" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil ))nil ))nil 3254159790"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" )"" (expand "sqv" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )"nnreal" vectors nil )"(total_order?[real])" nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" ))nil ))nil 3403524127"" (skosimp*)"" (expand "norm" ) (("" (rewrite "sq_sqrt" ) nil nil )) nil )) nil )"nnreal" vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" )"(total_order?[real])" nil ))nil ))nil 3254159790"" (skosimp*) (("" (expand "norm" ) (("" (propax) nil nil )) nil ))nil )"nnreal" vectors nil )) nil ))nil 3425027810"" (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 nil )nil vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3602098547"" (skeep)"" (rewrite "norms_eq_sqv" )"" (rewrite "sqv_sos" )"" (rewrite "sqv_sos" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil vectors nil ))nil ))nil 3475937589"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_le" ) (("" (inst?) nil nil )) nil )) nil ))nil )"nnreal" vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" ))nil ))nil 3475937606"" (skosimp*)"" (expand "norm" )"" (lemma "sqrt_lt" ) (("" (inst?) nil nil )) nil )) nil ))nil )"nnreal" vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" ))nil ))nil 3254159790"" (skosimp*)"" (expand "norm" )"" (rewrite "sqv_scal" )"" (rewrite "sqrt_times" )"" (rewrite "sqrt_sq_abs" ) nil nil )) nil ))nil ))nil ))nil )"nnreal" vectors nil )nil sqrt "reals/" )nil real_types nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" vectors nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil sqrt "reals/" )"nnreal" nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil ))nil ))nil 3430835217"" (skeep)"" (rewrite "norm_scal" )"" (expand "abs" ) (("" (grind-reals) nil nil )) nil )) nil ))nil )"posreal" vectors nil )"posreal" nil )nil vectors 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil real_types nil )"nnreal" vectors nil )"Vector" vectors nil )nil vectors nil )"{y: posreal | y >= x}" nil )"posreal" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil )nil 3256053722 ("" (subtype-tcc) nil nil ) nil shostak))nil 3560353234"" (skeep) (("" (typepred "^(nzv)" ) (("" (propax) nil nil )) nil ))nil )"Normalized" vectors nil )nil vectors nil )nil vectors nil )"Vector" vectors nil )"boolean" notequal nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3256053877"" (skosimp*)"" (expand "^" )"" (assert )"" (rewrite "dot_scal_right" )"" (assert )"" (rewrite "dot_scal_left" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"Normalized" vectors nil )nil vectors 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil real_types nil )"nnreal" vectors nil )"Vector" vectors nil )nil vectors nil )"Vector" vectors nil )"real" reals nil )nil vectors nil )"Nz_vector" vectors nil )"posreal" nil )"posreal" vectors nil )"real" reals nil )"posreal" nil ))nil )nil 3255950619"" (skosimp*)"" (expand "normalize" )"" (assert )"" (rewrite "dot_scal_right" )"" (assert )"" (rewrite "dot_scal_left" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3268404906"" (skeep)"" (expand "^" )"" (rewrite "norm_scal" )"" (expand "abs" )"" (grind-reals) (("" (rewrite "scal_1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"Normalized" vectors nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"Vector" vectors nil )nil vectors nil )"Nz_vector" vectors nil )nil real_props nil )"posreal" nil )"{y: posreal | y >= x}" nil )nil vectors nil )"Vector" vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[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 nil )"posreal" nil )"posreal" vectors nil ))nil 3445611764"" (skeep)"" (expand "^" )"" (rewrite "scal_assoc" )"" (grind-reals) (("" (rewrite "scal_1" ) nil nil )) nil ))nil ))nil ))nil )"Normalized" vectors nil )nil real_props nil )nil vectors nil )"Nz_vector" vectors nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil vectors nil )"Vector" vectors nil )"boolean" notequal nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil )"posreal" nil )"posreal" vectors nil ))nil ))nil 3560354890"" (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 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 nil )"nnreal" vectors nil )nil real_types 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 integers nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil vectors nil )"nzreal" nil )"posreal" nil )"{y: posreal | y >= x}" nil )"posreal" vectors nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"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 nil ))nil ))nil 3255265285"" (skosimp*)"" (case "sqv(v!1) = 0" )"1" (rewrite "sqv_eq_0" )"1" (replace -1)"1" (hide -1)"1" (rewrite "dot_zero_right" )"1" (rewrite "sq_0" ) (("1" (assert ) nil nil )) nil ))nil ))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" (lemma "sqv_eq_0" )"2" (inst?) (("2" (assert ) 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" (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" "1" expand "sq" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide -1 2 3)"2" (rewrite "dot_scal_left" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) (("2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil vectors nil )"nnreal" nil )"(total_order?[real])" nil )nil sq "reals/" )nil vectors nil )"real" reals nil )"boolean" notequal nil )"Vector" vectors nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" vectors nil )"nnreal" nil )nil vectors 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 )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )nil vectors nil )"real" vectors nil )"Vector" vectors nil ))nil ))nil 3254159790"" (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 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 nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )"nnreal" vectors nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" vectors nil )"nonneg_real" sq "reals/" )nil real_types nil )"nnreal" nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3445088723"" (skeep)"" (lemma "dot_norm" )"" (expand "abs" )"" (inst?) (("" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil vectors 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 naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"nnreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil ))nil 3459101166"" (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 nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"Vector" vectors nil )"real" vectors nil ) (<= const-decl "bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"nnreal" vectors nil )nil vectors nil )"real" reals nil )nil vectors nil )"nnreal" nil )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors nil )"nnreal" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"{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 3445157516"" (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" "sqv_add" )"4" "4" expand "sqv" -1 2)"4" expand "sqv" -1 2)"4" assert )nil nil ))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" "dot_scal_left" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "sqv_add" )"2" (expand "sqv" ) (("2" (propax) nil nil )) 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 3445157297"" (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" rewrite "sqv_add" )"2" expand "sqv" )"2" nil nil ))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" "dot_scal_left" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "sqv_add" )"2" (expand "sqv" ) (("2" (propax) nil nil )) 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 3445156857"" (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" rewrite "sqv_add" )"2" expand "sqv" )"2" nil nil ))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" "dot_scal_left" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (rewrite "sqv_add" )"2" (expand "sqv" ) (("2" (propax) nil nil )) 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 3459097048"" (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 "-" )"" "(LAMBDA i:sq(u(i)-w(i))) = (LAMBDA i:sq(u(i)-v(i)+v(i)-w(i)))" )"1" (hide -1)"1" (lemma "schwarz_cor" )"1" (inst -1 "u-v" "v-w" )"1" (rewrite "sqv_sq" )"1" (rewrite "sqv_sq" )"1" rewrite "sqv_sq" )"1" expand "-" )"1" expand "+" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (decompose-equality) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"real" vectors nil )"real" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"nonneg_real" sq "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors nil )"real" vectors nil )"real" reals nil ))nil )nil 3459096992 ("" (postpone) nil nil ) nil shostak))nil 3255194138"" (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 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil real_types nil )"nnreal" vectors nil )"real" vectors 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 nil )"real" reals nil )nil vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"real" reals nil )nil vectors nil )"nnreal" nil )"(total_order?[real])" nil )nil sqrt "reals/" )nil sqrt "reals/" ))nil )nil 3255194125 ("" (postpone) nil nil ) nil shostak))nil 3254159790"" (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" )"" 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 )"nnreal" vectors 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/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"nnreal" vectors nil )"real" vectors nil )"[numfield, numfield -> numfield]" number_fields nil )nil sq "reals/" )nil vectors nil )"real" reals nil )nil vectors nil )"Vector" vectors nil )nil vectors nil )"real" reals nil )"real" reals nil )nil vectors nil )nil vectors nil )nil vectors nil )"nonneg_real" sq "reals/" )"nnreal" nil )nil sqrt "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )nil sq "reals/" ))nil ))nil 3255265208"" (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 nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil )"(total_order?[real])" nil )nil vectors nil )"real" vectors nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )nil 3255194342"" (skosimp*)"" (lemma "norm_add_le" )"" (inst -1 "u!1-v!1" "v!1" )"" (assert )"" (auto-rewrite-theory "vectors" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3256554706"" (skosimp*)"" (expand "norm" )"" (expand "sqv" )"" (expand "*" )"" (rewrite "sqrt_sq_abs" :dir rl)"" "(LAMBDA i: u!1(i) * u!1(i)) = LAMBDA i: sq(u!1(i)))") "1" (hide -1)"1" (lemma "sqrt_ge" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (case "i!1 = n - 1" )"1" (expand "sigma" )"1" (assert )"1" "1" "1" replace -1 * rl)"1" "sigma_nonneg[below[n]]" )"1" "1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "i!1 = 0" )"1" (lemma "sigma_first" )"1" "1" assert )"1" replace -1)"1" "1" assert )"1" "sigma_nonneg[below[n]]" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sigma_middle[below(n)]" )"2" "(LAMBDA i: sq(u!1(i)))" "n-1" "i!1" "0" )"2" assert )"2" replace -1)"2" "2" "sigma(1 + i!1, n - 1, (LAMBDA i: sq(u!1(i)))) >= 0" )"1" case "sigma(0, i!1 - 1, (LAMBDA i: sq(u!1(i)))) >= 0" )"1" (assert ) nil nil )"2" "2" "sigma_nonneg[below[n]]" )"2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_nonneg[below[n]]" )"2" "2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "sigma_nonneg[below[n]]" )"2" (inst?)"2" (assert )"2" (skosimp*) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "sq" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" vectors nil )"real" vectors nil )"nonneg_real" sq "reals/" )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"real" reals nil )nil sqrt "reals/" )"(total_order?[real])" nil )"nnreal" nil )nil sigma "reals/" )nil sigma "reals/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"nnreal" vectors nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" )"nnreal" vectors nil ))nil 3256551862"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (auto-rewrite "sqv_sub" )"" (auto-rewrite "scal_sub_right" )"" (auto-rewrite "dot_sub_right" )"" (auto-rewrite "dot_sub_left" )"" (auto-rewrite "sub_cancel" )"" (assert )"" (expand "sqv" )"" (auto-rewrite "dot_scal_assoc" )"" (auto-rewrite "dot_scal_right" )"" "dot_scal_left" )"" assert )"" "dot_comm" )"" "v0!1" "v1!1" )"" replace -1)"" "" "dot_comm" )"" "" (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 )"nnreal" nil )"nnreal" vectors nil )"odd_int" integers nil )nil vectors nil )nil vectors nil )"real" reals nil )nil vectors nil )nil vectors nil )nil vectors nil )nil vectors nil )"real" reals nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"real" vectors nil )"nnreal" vectors nil )nil real_types nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sqrt "reals/" ))nil )nil 3256551604"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (auto-rewrite "sqv_sub" )"" (auto-rewrite "scal_sub_right" )"" (auto-rewrite "dot_sub_right" )"" (auto-rewrite "dot_sub_left" )"" (auto-rewrite "sub_cancel" )"" (assert )"" (expand "sqv" )"" (auto-rewrite "dot_scal_assoc" )"" (assert )"" "dot_scal_right" )"" "dot_scal_left" )"" assert )"" "dot_comm" )"" "v0!1" "v1!1" )"" assert )"" replace -1)"" assert )"" "" "dot_comm" )"" "" 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 sqrt "reals/" )) nil )nil 3256551072"" (skosimp*)"" (expand "norm" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (rewrite "sq_sqrt" )"" (auto-rewrite "sqv_sub" )"" (assert )"" (auto-rewrite "scal_sub_right" )"" (assert )"" (auto-rewrite "dot_sub_right" )"" (assert )"" (auto-rewrite "dot_sub_left" )"" (assert )"" (expand "sqv" )"" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil ))nil 3430833917"" (skeep)"" (expand "parallel?" )"" (inst 1 "1" ) (("" (rewrite "scal_1" ) nil nil )) nil )) nil ))nil )"bool" vectors nil )nil vectors nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors 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 ))nil 3430833984"" (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 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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil vectors nil ))nil ))nil 3430834003"" (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 nil )nil vectors nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors 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 ))nil 3430834019"" (skeep)"" (expand "parallel?" )"" (split)"1" (flatten)"1" (skeep -1) (("1" (rewrite "scal_zero" ) nil nil )) nil ))nil )"2" (flatten)"2" (replaces -1)"2" (inst 1 "1" ) (("2" (rewrite "scal_zero" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vectors nil )nil vectors 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 ))nil 3430834131"" (skeep)"" (expand * "dir_parallel?" "parallel?" )"" (skeep -1) (("" (inst 1 "pk" ) nil nil )) nil )) nil ))nil )"bool" vectors nil )"bool" vectors 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 3447774095"" (skeep)"" (expand "orthogonal?" )"" (rewrite "sqv_add" )"" (assert )"" (rewrite "dot_scal_left" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" vectors nil )"real" reals nil )nil vectors nil )"real" reals nil )"nnreal" nil )nil vectors nil )nil vectors nil )"posnat" vectors nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors nil ))nil ))nil 3447774081"" (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/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )nil real_types nil )"nnreal" vectors nil )"real" vectors 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 nil )nil vectors nil )nil sq "reals/" ))nil ))nil 3447774063"" (skeep)"" (rewrite "add_comm" )"" (rewrite "norm_add_ge_left" )"" (expand "orthogonal?" ) (("" (rewrite "dot_comm" ) nil nil ))nil ))nil ))nil ))nil )nil vectors nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" vectors nil )nil vectors nil )nil vectors nil )"bool" vectors nil )nil vectors nil )"(total_order?[real])" nil )nil vectors nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=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.301Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-28)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
