Quelle vect2_cont_dot.prf
Sprache: Lisp
(vect2_cont_dotnil 3445266811"" (skeep)"" (typepred "vv1" )"" (typepred "vv2" )"" (expand "continuous_vv" )"" (expand "continuous_vr" )"" (expand "continuous_vr?" )"" (expand "continuous_vv?" )"" (skeep)"" (expand "continuous_vr?" )"" (expand "continuous_vv?" )"" (skosimp*)"" (inst - "x0" )"" (inst -2 "x0" )"" (inst-cp -2 "1" )"" "" case "FORALL (x: Vect2): norm(x - x0) < delta!1 IMPLIES norm(vv1(x)) < 1 + norm(vv1(x0))" )"1" "1" "r" "1 + norm(vv1(x0))" )"1" "epsilon!1/(2*r)" )"1" "1" case "norm(vv2(x0)) = 0" )"1" "norm_eq_0" )"1" "1" assert )"1" replace -1 * lr)"1" "1" assert )"1" "1" "min(delta!1,delta!2)" )"1" "1" "x!1" )"1" "x!1" )"1" assert )"1" "schwarz" )"1" "1" replace "1" "1" assert )"1" "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )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" "epsilon!1/(2*norm(vv2(x0)))" )"1" "1" "min(min(delta!1,delta!2),delta!3)" )"1" "1" "x!1" )"1" "x!1" )"1" "x!1" )"1" case "abs(vv1(x!1) * vv2(x!1) - vv1(x0) * vv2(x0)) <= norm(vv2(x0)) * norm((vv1(x!1) - vv1(x0))) + norm(vv1(x!1)) * norm((vv2(x!1) - vv2(x0)))" )"1" assert )"1" case "norm(vv1(x!1)) * norm((vv2(x!1) - vv2(x0))) <epsilon!1/2" )"1" case "norm(vv2(x0)) * norm((vv1(x!1) - vv1(x0))) < epsilon!1/2" )"1" assert )nil nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" assert )"2" case "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "triangle" )"2" "vv1(x!1) * (vv2(x!1) - vv2(x0))" "vv2(x0)*(vv1(x!1) - vv1(x0))" )"2" assert )"2" "schwarz" )"2" "vv1(x!1)" "(vv2(x!1) - vv2(x0))" )"2" "vv2(x0)" "(vv1(x!1) - vv1(x0))" )"2" assert )"2" "2" "norm" "abs" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "epsilon!1 / (2 * norm(vv2(x0))) > 0" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" assert )"2" "2" "norm_sub_ge" )"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 )"bool" cont_vect2_vect2 nil )nil vectors_2D_def "vectors/" )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cont_vect2_real nil )"bool" cont_vect2_vect2 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 )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"posreal" nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"{f: [Vect2 -> Vect2] | continuous_vv?(f)}" nil )"Vect2" vect2_cont_dot nil )"posreal" vect2_cont_dot nil )"real" reals nil )"real" reals nil )nil real_props nil )nil real_props nil )"real" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"nnreal" nil )nil extra_real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nnreal" nil )nil real_props nil )nil reals nil )nil extra_real_props nil )"(total_order?[real])" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" 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 vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"posreal" nil )nil vectors_2D "vectors/" )"bool" cont_vect2_real nil )"real" reals nil ))nil )nil 3445172424"" (skeep) (("" (postpone) nil nil )) nil ) nil shostak))nil 3445259881"" (skeep)"" (typepred "rv1" )"" (typepred "rv2" )"" (expand "continuous?" )"" (skeep)"" (rewrite "continuous_functions[T].continuity_def" )"" (expand "continuous_rv?" )"" (expand "convergence" )"" (expand "convergence" )"" (split +)"1" (hide -)"1" (expand "fullset" )"1" (expand "adh" )"1" (skosimp*)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "fullset" )"2" (inst - "x0" )"2" (inst -2 "x0" )"2" expand "continuous_rv?" )"2" "1" )"2" "2" case "FORALL x: abs(x - x0) < delta!1 IMPLIES norm(rv1(x)) < 1 + norm(rv1(x0))" )"1" "1" "r" "1 + norm(rv1(x0))" )"1" "epsilon!1/(2*r)" )"1" "1" case "norm(rv2(x0)) = 0" )"1" "norm_eq_0" )"1" "1" assert )"1" replace "1" "1" assert )"1" "1" "min(delta!1,delta!2)" )"1" "1" "x!1" )"1" "x!1" )"1" assert )"1" "schwarz" )"1" "1" replace "1" "1" assert )"1" "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )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" "epsilon!1/(2*norm(rv2(x0)))" )"1" "1" "min(min(delta!1,delta!2),delta!3)" )"1" "1" "x!1" )"1" "x!1" )"1" "x!1" )"1" case "abs(rv1(x!1) * rv2(x!1) - rv1(x0) * rv2(x0)) <= norm(rv2(x0)) * norm((rv1(x!1) - rv1(x0))) + norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0)))" )"1" assert )"1" case "norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0))) <epsilon!1/2" )"1" case "norm(rv2(x0)) * norm((rv1(x!1) - rv1(x0))) < epsilon!1/2" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" replace "2" "2" assert )"2" case "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "triangle" )"2" "rv1(x!1) * (rv2(x!1) - rv2(x0))" "rv2(x0)*(rv1(x!1) - rv1(x0))" )"2" assert )"2" "schwarz" )"2" "rv1(x!1)" "(rv2(x!1) - rv2(x0))" )"2" "rv2(x0)" "(rv1(x!1) - rv1(x0))" )"2" assert )"2" "2" "norm" "abs" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "epsilon!1 / (2 * norm(rv2(x0))) > 0" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" assert )"2" "2" "norm_sub_ge" )"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 )"bool" cont_real_vect2 nil )nil vectors_2D_def "vectors/" )nil vect2_cont_dot nil )"[real -> boolean]" vect2_cont_dot nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" continuous_functions "analysis/" )nil continuous_functions "analysis/" )nil vectors_2D "vectors/" )"real" vectors_2D "vectors/" )"bool" lim_of_functions "analysis/" )"set" sets nil )nil abs_lems "reals/" )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"setof[real]" convergence_functions "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"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 )"[bool, bool -> bool]" booleans nil )"posreal" nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"{f: [T -> Vect2] | continuous_rv?(f)}" nil )"T" vect2_cont_dot nil )"posreal" vect2_cont_dot nil )"real" reals nil )"real" reals nil )nil real_props nil )nil real_props nil )"Vector" vectors_2D "vectors/" )"nnreal" nil )nil extra_real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nnreal" nil )nil real_props nil )nil reals nil )nil extra_real_props nil )"(total_order?[real])" nil )"(total_order?[real])" 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 vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"posreal" nil )nil vectors_2D "vectors/" )"bool" cont_real_vect2 nil )"bool" convergence_functions "analysis/" )"real" reals nil ))nil )nil 3445259024"" (skeep)"" (typepred "rv1" )"" (typepred "rv2" )"" (expand "continuous_rv" )"" (expand "continuous?" )"" (expand "continuous" )"" (skosimp*)"" (expand "continuous" )"" (expand "continuous?" )"" (expand "convergence" )"" (expand "convergence" )"" (split +)"1" (hide -)"1" (expand "fullset" )"1" expand "adh" )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "fullset" )"2" "x0!1" )"2" "x0!1" )"2" "1" )"2" "2" case "FORALL x: abs(x - x0!1) < delta!1 IMPLIES norm(rv1(x)) < 1 + norm(rv1(x0!1))" )"1" "1" "r" "1 + norm(rv1(x0!1))" )"1" "epsilon!1/(2*r)" )"1" "1" "epsilon!1/(2*norm(rv2(x0!1)))" )"1" "1" "min(min(delta!1,delta!2),delta!3)" )"1" "1" "x!1" )"1" "x!1" )"1" "x!1" )"1" "abs(rv1(x!1) * rv2(x!1) - rv1(x0!1) * rv2(x0!1)) < norm(rv2(x0!1)) * norm((rv1(x!1) - rv1(x0!1))) + norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0!1)))" )"1" assert )"1" case "norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0!1))) <epsilon!1/2" )"1" case "norm(rv2(x0!1)) * norm((rv1(x!1) - rv1(x0!1))) < epsilon!1/2" )"1" assert )nil nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" replace "2" "2" assert )"2" case "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "triangle" )"2" "rv1(x!1) * (rv2(x!1) - rv2(x0!1))" "rv2(x0!1)*(rv1(x!1) - rv1(x0!1))" )"2" assert )"2" "schwarz" )"2" "rv1(x!1)" "(rv2(x!1) - rv2(x0!1))" )"2" "rv2(x0!1)" "(rv1(x!1) - rv1(x0!1))" )"2" assert )"2" "2" "norm" "abs" ))"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "epsilon!1 / (2 * norm(rv2(x0!1))) > 0" )"1" assert )nil nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3445174118"" (skeep)"" (typepred "rv1" )"" (typepred "rv2" )"" (expand "continuous_rv" )"" (expand "continuous?" )"" (expand "continuous" )"" (skosimp*)"" (expand "continuous" )"" (expand "continuous?" )"" (expand "convergence" )"" (expand "convergence" )"" (split +)"1" (hide -)"1" (expand "fullset" )"1" expand "adh" )"1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "fullset" )"2" "x0!1" )"2" "x0!1" )"2" "1" )"2" "2" case "FORALL x: abs(x - x0!1) < delta!1 IMPLIES norm(rv1(x)) < 1 + norm(rv1(x0!1))" )"1" "1" "r" "1 + norm(rv1(x0!1))" )"1" "epsilon!1/(2*r)" )"1" "1" "epsilon!1/(2*norm(rv2(x0!1)))" )"1" "1" "min(min(delta!1,delta!2),delta!3)" )"1" "1" "x!1" )"1" "x!1" )"1" "x!1" )"1" "abs(rv1(x!1) * rv2(x!1) - rv1(x0!1) * rv2(x0!1)) <= norm(rv2(x0!1)) * norm((rv1(x!1) - rv1(x0!1))) + norm(rv1(x!1)) * norm((rv2(x!1) - rv2(x0!1)))" )"1" assert )"1" case "epsilon!1 / (2 * r) + epsilon!1 / (2 * norm(rv2(x0!1))) = epsilon!1" )"1" assert )"1" nil nil ))nil )"2" nil nil ))nil ))nil )"2" "2" "triangle" )"2" "rv1(x!1) * (rv2(x!1) - rv2(x0!1))" "rv2(x0!1)*(rv1(x!1) - rv1(x0!1))" )"2" assert )"2" rewrite "dot_sub_right" )"2" rewrite "dot_sub_right" )"2" assert )"2" "schwarz" )"2" "rv1(x!1)" "(rv2(x!1) - rv2(x0!1))" )"2" "rv2(x0!1)" "(rv1(x!1) - rv1(x0!1))" )"2" assert )"2" rewrite "dot_sub_right" )"2" rewrite "dot_sub_right" )"2" assert )"2" "2" "norm" "abs" ))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" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3445271646"" (skeep)"" (typepred "rr" )"" (typepred "rv" )"" (expand "continuous?" )"" (expand "continuous_rv?" )"" (skeep)"" (inst - "x0" )"" (inst -2 "x0" )"" (expand "continuous?" )"" (expand "continuous_rv?" )"" (inst-cp -2 "1" )"" (skosimp*)"" case "FORALL x: abs(x - x0) < delta!1 IMPLIES abs(rr(x)) < 1 + abs(rr(x0))" )"1" (hide -4)"1" "r" "1 + abs(rr(x0))" )"1" "epsilon!1/(2*r)" )"1" "1" case "norm(rv(x0)) = 0" )"1" "norm_eq_0" )"1" "1" assert )"1" replace -1 * lr)"1" "1" assert )"1" "1" "min(delta!1,delta!2)" )"1" "1" "x!1" )"1" "x!1" )"1" assert )"1" rewrite "norm_scal" )"1" replace "1" "1" "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil )"2" rewrite "abs_abs" )"2" "2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "epsilon!1/(2*norm(rv(x0)))" )"1" "1" "min(min(delta!1,delta!2),delta!3)" )"1" "1" "x!1" )"1" "x!1" )"1" "x!1" )"1" case "norm(rr(x!1) * rv(x!1) - rr(x0) * rv(x0)) <= norm(rv(x0)) * abs((rr(x!1) - rr(x0))) + abs(rr(x!1)) * norm((rv(x!1) - rv(x0)))" )"1" assert )"1" case "abs(rr(x!1)) * norm((rv(x!1) - rv(x0))) <epsilon!1/2" )"1" case "norm(rv(x0)) * abs((rr(x!1) - rr(x0))) < epsilon!1/2" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "2" replace "2" "1" assert )"1" case "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" rewrite "abs_abs" )"2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "norm_triangle" )"2" "rr(x!1) * rv(x!1)" "rr(x!1)*rv(x0)" "rr(x0) * rv(x0)" )"2" assert )"2" "rr(x!1) * rv(x!1) - rr(x!1) * rv(x0) = ") "1" "1" "rr(x!1) * rv(x0) - rr(x0) * rv(x0) = ") "1" "1" rewrite "norm_scal" )"1" assert )"1" rewrite "norm_scal" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "epsilon!1 / (2 * norm(rv(x0))) > 0" )"1" (assert ) nil nil )"2" "2" nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "2" "2" "2" assert )"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 continuous_functions"analysis/" )"bool" continuous_functions "analysis/" )nil vect2_cont_dot nil )"[real -> boolean]" vect2_cont_dot nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cont_real_vect2 nil )"real" reals nil )"real" reals nil )"posreal" nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"{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 )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil reals nil )nil real_props nil )"{y: posreal | y >= x}" nil )"(total_order?[real])" nil )nil extra_real_props nil )"nnreal" nil )nil vectors_2D "vectors/" )"(total_order?[real])" nil )nil vectors_2D "vectors/" )nil extra_real_props nil )"nnreal" nil )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil real_props nil )nil vectors_2D "vectors/" )"real" reals nil )"odd_int" integers nil )"posreal" vect2_cont_dot nil )"T" vect2_cont_dot nil )"{f: [T -> Vect2] | continuous_rv?(f)}" nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"posreal" nil )"[bool, bool -> bool]" booleans 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 )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" continuous_functions "analysis/" )"real" reals nil )nil vectors_2D_def "vectors/" )"bool" cont_real_vect2 nil ))nil )nil 3445180767"" (skeep)"" (typepred "rr" )"" (typepred "rv" )"" (expand "continuous_rv" )"" (expand "continuous" )"" (expand "continuous?" )"" (expand "continuous" )"" (expand "continuous?" )"" (skosimp*)"" (expand "convergence" )"" (skosimp*)"" (inst - "x0!1" )"" (inst - "epsilon!1" )"" (skosimp*)"" "delta!1" )"" "" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3445275178"" (skeep)"" (typepred "vr" )"" (typepred "vv" )"" (expand "continuous_vv?" )"" (skeep)"" (expand "continuous_vv?" )"" (expand "continuous_vr?" )"" (skosimp*)"" (expand "continuous_vr?" )"" (inst - "x0" )"" (inst -2 "x0" )"" (inst-cp -2 "1" )"" (skosimp*)"" case "FORALL (x: Vect2): norm(x - x0) < delta!1 IMPLIES abs(vr(x)) < 1 + abs(vr(x0))" )"1" "1" "r" "1 + abs(vr(x0))" )"1" "epsilon!1/(2*r)" )"1" "1" case "norm(vv(x0)) = 0" )"1" "norm_eq_0" )"1" "1" assert )"1" replace -1 * lr)"1" "1" assert )"1" "1" "min(delta!1,delta!2)" )"1" "1" "x!1" )"1" "x!1" )"1" assert )"1" rewrite "norm_scal" )"1" replace "1" "1" "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil )"2" rewrite "abs_abs" )"2" "2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "epsilon!1/(2*norm(vv(x0)))" )"1" "1" "min(min(delta!1,delta!2),delta!3)" )"1" "1" "x!1" )"1" "x!1" )"1" "x!1" )"1" assert )"1" case "norm(vr(x!1) * vv(x!1) - vr(x0) * vv(x0)) <= norm(vv(x0)) * abs((vr(x!1) - vr(x0))) + abs(vr(x!1)) * norm((vv(x!1) - vv(x0)))" )"1" assert )"1" case "abs(vr(x!1)) * norm((vv(x!1) - vv(x0))) <epsilon!1/2" )"1" case "norm(vv(x0)) * abs((vr(x!1) - vr(x0))) < epsilon!1/2" )"1" assert )nil nil )"2" "2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "1" assert )"1" case "r * (epsilon!1 / (2 * r)) = epsilon!1/2" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil )"2" rewrite "abs_abs" )"2" "2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "norm_triangle" )"2" "vr(x!1) * vv(x!1)" "vr(x!1)*vv(x0)" "vr(x0) * vv(x0)" )"2" assert )"2" "vr(x!1) * vv(x!1) - vr(x!1) * vv(x0) = ") "1" "1" "vr(x!1) * vv(x0) - vr(x0) * vv(x0) = ") "1" "1" rewrite "norm_scal" )"1" assert )"1" rewrite "norm_scal" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "epsilon!1 / (2 * norm(vv(x0))) > 0" )"1" (assert ) nil nil )"2" "2" nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" assert )"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 )"bool" cont_vect2_real 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 )"bool" cont_vect2_vect2 nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil vectors_2D "vectors/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"posreal" nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"{f: [Vect2 -> Vect2] | continuous_vv?(f)}" nil )"Vect2" vect2_cont_dot nil )"posreal" vect2_cont_dot nil )"nnreal" nil )"Vector" vectors_2D "vectors/" )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil vectors_2D "vectors/" )"real" reals nil )"odd_int" integers nil )nil extra_real_props nil )nil vectors_2D "vectors/" )"(total_order?[real])" nil )nil vectors_2D "vectors/" )"nnreal" nil )nil extra_real_props nil )"(total_order?[real])" nil )"{y: posreal | y >= x}" nil )nil real_props nil )nil reals nil )nil real_props nil )"(strict_total_order?[real])" real_props 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 vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"posreal" nil )"real" reals nil )"real" reals nil )"bool" cont_vect2_real nil )"real" reals nil )"bool" cont_vect2_vect2 nil ))nil )nil 3445184045"" (skeep)"" (typepred "vr" )"" (typepred "vv" )"" (expand "continuous_vv" )"" (expand "continuous_vr" ) (("" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil )nil shostak))nil 3443886387"" (skeep)"" (lemma "scal_cont_rv" )"" (inst -1 "LAMBDA(x):y" "rv" )"" (rewrite "const_cont" ) nil nil )) nil ))nil ))nil )nil vect2_cont_dot nil )nil continuous_lambda "analysis/" )"T" vect2_cont_dot nil )"bool" cont_real_vect2 nil )nil vectors_2D_def "vectors/" )nil continuous_functions"analysis/" )"bool" continuous_functions "analysis/" )nil booleans nil )nil vect2_cont_dot nil )"[real -> boolean]" vect2_cont_dot nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.82 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
