(limit_real_vect2nil 3473161988"" (grind :exclude ("abs" "norm" "-" "sigma" ) :if-match nil )"" (case "norm(l1!1 - l2!1) = 0" )"1" (hide -2 -3 -4)"1" (lemma "norm_eq_0" )"1" (inst?)"1" (assert )"1" (lemma "add_move_right" )"1" (inst?)"1" (inst -1 "zero" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "eps" "norm(l1!1 - l2!1)" )"2" (replace -1)"2" (inst -3 "eps/2" )"1" (inst -4 "eps/2" )"1" (skosimp*)"1" case " EXISTS (x: T): a!1 /= x AND abs(x - a!1) < delta!1 AND abs(x - a!1) < delta!2" )"1" (skosimp*)"1" (inst?)"1" (inst?)"1" (lemma "dist_triangle" )"1" (inst - "l1!1" "f!1(x!1)" "l2!1" )"1" (rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" "norm(l1!1 - l2!1) > 0" )"1" assert )"1" "norm_sym" )"1" "l1!1" "f!1(x!1)" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "norm_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "DEL" "min(delta!1,delta!2)" )"2" (inst - "a!1" )"2" (inst - "a!1" )"2" (assert )"2" (lemma "norm_triangle" )"2" (inst?)"2" "f!1(a!1)" )"2" assert )"2" "norm_sym" )"2" "l1!1" "f!1(a!1)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )nil distance_2D "vectors/" )nil distance_2D "vectors/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"(total_order?[real])" nil )nil vectors_2D "vectors/" )nil abs_lems "reals/" )nil vectors_2D "vectors/" )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )nil real_types nil )nil real_types nil )"nnreal" limit_real_vect2 nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )"nnreal" nil )"(strict_total_order?[real])" 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )"real" reals nil )"bool" limit_real_vect2 nil ))nil )nil 3445160510"" (grind :exclude ("abs" "norm" "-" "sigma" ) :if-match nil )"" (case "norm(l1!1 - l2!1) = 0" )"1" (hide -2 -3 -4)"1" (lemma "norm_eq_0" )"1" (inst?)"1" (assert )"1" (lemma "add_move_right" )"1" (inst?)"1" (inst -1 "zero" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "eps" "norm(l1!1 - l2!1)" )"2" (replace -1)"2" (inst -3 "eps/2" )"1" (inst -4 "eps/2" )"1" (skosimp*)"1" case " EXISTS (x: real): a!1 /= x AND abs(x - a!1) < delta!1 AND abs(x - a!1) < delta!2" )"1" (skosimp*)"1" (inst?)"1" (inst?)"1" (lemma "dist_triangle" )"1" (inst - "l1!1" "f!1(x!1)" "l2!1" )"1" (rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" "norm(l1!1 - l2!1) > 0" )"1" assert )"1" "norm_sym" )"1" "l1!1" "f!1(x!1)" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "norm_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "DEL" "min(delta!1,delta!2)" )"2" (inst + "a!1+DEL/2" )"2" (assert )"2" (hide -2 -3 -4 -5 3)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil distance_2D "vectors/" )nil distance_2D "vectors/" )nil vectors_2D "vectors/" ))nil )nil 3442578793"" (grind :exclude ("abs" "norm" "-" "sigma" ) :if-match nil )"" (case "norm(l1!1 - l2!1) = 0" )"1" (hide -2 -3 -4)"1" (lemma "norm_eq_0" )"1" (inst?)"1" (assert )"1" (lemma "add_move_right" )"1" (inst?)"1" (inst -1 "zero" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "eps" "norm(l1!1 - l2!1)" )"2" (replace -1)"2" (inst -3 "eps/2" )"1" (inst -4 "eps/2" )"1" (skosimp*)"1" case " EXISTS (x: real): a!1 /= x AND abs(x - a!1) < delta!1 AND abs(x - a!1) < delta!2" )"1" (skosimp*)"1" (inst?)"1" (inst?)"1" (lemma "dist_triangle_lt" )"1" (inst - "l1!1" "f!1(x!1)" "l2!1" )"1" (rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" rewrite "dist_norm" )"1" "norm(l1!1 - l2!1) > 0" )"1" assert )"1" "norm_sym" )"1" "l1!1" "f!1(x!1)" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "norm_eq_0" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (name "DEL" "min(delta!1,delta!2)" )"2" (inst + "a!1+DEL/2" )"2" (assert )"2" (hide -2 -3 -4 -5 3)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D "vectors/" )nil distance_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" ))nil )nil 3299406886"" (grind :exclude ("abs" "norm" "-" ) :if-match nil )"" (rewrite "abs_diff_0" )"" (name "eps" "abs(l1!1 - l2!1)" )"" (replace -1)"" (inst -4 "eps/2" )"1" (inst -5 "eps/2" )"1" (assert )"1" (skosimp*)"1" case " EXISTS (x: Vector): a!1 /= x AND norm(x - a!1) < delta!1 AND norm(x - a!1) < delta!2" )"1" (skosimp*)"1" (inst?)"1" (inst?)"1" (assert )"1" (case "0 < norm(x!1 - a!1)" )"1" assert )"1" "triangle2" )"1" "eps/2" "eps/2" "l1!1" "f!1(x!1)" "l2!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "norm_eq_0" )"2" "2" assert )"2" replace -1 * lr)"2" assert )"2" rewrite "sub_eq_zero" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -4 -5)"2" (name "DEL" "min(delta!1,delta!2)" )"2" "a!1 WITH [0 := a!1(0) + DEL/2]" )"1" (inst + "AA" )"1" (case "norm(AA - a!1) = abs(DEL/2)" )"1" replace -1 * lr)"1" "1" case "a!1 /= AA" )"1" assert )"1" "1" (grind) nil nil ))nil ))nil )"2" "2" assert )"2" "2" replace -1 * lr)"2" "2" case "AA WITH [(0) := AA(0) + DEL / 2](0) = AA(0)" )"1" "1" assert )nil nil ))nil )"2" replace -1 * lr)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" replace -1 * rl)"2" "2" expand "norm" )"2" "a!1 WITH [(0) := a!1(0) + DEL / 2] - a!1 = LAMBDA (i: Index): IF i = 0 THEN DEL/2 ELSE 0 ENDIF)") "1" "1" expand "sqv" )"1" expand "*" )"1" "sigma_first" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil abs_lems "reals/" )"real" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil sqrt "reals/" )nil abs_lems "reals/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" ))nil ))nil 3299406886"" (grind :exclude ("abs" "norm" "-" ) :if-match nil )"" (case "norm(l!1 - f!1(x!1)) = 0" )"1" (lemma "norm_eq_0" )"1" (inst?)"1" (assert ) (("1" (rewrite "sub_eq_zero" ) nil nil )) nil ))nil ))nil )"2" (inst - "norm(l!1 - f!1(x!1))" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (rewrite "norm_sym" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )"bool" reals nil )nil vectors_2D "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"(strict_total_order?[real])" real_props nil )nil abs_lems "reals/" )nil vectors_2D "vectors/" )nil real_types nil )nil real_types nil )"T" limit_real_vect2 nil )"[T -> Vect2]" limit_real_vect2 nil )"Vect2" limit_real_vect2 nil )"bool" reals nil )"(strict_total_order?[real])" 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )"real" reals nil )"bool" limit_real_vect2 nil ))nil ))nil 3299406886"" (skeep)"" (grind :exclude ("abs" "norm" "+" "-" ) :if-match nil )"" (inst - "epsilon!1/4" )"" (inst - "epsilon!1/4" )"" (skosimp*)"" (inst 1 "min(delta!1, delta!2)" )"" (skosimp*)"" (inst?)"" (inst?)"" (assert )"" (lemma "norm_add_le" )"" (inst - "f1(x!1) - l1" "f2(x!1)-l2" )"" "norm(f1(x!1) - l1 + (f2(x!1) - l2)) = norm((f1 + f2)(x!1) - (l1 + l2))" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (grind :exclude "norm" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" limit_real_vect2 nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props 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 )nil limit_real_vect2 nil )"[real -> boolean]" limit_real_vect2 nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D_def "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )"real" reals nil )"nnreal" nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"nnreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" nil ))nil ))nil 3445161748"" (skeep)"" (grind :exclude ("abs" "norm" "-" ) :if-match nil )"" (inst - "epsilon!1" )"" (skolem!)"" (inst + "delta!1" )"" (skosimp)"" (inst?)"" (assert )"" "norm((-f)(x!1) - -l) = norm(f(x!1) -l)" )"" (assert )"" (hide-all-but 1)"" (lemma "norm_neg" )"" (inst - "f(x!1) - l" )"" (grind :exclude "norm" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" limit_real_vect2 nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )"real" reals nil )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )nil real_types nil )"nnreal" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"[real -> boolean]" limit_real_vect2 nil )nil limit_real_vect2 nil ))nil )nil 3299406886"" (skeep)"" (grind :exclude ("abs" "norm" "-" ) :if-match nil )"" (inst - "epsilon!1" )"" (skolem!)"" (inst + "delta!1" )"" (skosimp)"" (inst?)"" (assert )"" "norm((-f)(x!1) - -l) = norm(f(x!1) -l)" )"" (assert )"" (hide-all-but 1)"" (lemma "norm_neg" )"" (inst - "f(x!1) - l" )"" (grind :exclude "norm" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )"nnreal" vectors_2D "vectors/" )nil vectors_2D "vectors/" ))nil ))nil 3299406886"" (skosimp*)"" (case-replace "f1!1 - f2!1 = f1!1 + (-f2!1)" )"1" (lemma "cv_sum" )"1" (inst?)"1" (inst - "(-f2!1)" "-l2!1" )"1" (assert )"1" (hide 2)"1" (lemma "cv_neg" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (grind) (("2" (apply-extensionality 1 :hide? t) 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" )"[T, T -> boolean]" equalities nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil limit_real_vect2 nil )nil limit_real_vect2 nil )"real" reals nil ))nil ))nil 3473594761";;; Proof cv_const-1 for formula limit_real_vect2.cv_const" expand "convergence" )";;; Proof cv_const-1 for formula limit_real_vect2.cv_const" ";;; Proof cv_const-1 for formula limit_real_vect2.cv_const" expand "const_vfun" )";;; Proof cv_const-1 for formula limit_real_vect2.cv_const" assert ) nil ))))))";;; developed with shostak decision procedures") nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"[T -> Vect2]" vect_fun_ops_rv nil )"bool" limit_real_vect2 nil )"real" reals nil ))nil )nil 3299406886"" (expand "convergence" )"" (skosimp*)"" (expand "const_fun" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" ))nil ))nil 3445182373"" (skeep)"" (case-replace "b = 0" )"1" (assert )"1" (lemma "cv_const" )"1" (inst - "a" "zero" )"1" (expand "const_vfun" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (expand "convergence" )"2" (skosimp*)"2" (inst - "epsilon!1/abs(b)" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (cross-mult -1)"1" (lemma "norm_scal" )"1" (inst - "b" "f(x!1)-l" )"1" (rewrite "scal_sub_right" )"1" expand "*" 2 1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (case "epsilon!1 / abs(b) > 0" )"1" (assert ) nil nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil )"3" (lemma "abs_eq_0" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil )"[T -> Vect2]" vect_fun_ops_rv nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil vectors_2D "vectors/" )nil abs_lems "reals/" )nil extra_real_props nil )nil abs_lems "reals/" )"(strict_total_order?[real])" real_props nil )nil vectors_2D "vectors/" )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )"nnreal" nil )"Vector" vectors_2D "vectors/" )"nnreal" vectors_2D "vectors/" )nil real_types nil )nil real_props nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"posreal" limit_real_vect2 nil )"boolean" notequal nil )nil booleans nil )"bool" reals nil )nil real_types 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 )"T" limit_real_vect2 nil )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" limit_real_vect2 nil )"real" reals nil ))nil )nil 3445182023"" (skeep)"" (expand "convergence" )"" (skosimp*)"" (inst - "epsilon!1/b" )"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst?)"1" (assert )"1" (lemma "norm_scal" )"1" (inst - "b" "f(x!1)" )"1" (cross-mult -2)"1" (postpone) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ) ("3" (postpone) nil nil ))nil ))nil ))nil ))nil )nil nil ))nil 3445162155"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (typepred "x0!1" )"" (expand "convergent?" )"" (skosimp*) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" )"bool" limit_real_vect2 nil )"bool" sets nil ))nil ))nil 3299406886"" (skolem!)"" (name-replace "ll" "lim(f!1, x0!1)" :hide? nil )"" (expand "lim" -)"" (typepred "choose(LAMBDA l: convergence(f!1, x0!1, l))" )"1" (assert ) nil nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )nil vectors_2D_def "vectors/" )nil booleans nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil booleans nil )"bool" limit_real_vect2 nil )"Vect2" limit_real_vect2 nil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )"bool" limit_real_vect2 nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil )"bool" sets nil ))nil ))nil 3299406886"" (skolem!)"" (use "lim_fun_lemma" )"" (ground)"" (use "cv_unique" ("l2" "lim(f!1, x0!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil limit_real_vect2 nil )"bool" limit_real_vect2 nil )nil booleans nil )nil vectors_2D_def "vectors/" )nil limit_real_vect2 nil )"[real -> boolean]" limit_real_vect2 nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil limit_real_vect2 nil )"Vect2" limit_real_vect2 nil ))nil ))nil 3299406886"" (skolem!)"" (prop)"1" (expand "convergent?" ) (("1" (inst?) nil nil )) nil )"2" (rewrite "lim_fun_def" )"2" (expand "convergent?" ) (("2" (inst?) nil nil )) nil )) nil )"3" (rewrite "lim_fun_def" ) nil nil ))nil ))nil )nil vectors_2D_def "vectors/" )nil reals nil )"bool" limit_real_vect2 nil )nil booleans nil )nil limit_real_vect2 nil )"[real -> boolean]" limit_real_vect2 nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil limit_real_vect2 nil ))nil ))nil 3299406886"" (grind :exclude "convergence" )"" (forward-chain "cv_in_domain" ) (("" (assert ) nil nil )) nil ))nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" )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]" limit_real_vect2 nil )nil limit_real_vect2 nil )"bool" limit_real_vect2 nil ))nil ))nil 3299406886"" (skosimp)"" (rewrite "lim_fun_def" )"" (rewrite "convergent_in_domain" ) nil nil )) nil ))nil )nil limit_real_vect2 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" )nil booleans nil )"bool" limit_real_vect2 nil )nil limit_real_vect2 nil ))nil ))nil 3299406886"" (expand "convergent?" )"" (skosimp*)"" (inst 1 "l!1 + l!2" ) (("" (rewrite "cv_sum" ) nil nil )) nil ))nil ))nil )nil limit_real_vect2 nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" limit_real_vect2 nil )nil limit_real_vect2 nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )"bool" limit_real_vect2 nil ))nil ))nil 3299406886"" (expand "convergent?" )"" (skosimp*)"" (forward-chain "cv_neg" ) (("" (inst?) nil nil )) nil )) nil ))nil )nil vectors_2D "vectors/" )"Vector" vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil limit_real_vect2 nil )"[real -> boolean]" limit_real_vect2 nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil limit_real_vect2 nil )"bool" limit_real_vect2 nil ))nil ))nil 3299406886"" (expand "convergent?" )"" (skosimp*)"" (inst 1 "l!1 - l!2" ) (("" (rewrite "cv_diff" ) nil nil ))nil ))nil ))nil )nil limit_real_vect2 nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" limit_real_vect2 nil )nil limit_real_vect2 nil )"Vector" vectors_2D "vectors/" )nil vectors_2D "vectors/" )nil vectors_2D_def "vectors/" )nil reals nil )"bool" limit_real_vect2 nil ))nil ))nil 3299406886"" (expand "convergent?" )"" (skolem!)"" (inst?) (("" (rewrite "cv_const" ) nil nil )) nil )) nil ))nil )nil limit_real_vect2 nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" )nil reals nil )"bool" limit_real_vect2 nil ))nil ))nil 3299406886"" (skosimp) (("" (rewrite "sum_fun_convergent" ) nil nil )) nil )nil limit_real_vect2 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" ))nil ))nil 3299406886"" "lim_fun_lemma" "lim_fun_def" "sum_fun_convergent" "cv_sum" ))"" (skosimp) (("" (assert ) nil nil )) nil )) nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil ))nil ))nil 3299406886"" (lemma "neg_fun_convergent" ) (("" (propax) nil nil )) nil )nil limit_real_vect2 nil )) nil ))nil 3299406886"" "lim_fun_lemma" "lim_fun_def" "neg_fun_convergent" "cv_neg" ))"" (skosimp) (("" (assert ) nil nil )) nil )) nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil ))nil ))nil 3299406886"" (skosimp) (("" (rewrite "diff_fun_convergent" ) nil nil )) nil )nil limit_real_vect2 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]" limit_real_vect2 nil )nil limit_real_vect2 nil )nil vectors_2D_def "vectors/" ))nil ))nil 3299406886"" "lim_fun_lemma" "lim_fun_def" "diff_fun_convergent" "cv_diff" ))"" (skosimp) (("" (assert ) nil nil )) nil )) nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil )nil limit_real_vect2 nil ))nil )))quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.25Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
