Quelle vect_vect_2D_continuity.prf
Sprache: Lisp
(vect_vect_2D_continuitynil 3515487776 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" vect_vect_2D_continuity nil )"boolean" notequal nil ))nil ))nil 3515488189"" (skeep)"" (expand "continuous_vvv?" )"" (skeep)"" (typepred "ffvc" )"" (typepred "ggvc" )"" (expand "continuous_vvv?" )"" (inst - "epsil/2" "s" "nzv" )"" (inst - "epsil/2" "s" "nzv" )"" (skosimp*)"" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)" )"" (skeep)"" (inst - "sp" "nzvp" )"" (inst - "sp" "nzvp" )"" (assert )"" expand "sum_vvv" )"" "norm_add_le" )"" "ffvc(s,nzv) - ffvc(sp,nzvp)" "ggvc(s,nzv) - ggvc(sp,nzvp)" )"" "norm" "min" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"nnreal" nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_vect_2D_continuity nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"posreal" nil ))nil 3515494507"" (skeep)"" (expand "continuous_vvr?" )"" (skeep)"" (typepred "ffrc" )"" (typepred "ggrc" )"" (expand "continuous_vvr?" )"" (inst - "epsil/2" "s" "nzv" )"" (inst - "epsil/2" "s" "nzv" )"" (skosimp*)"" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)" )"" (skeep)"" (inst - "sp" "nzvp" )"" (inst - "sp" "nzvp" )"" (assert )"" expand "sum_vvr" )"" "triangle" )"" "ffrc(s,nzv) - ffrc(sp,nzvp)" "ggrc(s,nzv) - ggrc(sp,nzvp)" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" vect_vect_2D_continuity nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"nnreal" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vect_vect_2D_continuity nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"posreal" nil ))nil ))nil 3515488435"" (skeep)"" (expand "continuous_vvv?" )"" (skeep)"" (typepred "ffvc" )"" (typepred "ggvc" )"" (expand "continuous_vvv?" )"" (inst - "epsil/2" "s" "nzv" )"" (inst - "epsil/2" "s" "nzv" )"" (skosimp*)"" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)" )"" (skeep)"" (inst - "sp" "nzvp" )"" (inst - "sp" "nzvp" )"" (assert )"" expand "diff_vvv" )"" "norm_add_le" )"" "ffvc(s,nzv) - ffvc(sp,nzvp)" "ggvc(sp,nzvp) - ggvc(s,nzv)" )"" "norm_neg" )"" "ggvc(sp, nzvp) - ggvc(s, nzv)" )"" "norm" "min" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_vect_2D_continuity nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"posreal" nil ))nil )nil 3515488366"" (skeep)"" (expand "continuous_vvv?" )"" (skeep)"" (typepred "ffvc" )"" (typepred "ggvc" )"" (expand "continuous_vvv?" )"" (inst - "epsil/2" "s" "nzv" )"" (inst - "epsil/2" "s" "nzv" )"" (skosimp*)"" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)" )"" (skeep)"" (inst - "sp" "nzvp" )"" (inst - "sp" "nzvp" )"" (assert )"" expand "sum_vvv" )"" "norm_add_le" )"" "ffvc(s,nzv) - ffvc(sp,nzvp)" "ggvc(s,nzv) - ggvc(sp,nzvp)" )"" "norm" "min" ))nil ))))))))))))))))))))))))))))))))))nil )nil nil ))nil 3515833806"" (skeep)"" (typepred "ffvc" )"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst - "epsil!1/(abs(c)+1)" "s!1" "nzv!1" )"" (skosimp*)"" (inst + "ds!1" "dv!1" )"" (skosimp*)"" (inst - "sp!1" "nzvp!1" )"" (assert )"" (expand "scal_vvv" )"" (lemma "norm_scal" )"" "c" "ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1)" )"" (assert )"" case "c * (ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1))=c * ffvc(s!1, nzv!1) - c * ffvc(sp!1, nzvp!1)" )"1" replace -1)"1" "1" case "abs(c) * norm(ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1)) < epsil!1" )"1" (assert ) nil nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )"nnreal" nil )"real" reals nil )"real" reals nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil real_props nil )"Vector" vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D "vectors/" )"Vect2" vect_vect_2D_continuity nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"posreal" nil )"posreal" nil ))nil 3515489053"" (skeep)"" (expand "continuous_vvr?" )"" (skosimp*)"" (typepred "ffvc" )"" (typepred "ggvc" )"" (expand "continuous_vvv?" )"" (label "fcont" -2)"" (label "gcont" -1)"" "ep1" "epsil!1/(8*norm(ggvc(s!1,nzv!1))+1)" )"" "ep2" "epsil!1/(8*(norm(ffvc(s!1,nzv!1)) + ep1))" )"" (label "ep1name" -2)"" (label "ep2name" -1)"" (inst - "ep2" "s!1" "nzv!1" )"" (inst - "ep1" "s!1" "nzv!1" )"" "" "min(ds!1,ds!2)" "min(dv!1,dv!2)" )"" "" "sp!1" "nzvp!1" )"" "sp!1" "nzvp!1" )"" assert )"" expand "dot_vvv" )"" "triangle" )"" "ffvc(s!1,nzv!1) * ggvc(s!1,nzv!1) - ffvc(sp!1,nzvp!1) * ggvc(s!1,nzv!1)" " ffvc(sp!1,nzvp!1) * ggvc(s!1,nzv!1) - ") "" assert )"" "schwarz" )"" "ffvc(s!1,nzv!1)-ffvc(sp!1,nzvp!1)" "ggvc(s!1,nzv!1)" )"" assert )"" "schwarz" )"" "ffvc(sp!1,nzvp!1)" "ggvc(s!1,nzv!1) - ggvc(sp!1,nzvp!1)" )"" assert )"" rewrite "dot_sub_right" )"" rewrite "dot_sub_left" )"" case "norm(ffvc(s!1, nzv!1) - ffvc(sp!1, nzvp!1)) * norm(ggvc(s!1, nzv!1)) + norm(ffvc(sp!1, nzvp!1)) * ") "1" assert )nil nil )"2" "2" case "norm(ffvc(sp!1,nzvp!1)) <= norm(ffvc(s!1,nzv!1)) + ep1" )"1" replace "ep1name" "1" "ep1name" )"1" replace "ep2name" "1" "ep2name" )"1" "A" "ffvc(s!1,nzv!1)" )"1" "B" "ffvc(sp!1,nzvp!1)" )"1" "X" "ggvc(s!1,nzv!1)" )"1" "Y" "ggvc(sp!1,nzvp!1)" )"1" "yname" "1" "xname" "1" "bname" "1" "aname" "1" replace "aname" )"1" replace "bname" )"1" replace "xname" )"1" replace "yname" )"1" "aname" )"1" "bname" )"1" "xname" )"1" "yname" )"1" "gcont" )"1" "ep1name" )"1" "xname" )"1" replace "1" "1" replace "1" "myvar" "norm(A) + epsil!1 / (1+8 * norm(X))" )"1" "namemyvar" "1" case "norm(A - B) * norm(X) < epsil!1/2 AND norm(B) * norm(X - Y) <= epsil!1/2" )"1" "1" assert )nil nil ))nil )"2" "2" "1" case "ep1*norm(X) < epsil!1/2" )"1" "fcont" )"1" "norm(X)" )"1" assert )nil nil ))nil ))nil )"2" "2" replace "ep1name" "2" nil nil ))nil ))nil ))nil )"2" "2" "norm(X-Y)" )"2" "2" "2" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "fcont" "2" "norm_add_le" )"2" "ffvc(s!1, nzv!1)-ffvc(sp!1, nzvp!1)" "-ffvc(s!1, nzv!1)" )"2" 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" vect_vect_2D_continuity nil )"bool" vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nnreal" nil )nil real_props nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil reals nil )nil real_props nil )"nnreal" nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"Vect2" vect_vect_2D_continuity nil )nil real_props nil )nil extra_real_propsnil )"bool" reals nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"real" vectors_2D "vectors/" )"real" vect_vect_2D_continuity nil )"posreal" nil )"posreal" nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_types nil )"nnreal" vectors_2D "vectors/" ))nil )nil 3515488825 ("" (postpone) nil nil ) nil shostak))nil 3515496006"" (skeep)"" (name "fffv" "LAMBDA (s,nzv): (# x:= ffrc(s,nzv), y:= 0 #)" )"" (name "gggv" "LAMBDA (s,nzv): (# x:= ggrc(s,nzv), y:= 0 #)" )"" (lemma "dot_vvv_cont" )"" (inst - "fffv" "gggv" )"1" (hide -2 -3)"1" (expand "dot_vvv" )"1" (expand "prod_vvr" )"1" (expand "gggv" )"1" (expand "fffv" )"1" (expand "*" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "continuous_vvv?" )"2" (typepred "ggrc" )"2" (expand "continuous_vvr?" )"2" (skosimp*)"2" (inst - "epsil!1" "s!1" "nzv!1" )"2" (skosimp*)"2" (inst + "ds!1" "dv!1" )"2" (skosimp*)"2" "sp!1" "nzvp!1" )"2" assert )"2" rewrite "sqrt_sqv_norm" 1 :dir rl)"2" case "FORALL (vvww:Vect2): sqv(vvww) = sq(vvww`x) + sq(vvww`y)" )"1" rewrite -1)"1" expand "gggv" +)"1" expand "-" +)"1" rewrite "sq_0" )"1" assert )"1" case "FORALL (aaa:real): sqrt(sq(aaa)) = abs(aaa)" )"1" rewrite -1 1)nil nil )"2" "2" "2" case "aaa>=0" )"1" nil nil )"2" "sqrt_sq" )"2" "-aaa" )"2" rewrite "sq_neg" )"2" "1" replace "1" expand "abs" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (expand "continuous_vvv?" )"3" (typepred "ffrc" )"3" (expand "continuous_vvr?" )"3" (skosimp*)"3" (inst - "epsil!1" "s!1" "nzv!1" )"3" (skosimp*)"3" (inst + "ds!1" "dv!1" )"3" (skosimp*)"3" "sp!1" "nzvp!1" )"3" assert )"3" rewrite "sqrt_sqv_norm" 1 :dir rl)"3" case "FORALL (vvww:Vect2): sqv(vvww) = sq(vvww`x) + sq(vvww`y)" )"1" rewrite -1)"1" expand "fffv" +)"1" expand "-" +)"1" rewrite "sq_0" )"1" assert )"1" case "FORALL (aaa:real): sqrt(sq(aaa)) = abs(aaa)" )"1" rewrite -1 1)nil nil )"2" "2" "2" case "aaa>=0" )"1" nil nil )"2" "sqrt_sq" )"2" "-aaa" )"2" rewrite "sq_neg" )"2" "1" replace "1" expand "abs" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )nil vect_vect_2D_continuity nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil sqrt "reals/" )nil sq "reals/" )"real" reals nil )nil sqrt "reals/" )"(total_order?[real])" nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil real_types nil )"real" reals nil )"real" reals nil )"real" vect_vect_2D_continuity nil )"real" vectors_2D "vectors/" )"real" vect_vect_2D_continuity nil )"[[Vect2, Nz_vect2] -> [# x: real, y: naturalnumber #]]" nil )"[[Vect2, Nz_vect2] -> [# x: real, y: naturalnumber #]]" nil )"bool" vect_vect_2D_continuity nil ))nil 3515837711"" (skeep)"" (expand "continuous_vvr?" )"" (skosimp*)"" (inst + "1" "1" )"" (skosimp*)"" (expand "const_vvr" )"" (assert )"" (expand "abs" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" vect_vect_2D_continuity nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" vect_vect_2D_continuity nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil ))nil 3515494224"" (skeep)"" (name "ggx" "LAMBDA (s,nzv): ggvc(s,nzv)`x" )"" (name "ggy" "LAMBDA (s,nzv): ggvc(s,nzv)`y" )"" "ggvy" "LAMBDA (s,nzv): (# x:= 0, y:= ggvc(s,nzv)`y #)" )"" "ggvx" "LAMBDA (s,nzv): (# x:=ggvc(s,nzv)`x,y:=0 #)" )"" (lemma "sum_vvv_cont" )"" "scal_vvr_vvv(ffrc, ggvx)" "scal_vvr_vvv(ffrc,ggvy)" )"1" (hide-all-but (-1 1))"1" (expand "sum_vvv" )"1" (expand "scal_vvr_vvv" )"1" (expand "ggvy" )"1" (expand "ggvx" )"1" (expand "*" )"1" (expand "+" ) (("1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "prod_vvr_cont" )"2" (inst - "ffrc" "ggy" )"1" (hide-all-but (-1 1))"1" (expand "prod_vvr" )"1" (expand "scal_vvr_vvv" )"1" (expand "ggvy" )"1" (expand "*" )"1" expand "continuous_vvv?" )"1" expand "continuous_vvr?" )"1" "1" "epsil!1" "s!1" "nzv!1" )"1" "1" "ds!1" "dv!1" )"1" "1" "sp!1" "nzvp!1" )"1" assert )"1" expand "ggy" )"1" expand "-" )"1" rewrite "sqrt_sqv_norm" "1" case "FORALL (vvww:Vect2): sqv(vvww) = sq(vvww`x) + sq(vvww`y)" )"1" rewrite -1)"1" "1" case "FORALL (aaa:real): sqrt(sq(aaa)) = abs(aaa)" )"1" rewrite nil nil )"2" "2" "2" expand "abs" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "ggvc" )"2" (expand "continuous_vvv?" )"2" (expand "continuous_vvr?" )"2" (skosimp*)"2" "epsil!1" "s!1" "nzv!1" )"2" "2" "ds!1" "dv!1" )"2" "2" "sp!1" "nzvp!1" )"2" assert )"2" expand "ggy" )"2" "norm_ge_comps" )"2" "2" "2" "norm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (lemma "prod_vvr_cont" )"3" (inst - "ffrc" "ggx" )"1" (hide-all-but (-1 1))"1" (expand "prod_vvr" )"1" (expand "scal_vvr_vvv" )"1" (expand "ggvx" )"1" (expand "*" )"1" expand "continuous_vvv?" )"1" expand "continuous_vvr?" )"1" "1" "epsil!1" "s!1" "nzv!1" )"1" "1" "ds!1" "dv!1" )"1" "1" "sp!1" "nzvp!1" )"1" assert )"1" expand "ggx" )"1" expand "-" )"1" rewrite "sqrt_sqv_norm" "1" case "FORALL (vvww:Vect2): sqv(vvww) = sq(vvww`x) + sq(vvww`y)" )"1" rewrite -1)"1" "1" case "FORALL (aaa:real): sqrt(sq(aaa)) = abs(aaa)" )"1" rewrite nil nil )"2" "2" "2" expand "abs" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (typepred "ggvc" )"2" (expand "continuous_vvv?" )"2" (expand "continuous_vvr?" )"2" (skosimp*)"2" "epsil!1" "s!1" "nzv!1" )"2" "2" "ds!1" "dv!1" )"2" "2" "sp!1" "nzvp!1" )"2" assert )"2" expand "ggx" )"2" "norm_ge_comps" )"2" "2" "2" "norm" )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 )"bool" vect_vect_2D_continuity nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil vect_vect_2D_continuity nil )"[[Vect2, Nz_vect2] -> real]" nil )nil vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"(total_order?[real])" nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )nil sqrt "reals/" )"nonneg_real" sq "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" vectors_2D "vectors/" )nil real_types nil )"nnreal" nil )"Vector" vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"real" vect_vect_2D_continuity nil )"[[Vect2, Nz_vect2] -> real]" nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" vect_vect_2D_continuity nil )"[[Vect2, Nz_vect2] -> [# x: naturalnumber, y: real #]]" nil )"Vect2" vect_vect_2D_continuity nil )"bool" vect_vect_2D_continuity nil )"(continuous_vvr?)" vect_vect_2D_continuitynil )"[[Vect2, Nz_vect2] -> [# x: real, y: naturalnumber #]]" nil ))nil 3515834436"" (skeep)"" (typepred "ffrc" )"" (expand "continuous_vvr?" )"" (skosimp*)"" (inst - "epsil!1/(abs(c)+1)" "s!1" "nzv!1" )"" (skosimp*)"" (inst + "ds!1" "dv!1" )"" (skosimp*)"" (inst - "sp!1" "nzvp!1" )"" (assert )"" (expand "scal_vvr" )"" (lemma "abs_mult" )"" "c" "ffrc(s!1, nzv!1) - ffrc(sp!1, nzvp!1)" )"" (assert )"" assert )"" case "abs(c) * abs(ffrc(s!1, nzv!1) - ffrc(sp!1, nzvp!1)) < epsil!1" )"1" (assert ) nil nil )"2" "2" (cross-mult -1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"nnreal" nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" vect_vect_2D_continuity nil )"real" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"posreal" nil )"posreal" nil )"real" reals nil ))nil ))nil 3515487776 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" vect_vect_2D_continuity nil )"real" reals nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"bool" vect_vect_2D_continuity nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"boolean" notequal nil )"bool" vect_vect_2D_continuity nil ))nil ))nil 3515496927"" (skeep)"" (case "continuous_vvr?(div_vvr(LAMBDA (s,nzv): 1, ggnzc))" )"1" (lemma "prod_vvr_cont" )"1" (inst - "ffrc" "div_vvr(LAMBDA (s, nzv): 1, ggnzc)" )"1" (hide -2)"1" (expand "prod_vvr" )"1" (expand "div_vvr" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (name "gg" "ggnzc" )"2" (replace -1)"2" (hide -1)"2" (typepred "gg" )"2" (expand "continuous_vvr?" )"2" (skosimp*)"2" (expand "continuous_nz_vvr?" )"2" (flatten)"2" (expand "continuous_vvr?" )"2" "newep" "min(abs(gg(s!1,nzv!1))/2,sq(gg(s!1,nzv!1))*epsil!1/4)" )"2" (inst - "newep" "s!1" "nzv!1" )"1" "1" "ds!1" "dv!1" )"1" "1" "sp!1" "nzvp!1" )"1" assert )"1" expand "div_vvr" )"1" case "1 / gg(s!1, nzv!1) - 1 / gg(sp!1, nzvp!1) = (gg(sp!1,nzvp!1) - gg(s!1,nzv!1))/(gg(s!1,nzv!1)*gg(sp!1,nzvp!1))" )"1" replace -1)"1" rewrite "abs_div" )"1" "1" case "abs((gg(s!1, nzv!1) * gg(sp!1, nzvp!1))) >= sq(gg(s!1, nzv!1))/2" )"1" "1" "newep" )"1" "epsil!1" )"1" assert )"1" expand "abs" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "abs_mult" )"2" case "abs(gg(sp!1, nzvp!1)) >= abs(gg(s!1,nzv!1))/2" )"1" "sq_abs" )"1" "gg(s!1,nzv!1)" )"1" expand "sq" "1" replace "1" "1" "abs(gg(s!1, nzv!1))" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "triangle" )"2" "gg(s!1, nzv!1) - gg(sp!1, nzvp!1)" "gg(sp!1, nzvp!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (field) nil nil ))nil )"3" expand "nzero_vvr?" )"3" "s!1" "nzv!1" )"3" "sp!1" "nzvp!1" )"3" "nzreal_times_nzreal_is_nzreal" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nzero_vvr?" )"2" "s!1" "nzv!1" )"2" assert )"2" "2" "sq_eq_0" )"2" "2" assert )"2" expand "min" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )"real" vect_vect_2D_continuity nil )"bool" vect_vect_2D_continuity nil )"bool" vect_vect_2D_continuity nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil booleans nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )"(continuous_nz_vvr?)" nil )"real" vect_vect_2D_continuity nil )"nzreal" nil )"real" reals nil )"real" reals nil )nil vect_vect_2D_continuity nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(continuous_nz_vvr?)" nil )"Vect2" vect_vect_2D_continuity nil )"Nz_vect2" vect_vect_2D_continuity nil )"posreal" vect_vect_2D_continuity nil )"{z: nonneg_real | AND " nil )nil reals nil )nil real_types nil )nil sq "reals/" )nil real_props nil )"nnreal" nil )"real" reals nil )nil real_props nil )nil real_props nil )"Nz_vect2" vect_vect_2D_continuity nil )"Vect2" vect_vect_2D_continuity nil )"(total_order?[real])" nil )nil extra_real_propsnil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )nil reals nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )"nnreal" nil )"nnreal" nil )"{z: nonneg_real | z <= x AND z <= y}" real_defs nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"bool" reals nil )nil real_types nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3515498484"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst + "epsil!1" "epsil!1" ) (("" (skosimp*) nil nil )) nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" vect_vect_2D_continuity nil ))nil 3515498511"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst + "epsil!1" "epsil!1" ) (("" (skosimp*) nil nil )) nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" vect_vect_2D_continuity nil ))nil ))nil 3515834855"" (skeep)"" (typepred "ffrc" )"" (typepred "ggrc" )"" (expand "continuous_vvr?" )"" (skosimp*)"" (inst - "epsil!1" "s!1" "nzv!1" )"" (inst - "epsil!1" "s!1" "nzv!1" )"" (skosimp*)"" (inst + "min(ds!1,ds!2)" "min(dv!1,dv!2)" )"" (skosimp*)"" (inst - "sp!1" "nzvp!1" )"" (inst - "sp!1" "nzvp!1" )"" (assert )"" (hide (-3 -4))"" expand "max_vvr" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"real" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"odd_int" integers nil )"real" reals nil )"real" vect_vect_2D_continuity nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"{z: posreal | z <= x AND z <= y}" real_defs nil ))nil 3515853222"" (skeep)"" (typepred "ffvc" )"" (expand "continuous_vvr?" )"" (expand "continuous_vvv?" )"" (skeep)"" (inst - "epsil" "s" "nzv" )"" (skeep -1)"" (inst + "ds" "dv" )"" (skeep)"" (inst - "sp" "nzvp" )"" (assert )"" (expand "norm_vvv" )"" case "FORALL (vv,ww:Vect2): abs(norm(vv)-norm(ww))<=norm(vv-ww)" )"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide-all-but 1)"2" "2" "vectors_2D.norm_add_le" )"2" "vv-ww" "ww" )"2" assert )"2" "vectors_2D.norm_add_le" )"2" "ww-vv" "vv" )"2" assert )"2" "vectors_2D.norm_neg" )"2" "ww-vv" )"2" case "-(ww-vv) = vv-ww" )"1" replace -1)"1" "1" replace "1" expand "abs" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"boolean" notequal nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"nnreal" vect_vect_2D_continuity nil )nil vectors_2D "vectors/" )"nnreal" nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D "vectors/" )"real" reals nil )"(total_order?[real])" nil )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )"bool" vect_vect_2D_continuity nil )"real" reals nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.64 Sekunden
(vorverarbeitet am 2026-05-02)
¤ *© Formatika GbR, Deutschland
2026-05-26
