Quelle four_vects_2D_continuity.prf
Sprache: Lisp
(four_vects_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 numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" four_vects_2D_continuity nil )"boolean" notequal nil ))nil ))nil 3515488189"" (skeep)"" (expand "continuous_vvv?" )"" (skeep)"" (typepred "ffvc" )"" (typepred "ggvc" )"" (expand "continuous_vvv?" )"" (inst - "epsil/2" "so" "vo" "si" "vi" )"" (inst - "epsil/2" "so" "vo" "si" "vi" )"" (skosimp*)"" "min(dso!1,dso!2)" "min(dvo!1,dvo!2)" "min(dsi!1,dsi!2)" "min(dvi!1,dvi!2)" )"" (skeep)"" (inst - "nso" "nvo" "nsi" "nvi" )"" (inst - "nso" "nvo" "nsi" "nvi" )"" (assert )"" expand "sum_vvv" )"" "norm_add_le" )"" "ffvc(so,vo,si,vi) - ffvc(nso,nvo,nsi,nvi)" "ggvc(so,vo,si,vi)-ggvc(nso,nvo,nsi,nvi)" )"" "norm" "min" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" four_vects_2D_continuity nil )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/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" four_vects_2D_continuity nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal 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" "so" "vo" "si" "vi" )"" (inst - "epsil/2" "so" "vo" "si" "vi" )"" (skosimp*)"" "min(dso!1,dso!2)" "min(dvo!1,dvo!2)" "min(dsi!1,dsi!2)" "min(dvi!1,dvi!2)" )"" (skeep)"" (inst - "nso" "nvo" "nsi" "nvi" )"" (inst - "nso" "nvo" "nsi" "nvi" )"" (assert )"" expand "sum_vvr" )"" "triangle" )"" "ffrc(so,vo,si,vi) - ffrc(nso,nvo,nsi,nvi)" "ggrc(so,vo,si,vi)-ggrc(nso,nvo,nsi,nvi)" )"" "norm" "min" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" four_vects_2D_continuity nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )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 )"Vector" vectors_2D "vectors/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(total_order?[real])" nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" four_vects_2D_continuity nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal 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" "so" "vo" "si" "vi" )"" (inst - "epsil/2" "so" "vo" "si" "vi" )"" (skosimp*)"" "min(dso!1,dso!2)" "min(dvo!1,dvo!2)" "min(dsi!1,dsi!2)" "min(dvi!1,dvi!2)" )"" (skeep)"" (inst - "nso" "nvo" "nsi" "nvi" )"" (inst - "nso" "nvo" "nsi" "nvi" )"" (assert )"" expand "diff_vvv" )"" "norm_add_le" )"" "ffvc(so,vo,si,vi) - ffvc(nso,nvo,nsi,nvi)" "ggvc(nso,nvo,nsi,nvi)-ggvc(so,vo,si,vi)" )"" "norm_neg" )"" "ggvc(so, vo, si, vi) - ggvc(nso, nvo, nsi, nvi)" )"" case "forall (eg1,eg2:Vect2): -(eg1-eg2) = eg2-eg1" )"1" rewrite -1)"1" "1" "norm" "min" ))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 ))nil ))nil )"bool" four_vects_2D_continuity nil )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/" )"[T, T -> boolean]" equalities nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" four_vects_2D_continuity nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal 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?" )"" (skeep)"" (inst - "epsil/(abs(c)+1)" "so" "vo" "si" "vi" )"" (skeep -1)"" (inst + "dso" "dvo" "dsi" "dvi" )"" (skeep)"" (inst - "nso" "nvo" "nsi" "nvi" )"" (assert )"" (cross-mult -1)"" "l1" "norm(ffvc(so, vo, si, vi) - ffvc(nso, nvo, nsi, nvi))" )"" (replace -1)"" (hide-all-but (-2 1))"" "l1" )"" expand "l1" -2 2)"" expand "scal_vvv" )"" "norm_scal" )"" "c" "ffvc(so, vo, si, vi) - ffvc(nso, nvo, nsi, nvi)" )"" assert )"" "norm" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" four_vects_2D_continuity nil )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 )"[T, T -> boolean]" equalities nil )"nnreal" four_vects_2D_continuity nil )nil vectors_2D "vectors/" )"nnreal" nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"Vector" vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"Vect2" four_vects_2D_continuity nil )"nnreal" nil )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )nil real_props 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 )"boolean" notequal 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(so!1,vo!1,si!1,vi!1))+1)" )"" "ep2" "epsil!1/(8*(norm(ffvc(so!1,vo!1,si!1,vi!1)) + ep1))" )"" (label "ep1name" -2)"" (label "ep2name" -1)"" "ep2" "so!1" "vo!1" "si!1" "vi!1" )"" "ep1" "so!1" "vo!1" "si!1" "vi!1" )"" "" "min(dso!1,dso!2)" "min(dvo!1,dvo!2)" "min(dsi!1,dsi!2)" "min(dvi!1,dvi!2)" )"" "" "nso!1" "nvo!1" "nsi!1" "nvi!1" )"" "nso!1" "nvo!1" "nsi!1" "nvi!1" )"" assert )"" expand "dot_vvv" )"" "triangle" )"" "ffvc(so!1,vo!1,si!1,vi!1) * ggvc(so!1,vo!1,si!1,vi!1) - ffvc(nso!1,nvo!1,nsi!1,nvi!1) * ggvc(so!1,vo!1,si!1,vi!1)" " ffvc(nso!1,nvo!1,nsi!1,nvi!1) * ggvc(so!1,vo!1,si!1,vi!1) - ") "" assert )"" "schwarz" )"" "ffvc(so!1,vo!1,si!1,vi!1)-ffvc(nso!1,nvo!1,nsi!1,nvi!1)" "ggvc(so!1,vo!1,si!1,vi!1)" )"" assert )"" "schwarz" )"" "ffvc(nso!1,nvo!1,nsi!1,nvi!1)" "ggvc(so!1,vo!1,si!1,vi!1) - ggvc(nso!1,nvo!1,nsi!1,nvi!1)" )"" assert )"" rewrite "dot_sub_right" )"" rewrite "dot_sub_left" )"" case "norm(ffvc(so!1,vo!1,si!1,vi!1) - ffvc(nso!1,nvo!1,nsi!1,nvi!1)) * norm(ggvc(so!1,vo!1,si!1,vi!1)) + norm(ffvc(nso!1,nvo!1,nsi!1,nvi!1)) * ") "1" assert )nil nil )"2" "2" case "norm(ffvc(nso!1,nvo!1,nsi!1,nvi!1)) <= norm(ffvc(so!1,vo!1,si!1,vi!1)) + ep1" )"1" replace "ep1name" "1" "ep1name" )"1" replace "ep2name" "1" "ep2name" )"1" "A" "ffvc(so!1,vo!1,si!1,vi!1)" )"1" "B" "ffvc(nso!1,nvo!1,nsi!1,nvi!1)" )"1" "X" "ggvc(so!1,vo!1,si!1,vi!1)" )"1" "Y" "ggvc(nso!1,nvo!1,nsi!1,nvi!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(so!1,vo!1,si!1,vi!1)-ffvc(nso!1,nvo!1,nsi!1,nvi!1)" "-ffvc(so!1,vo!1,si!1,vi!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" four_vects_2D_continuity nil )"bool" four_vects_2D_continuity nil )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" four_vects_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" four_vects_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 )"boolean" notequal 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 vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" ))nil )nil 3515488825 ("" (postpone) nil nil ) nil shostak))nil 3515496006"" (skeep)"" "fffv" "LAMBDA (so,vo,si,vi): (# x:= ffrc(so,vo,si,vi), y:= 0 #)" )"" "gggv" "LAMBDA (so,vo,si,vi): (# x:= ggrc(so,vo,si,vi), 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" "epsil!1" "so!1" "vo!1" "si!1" "vi!1" )"2" (skosimp*)"2" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"2" (skosimp*)"2" "nso!1" "nvo!1" "nsi!1" "nvi!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" "epsil!1" "so!1" "vo!1" "si!1" "vi!1" )"3" (skosimp*)"3" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"3" (skosimp*)"3" "nso!1" "nvo!1" "nsi!1" "nvi!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" four_vects_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 booleans nil )nil numbers nil )nil vectors_2D_def "vectors/" )nil reals nil )nil four_vects_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/" )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" four_vects_2D_continuity nil )"real" vectors_2D "vectors/" )"real" four_vects_2D_continuity nil )"[[Vect2, Vect2, Vect2, Vect2] -> [# x: real, y: naturalnumber #]]" nil )"[[Vect2, Vect2, Vect2, Vect2] -> [# x: real, y: naturalnumber #]]" nil )"bool" four_vects_2D_continuity nil ))nil 3515837711"" (skeep)"" (expand "continuous_vvr?" )"" (skosimp*)"" (expand "const_vvr" )"" (assert )"" (expand "abs" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" four_vects_2D_continuity nil )"real" four_vects_2D_continuity nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil ))nil 3515494224"" (skeep)"" (name "ggx" "LAMBDA (so,vo,si,vi): ggvc(so,vo,si,vi)`x" )"" (name "ggy" "LAMBDA (so,vo,si,vi): ggvc(so,vo,si,vi)`y" )"" "ggvy" "LAMBDA (so,vo,si,vi): (# x:= 0, y:= ggvc(so,vo,si,vi)`y #)" )"" "ggvx" "LAMBDA (so,vo,si,vi): (# x:=ggvc(so,vo,si,vi)`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" "so!1" "vo!1" "si!1" "vi!1" )"1" "1" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"1" "1" "nso!1" "nvo!1" "nsi!1" "nvi!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" "so!1" "vo!1" "si!1" "vi!1" )"2" "2" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"2" "2" "nso!1" "nvo!1" "nsi!1" "nvi!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" "so!1" "vo!1" "si!1" "vi!1" )"1" "1" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"1" "1" "nso!1" "nvo!1" "nsi!1" "nvi!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" "so!1" "vo!1" "si!1" "vi!1" )"2" "2" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"2" "2" "nso!1" "nvo!1" "nsi!1" "nvi!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" four_vects_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 booleans nil )nil numbers nil )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 four_vects_2D_continuity nil )"[[Vect2, Vect2, Vect2, Vect2] -> real]" nil )nil four_vects_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/" )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" four_vects_2D_continuity nil )"[[Vect2, Vect2, Vect2, Vect2] -> real]" nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vect2" four_vects_2D_continuity nil )"[[Vect2, Vect2, Vect2, Vect2] -> [# x: naturalnumber, y: real #]]" nil )"Vect2" four_vects_2D_continuity nil )"bool" four_vects_2D_continuity nil )"(continuous_vvr?)" nil )"[[Vect2, Vect2, Vect2, Vect2] -> [# x: real, y: naturalnumber #]]" nil ))nil 3515834436"" (skeep)"" (typepred "ffrc" )"" (expand "continuous_vvr?" )"" (skosimp*)"" "epsil!1/(abs(c)+1)" "so!1" "vo!1" "si!1" "vi!1" )"" (skosimp*)"" (inst + "dso!1" "dvo!1" "dsi!1" "dvi!1" )"" (skosimp*)"" (inst - "nso!1" "nvo!1" "nsi!1" "nvi!1" )"" (assert )"" (expand "scal_vvr" )"" case "FORALL (e1,e2:real): c*e1-c*e2 = c*(e1-e2)" )"1" (inst?)"1" (replace -1)"1" rewrite "abs_mult" )"1" "1" "1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" four_vects_2D_continuity nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )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 )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"nnreal" nil )nil real_props nil )"nnreal" nil )nil real_props nil )"real" four_vects_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 )"boolean" notequal 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 numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" four_vects_2D_continuity nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"bool" four_vects_2D_continuity nil )"nnreal" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"real" reals nil )"real" reals nil )"real" reals nil )"boolean" notequal nil )"bool" four_vects_2D_continuity nil ))nil ))nil 3515496927"" (skeep)"" case "continuous_vvr?(div_vvr(LAMBDA (so,vo,si,vi): 1, ggnzc))" )"1" (lemma "prod_vvr_cont" )"1" (inst - "ffrc" "div_vvr(LAMBDA (so,vo,si,vi): 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(so!1,vo!1,si!1,vi!1))/2,sq(gg(so!1,vo!1,si!1,vi!1))*epsil!1/4)" )"2" "newep" "so!1" "vo!1" "si!1" "vi!1" )"1" "1" "dso!1" "dvo!1" "dsi!1" "dvi!1" )"1" "1" "nso!1" "nvo!1" "nsi!1" "nvi!1" )"1" assert )"1" expand "div_vvr" )"1" case "1 / gg(so!1,vo!1,si!1,vi!1) - 1 / gg(nso!1,nvo!1,nsi!1,nvi!1) = (gg(nso!1,nvo!1,nsi!1,nvi!1) - gg(so!1,vo!1,si!1,vi!1))/(gg(so!1,vo!1,si!1,vi!1)*gg(nso!1,nvo!1,nsi!1,nvi!1))" )"1" replace -1)"1" rewrite "abs_div" )"1" "1" case "abs((gg(so!1,vo!1,si!1,vi!1) * gg(nso!1,nvo!1,nsi!1,nvi!1))) >= sq(gg(so!1,vo!1,si!1,vi!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(nso!1,nvo!1,nsi!1,nvi!1)) >= abs(gg(so!1,vo!1,si!1,vi!1))/2" )"1" "sq_abs" )"1" "gg(so!1,vo!1,si!1,vi!1)" )"1" expand "sq" "1" replace "1" "1" "abs(gg(so!1,vo!1,si!1,vi!1))" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "triangle" )"2" "gg(so!1,vo!1,si!1,vi!1) - gg(nso!1,nvo!1,nsi!1,nvi!1)" "gg(nso!1,nvo!1,nsi!1,nvi!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" "nzreal_times_nzreal_is_nzreal" )"3" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nzero_vvr?" )"2" "so!1" "vo!1" "si!1" "vi!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" four_vects_2D_continuity nil )"real" four_vects_2D_continuity nil )"bool" four_vects_2D_continuity nil )"bool" four_vects_2D_continuity nil )nil booleans nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil vectors_2D_def "vectors/" )nil reals nil )"(continuous_nz_vvr?)" nil )"real" four_vects_2D_continuity nil )"nzreal" nil )"real" reals nil )"real" reals nil )nil four_vects_2D_continuity nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(continuous_nz_vvr?)" nil )"Vect2" four_vects_2D_continuity nil )"Vect2" four_vects_2D_continuity nil )"Vect2" four_vects_2D_continuity nil )"Vect2" four_vects_2D_continuity nil )"posreal" four_vects_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 )"Vect2" four_vects_2D_continuity nil )"Vect2" four_vects_2D_continuity nil )"Vect2" four_vects_2D_continuity nil )"Vect2" four_vects_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 )"boolean" notequal 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 3533308937"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst + "epsil!1" "1" "1" "1" )"" (assert ) (("" (skosimp*) nil 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" four_vects_2D_continuity nil ))nil 3533309020"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst + "1" "epsil!1" "1" "1" )"" (assert ) (("" (skosimp*) nil 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" four_vects_2D_continuity nil ))nil ))nil 3533309025"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst + "1" "1" "epsil!1" "1" )"" (assert ) (("" (skosimp*) nil 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" four_vects_2D_continuity nil ))nil ))nil 3533309029"" (expand "continuous_vvv?" )"" (skosimp*)"" (inst + "1" "1" "1" "epsil!1" )"" (assert ) (("" (skosimp*) nil 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" four_vects_2D_continuity nil ))nil ))nil 3515834855"" (skeep)"" (typepred "ffrc" )"" (typepred "ggrc" )"" (expand "continuous_vvr?" )"" (skosimp*)"" (inst - "epsil!1" "so!1" "vo!1" "si!1" "vi!1" )"" (inst - "epsil!1" "so!1" "vo!1" "si!1" "vi!1" )"" (skosimp*)"" "min(dso!1,dso!2)" "min(dvo!1,dvo!2)" "min(dsi!1,dsi!2)" "min(dvi!1,dvi!2)" )"" (skosimp*)"" (inst - "nso!1" "nvo!1" "nsi!1" "nvi!1" )"" (inst - "nso!1" "nvo!1" "nsi!1" "nvi!1" )"" (assert )"" (hide-all-but (-1 -2 1))"" expand "max_vvr" )"" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" four_vects_2D_continuity nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )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" four_vects_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" "so" "vo" "si" "vi" )"" (skeep -1)"" (inst + "dso" "dvo" "dsi" "dvi" )"" (skeep)"" (inst - "nso" "nvo" "nsi" "nvi" )"" (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" four_vects_2D_continuity nil )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" four_vects_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 )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )"bool" four_vects_2D_continuity nil )"real" reals nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.57 Sekunden
(vorverarbeitet am 2026-04-28)
¤ *© Formatika GbR, Deutschland
2026-05-26
