Quelle unif_cont_fun.prf
Sprache: Lisp
(unif_cont_funnil 3324907658"" (skosimp*)"" "(LAMBDA (j: posnat): choose({xy: [real,real] | P3!1(xy`1,xy`2,j)})`1)" "(LAMBDA (j: posnat): choose({xy: [real,real] | P3!1(xy`1,xy`2,j)})`2)" )"1" (skosimp*)"1" (inst -1 "k!1" ) (("1" (assert ) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (inst -2 "j!1" )"2" (skosimp*) (("2" (inst -1 "(x!1,y!1)" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[[real, real, posnat] -> bool]" nil )"bool" sets nil )set type-eq-decl nil sets nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(p)" sets nil )"bool" sets nil )"bool" sets nil ))nil ))"FIX" 3447507474"" (skosimp*)"" (assert )"" (flatten)"" (expand "uniformly_continuous?" )"" (skosimp*)"" case "EXISTS (N: posnat): FORALL (x, y: ({xx: T | a!1 <= xx AND xx <= b!1})): ") "1" (skosimp*) (("1" (inst + "1/N!1" ) nil nil )) nil )"2" (hide 2)"2" case "EXISTS (eps: posreal): FORALL (N: posnat): AND xx <= b!1})):AND abs(f!1(x) - f!1(y)) >= eps") "1" (skosimp*)"1" (hide 1)"1" (lemma "getem_scaf4" )"1" "(LAMBDA (x,y: real,n:posnat): abs(x - y) < 1 / n AND a!1 <= x AND x <= b!1 AND a!1 <= y AND y <= b!1 AND abs(f!1(x) - f!1(y)) >= eps!1)" )"1" (split -1)"1" (hide -2)"1" "1" "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})" )"1" "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))" )"1" "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"1" case "a!1 <= CC AND CC <= b!1" )"1" "1" rewrite "continuous_on_def" )"1" "CC" )"1" expand "convergence" )"1" "1" "eps!1/2" )"1" "1" expand "extend" )"1" case "EXISTS (kk: posnat): CC <= alpha(kk) AND alpha(kk) < CC + delta!1/2 AND 1/kk < delta!1/2" )"1" "1" case "EXISTS (nn: posnat): alpha(kk!1) - delta!1/2 < XX!1(nn) AND XX!1(nn) <= alpha(kk!1) AND nn >= kk!1" )"1" "1" "nn!1" )"1" "1" case "1/nn!1 < delta!1/2" )"1" case "CC - delta!1/2 <= XX!1(nn!1) AND XX!1(nn!1) <= CC + delta!1/2" )"1" case "CC - delta!1 < YY!1(nn!1) AND YY!1(nn!1) < CC + delta!1" )"1" "1" "triangle" )"1" "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))" )"1" assert )"1" "XX!1(nn!1)" )"1" "YY!1(nn!1)" )"1" "1" "1" "1" "abs(f!1(CC) - f!1(YY!1(nn!1))) = abs(f!1(YY!1(nn!1))-f!1(CC))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "xxnn" "XX!1(nn!1)" )"4" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "yynn" "YY!1(nn!1)" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "connected_domain" )"2" expand "connected?" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "xxnn" "XX!1(nn!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" case "1/nn!1 <= 1/kk!1" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "lub(A(kk!1))" )"1" expand "least_upper_bound?" )"1" "1" "alpha(kk!1)- delta!1 / 2" )"1" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "j!1" )"2" assert )"2" replace "2" "2" case "CC <= XX!1(j!1)" )"1" assert )"1" replace "1" assert )"1" "XX!1(j!1)" )nil nil ))nil ))nil ))nil )"2" "XX!1(j!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace "1" assert )"1" "XX!1(kk!1)" )"1" "kk!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" replace "2" "CC+delta!1/2" )"2" assert )"2" "2" "s!1" )"2" "2" case "FORALL (ii: posnat): ii >= jj!1 IMPLIES alpha(ii) <= alpha(jj!1)" )"1" case "(EXISTS (jk: posnat): jk >= jj!1 AND 1/jk < delta!1/2)" )"1" "1" "jk!1" )"1" assert )"1" "jk!1" )"1" assert )"1" "alpha(jk!1)" )"1" assert )"1" "jk!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "archimedean" )"2" "delta!1/2" )"2" "2" "max(jj!1,n!1)" )"2" expand "max" )"2" "2" "2" case "1/jj!1 <= 1/n!1" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )"2" replace "2" "2" assert )"2" case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES ") "1" "1" assert )"1" "1" expand "subset?" )"1" expand "member" )"1" "1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(ii!1)" )"1" "ii!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "lub(A!1)" )"2" "lub(B!1)" )"2" expand "least_upper_bound?" )"2" "2" "lub(B!1)" )"2" assert )"2" "2" expand "upper_bound?" )"2" "2" "s!2" )"2" expand "subset?" )"2" expand "member" )"2" "s!2" )"2" "s!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "connected_domain" )"2" assert )"2" expand "connected?" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" "alpha(1)" )"1" replace -3)"1" case "alpha(1) <= b!1" )"1" assert )"1" "a!1" )"1" assert )"1" "1" "s!1" )"1" "1" replace "1" assert )"1" "1" replace "1" "1" assert )"1" "1" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "XX!1(jj!1)" )"1" assert )"1" "jj!1" )"1" assert )nil nil ))nil ))nil )"2" "jj!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!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 )"2" replace "2" assert )"2" "lub(A(1))" )"2" expand "least_upper_bound?" )"2" "2" "b!1" )"2" assert )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "alpha(1)" )"1" assert )"1" "1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" expand "lower_bound?" )"2" "a!1" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" replace "2" "2" assert )"2" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" replace "1" "1" expand "upper_bound?" )"1" assert )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil )"2" "jj!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!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 )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace -2 -1 rl)"1" assert )"1" "XX!1(kk!1)" )"1" assert )"1" "kk!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!1" )"2" replace -2 -1 rl)"2" "2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "n!1" )"2" "2" "x!1" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "connected_domain" )"2" assert )"2" expand "connected?" )"2" "a!1" "b!1" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*)"3" (lemma "connected_domain" )"3" assert )"3" expand "connected?" )"3" "a!1" "b!1" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "epsi!1" )"2" (skosimp*)"2" (inst 2 "N!1" )"2" (skosimp*)"2" (inst + "x!1" "y!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"bool" unif_cont_fun nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal 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 )nil real_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil unif_cont_fun nil )"[real -> boolean]" unif_cont_fun nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posrat" nil )"T" unif_cont_fun nil )"T" unif_cont_fun nil )"[T, T -> boolean]" equalities nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"{x | greatest_lower_bound?(x, SB)}" nil )"posnat" unif_cont_fun nil )"(total_order?[real])" nil )"[posnat -> [real -> boolean]]" unif_cont_funnil )"[kk: posnat -> {x | least_upper_bound?(x, A(kk))}]" unif_cont_funnil )"{x | " nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil unif_cont_fun nil )"bool" deriv_domain_def nil )"nnreal" nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )nil real_props nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" bounded_real_defs nil )"bool" sets nil )"bool" sets nil )"bool" bounded_real_defs nil )"(bounded_above?)" unif_cont_fun nil )"(bounded_above?)" unif_cont_fun nil )"(A!1)" unif_cont_fun nil )"posnat" unif_cont_fun nil )"[posnat -> real]" unif_cont_fun nil )"posnat" unif_cont_fun nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"posnat" unif_cont_fun nil )nil real_props nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"{k: posint | i <= k AND j <= k}" nil )"{s: posrat | s >= q AND s >= r}" nil )"R" extend nil )"posreal" nil )"bool" convergence_functions nil )nil continuous_functions nil )nil defined_types nil )"posnat" unif_cont_fun nil )"{x | least_upper_bound?(x, SA)}" bounded_real_defsnil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" sets nil )set type-eq-decl nil sets nil )nil unif_cont_fun nil ))nil )"FIX" 3399972727"" (skosimp*)"" (assert )"" (flatten)"" (expand "uniformly_continuous?" )"" (skosimp*)"" case "EXISTS (N: posnat): FORALL (x, y: ({xx: T | a!1 <= xx AND xx <= b!1})): ") "1" (skosimp*) (("1" (inst + "1/N!1" ) nil nil )) nil )"2" (hide 2)"2" case "EXISTS (eps: posreal): FORALL (N: posnat): AND xx <= b!1})):") "1" (skosimp*)"1" (hide 1)"1" (lemma "getem_scaf4" )"1" "(LAMBDA (x,y: real,n:posnat): abs(x - y) < 1 / n AND a!1 <= x AND x <= b!1 AND a!1 <= y AND y <= b!1 AND abs(f!1(x) - f!1(y)) >= eps!1)" )"1" (split -1)"1" (hide -2)"1" "1" "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})" )"1" "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))" )"1" "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"1" case "a!1 <= CC AND CC <= b!1" )"1" "1" expand "continuous?" )"1" "CC" )"1" expand "convergence" )"1" "1" "eps!1/2" )"1" "1" expand "extend" )"1" case "EXISTS (kk: posnat): CC <= alpha(kk) AND alpha(kk) < CC + delta!1/2 AND 1/kk < delta!1/2" )"1" "1" case "EXISTS (nn: posnat): alpha(kk!1) - delta!1/2 < XX!1(nn) AND XX!1(nn) <= alpha(kk!1) AND nn >= kk!1" )"1" "1" "nn!1" )"1" "1" case "1/nn!1 < delta!1/2" )"1" case "CC - delta!1/2 <= XX!1(nn!1) AND XX!1(nn!1) <= CC + delta!1/2" )"1" case "CC - delta!1 < YY!1(nn!1) AND YY!1(nn!1) < CC + delta!1" )"1" "1" "triangle" )"1" "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))" )"1" assert )"1" "XX!1(nn!1)" )"1" "YY!1(nn!1)" )"1" "1" "1" "1" "abs(f!1(CC) - f!1(YY!1(nn!1))) = abs(f!1(YY!1(nn!1))-f!1(CC))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "xxnn" "XX!1(nn!1)" )"4" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "yynn" "YY!1(nn!1)" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "xxnn" "XX!1(nn!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" case "1/nn!1 <= 1/kk!1" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "lub(A(kk!1))" )"1" expand "least_upper_bound?" )"1" "1" "alpha(kk!1)- delta!1 / 2" )"1" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "j!1" )"2" assert )"2" replace "2" "2" case "CC <= XX!1(j!1)" )"1" assert )"1" replace "1" assert )"1" "XX!1(j!1)" )nil nil ))nil ))nil ))nil )"2" "XX!1(j!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace "1" assert )"1" "XX!1(kk!1)" )"1" "kk!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" replace "2" "CC+delta!1/2" )"2" assert )"2" "2" "s!1" )"2" "2" case "FORALL (ii: posnat): ii >= jj!1 IMPLIES alpha(ii) <= alpha(jj!1)" )"1" case "(EXISTS (jk: posnat): jk >= jj!1 AND 1/jk < delta!1/2)" )"1" "1" "jk!1" )"1" assert )"1" "jk!1" )"1" assert )"1" "alpha(jk!1)" )"1" assert )"1" "jk!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "archimedean" )"2" "delta!1/2" )"2" "2" "max(jj!1,n!1)" )"2" expand "max" )"2" "2" "2" case "1/jj!1 <= 1/n!1" )"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )"2" replace "2" "2" assert )"2" case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES ") "1" "1" assert )"1" "1" expand "subset?" )"1" expand "member" )"1" "1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(ii!1)" )"1" "ii!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "lub(A!1)" )"2" "lub(B!1)" )"2" expand "least_upper_bound?" )"2" "2" "lub(B!1)" )"2" assert )"2" "2" expand "upper_bound?" )"2" "2" "s!2" )"2" expand "subset?" )"2" expand "member" )"2" "s!2" )"2" "s!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" "alpha(1)" )"1" replace -3)"1" case "alpha(1) <= b!1" )"1" assert )"1" "a!1" )"1" assert )"1" "1" "s!1" )"1" "1" replace "1" assert )"1" "1" replace "1" "1" assert )"1" "1" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "XX!1(jj!1)" )"1" assert )"1" "jj!1" )"1" assert )nil nil ))nil ))nil )"2" "jj!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!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 )"2" replace "2" assert )"2" "lub(A(1))" )"2" expand "least_upper_bound?" )"2" "2" "b!1" )"2" assert )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "alpha(1)" )"1" assert )"1" "1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" expand "lower_bound?" )"2" "a!1" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" replace "2" "2" assert )"2" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" replace "1" "1" expand "upper_bound?" )"1" assert )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil )"2" "jj!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!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 )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace -2 -1 rl)"1" assert )"1" "XX!1(kk!1)" )"1" assert )"1" "kk!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!1" )"2" replace -2 -1 rl)"2" "2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "n!1" )"2" "2" "x!1" "y!1" )"2" assert )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "connected_domain" )"2" "a!1" "b!1" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" (skosimp*)"3" (lemma "connected_domain" )"3" "a!1" "b!1" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "epsi!1" )"2" (skosimp*)"2" (inst 2 "N!1" )"2" (skosimp*)"2" (inst + "x!1" "y!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)nil 3399972710";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" ";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" assert )";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" ";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" expand "uniformly_continuous?" )";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" ";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" case " EXISTS (N: posnat): AND xx <= b!1}))):") "1" (skosimp*) (("1" (inst + "1/N!1" ) nil )))"2" (hide 2)"2" case "EXISTS (eps: posreal): FORALL (N: posnat): AND xx <= b!1}))):AND abs(f!1(x) - f!1(y)) >= eps") "1" (skosimp*)"1" (hide 1)"1" (lemma "getem_scaf4" )"1" "(LAMBDA (x,y: real,n:posnat): abs(x - y) < 1 / n AND a!1 <= x AND x <= b!1 AND a!1 <= y AND y <= b!1 AND abs(f!1(x) - f!1(y)) >= eps!1)" )"1" (split -1)"1" (hide -2)"1" "1" "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})" )"1" "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))" )"1" "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"1" case "a!1 <= CC AND CC <= b!1" )"1" "1" expand "continuous?" )"1" "CC" )"1" expand "convergence" )"1" "1" "eps!1/2" )"1" "1" expand "extend" )"1" case "EXISTS (kk: posnat): CC <= alpha(kk) AND alpha(kk) < CC + delta!1/2 AND 1/kk < delta!1/2" )"1" "1" case "EXISTS (nn: posnat): alpha(kk!1) - delta!1/2 < XX!1(nn) AND XX!1(nn) <= alpha(kk!1) AND nn >= kk!1" )"1" "1" "nn!1" )"1" "1" case "1/nn!1 < delta!1/2" )"1" case "CC - delta!1/2 <= XX!1(nn!1) AND XX!1(nn!1) <= CC + delta!1/2" )"1" case "CC - delta!1 < YY!1(nn!1) AND YY!1(nn!1) < CC + delta!1" )"1" "1" "triangle" )"1" "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))" )"1" assert )"1" "XX!1(nn!1)" )"1" "YY!1(nn!1)" )"1" "1" "1" "1" "abs(f!1(CC) - f!1(YY!1(nn!1))) = abs(f!1(YY!1(nn!1))-f!1(CC))" )"1" assert )nil )"2" "2" nil )))))))"2" nil )"3" nil )"4" "4" "xxnn" "XX!1(nn!1)" )"4" nil )))))))"2" nil )"3" nil )"4" "4" "yynn" "YY!1(nn!1)" )"4" nil )))))))))))))"2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil )))))))))))"2" "2" "2" nil )))))))"2" assert )"2" "2" "xxnn" "XX!1(nn!1)" )"2" assert )nil )))))))))"2" assert )"2" assert )"2" "2" case "1/nn!1 <= 1/kk!1" )"1" assert )nil )"2" "2" "2" assert )nil )))))))))))))))))))))"2" "2" "lub(A(kk!1))" )"1" expand "least_upper_bound?" )"1" "1" "alpha(kk!1)- delta!1 / 2" )"1" "1" assert )"1" replace "1" assert )nil )))))"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "j!1" )"2" assert )"2" replace "2" "2" case "CC <= XX!1(j!1)" )"1" assert )"1" replace "1" assert )"1" "XX!1(j!1)" )nil )))))))"2" "XX!1(j!1)" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace "1" assert )"1" "XX!1(kk!1)" )"1" "kk!1" )"1" assert )nil )))))))))))))))"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "2" "j!1" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" replace "2" "CC+delta!1/2" )"2" assert )"2" "2" "s!1" )"2" "2" case "FORALL (ii: posnat): ii >= jj!1 IMPLIES alpha(ii) <= alpha(jj!1)" )"1" case "(EXISTS (jk: posnat): jk >= jj!1 AND 1/jk < delta!1/2)" )"1" "1" "jk!1" )"1" assert )"1" "jk!1" )"1" assert )"1" "alpha(jk!1)" )"1" assert )"1" "jk!1" )nil )))))))))))))))"2" "2" "archimedean" )"2" "delta!1/2" )"2" "2" "max(jj!1,n!1)" )"2" expand "max" )"2" "2" "2" case "1/jj!1 <= 1/n!1" )"1" assert )nil )"2" "2" assert )nil )))))))))))))))))))))))"2" "2" "2" replace "2" assert )"2" replace "2" "2" assert )"2" case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES ") "1" "1" assert )"1" "1" expand "subset?" )"1" expand "member" )"1" "1" "j!1" )"1" assert )nil )))))))))))))"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil )))))))))))"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil )))))))))))))))))))"3" "3" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(ii!1)" )"1" "ii!1" )"1" assert )nil )))))))))))"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil )))))))))))))))))))))"2" "2" "2" "2" "lub(A!1)" )"2" "lub(B!1)" )"2" expand "least_upper_bound?" )"2" "2" "lub(B!1)" )"2" assert )"2" "2" expand "upper_bound?" )"2" "2" "s!2" )"2" expand "subset?" )"2" expand "member" )"2" "s!2" )"2" "s!2" )"2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))"2" expand "extend" )"2" "2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil )))))))))))))))"2" assert )"2" "2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" "alpha(1)" )"1" replace -3)"1" case "alpha(1) <= b!1" )"1" assert )"1" "a!1" )"1" assert )"1" "1" "s!1" )"1" "1" replace "1" assert )"1" "1" replace "1" "1" assert )"1" "1" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "XX!1(jj!1)" )"1" assert )"1" "jj!1" )"1" assert )nil )))))"2" "jj!1" )"2" assert )nil )))))))))))"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil )))))))))))"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))"2" replace "2" assert )"2" "lub(A(1))" )"2" expand "least_upper_bound?" )"2" "2" "b!1" )"2" assert )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" "j!1" )"2" assert )nil )))))))))))))))))))))))))))))))))))"2" "1" )nil )))))))))))))))))"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "alpha(1)" )"1" assert )"1" "1" )nil )))))))))))"2" expand "bounded_below?" )"2" expand "lower_bound?" )"2" "a!1" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" replace "2" "2" assert )"2" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" replace "1" "1" expand "upper_bound?" )"1" assert )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil )))"2" "jj!1" )"2" assert )nil )))))))))))))))))"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil )))))))))))"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))))"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace -2 -1 rl)"1" assert )"1" "XX!1(kk!1)" )"1" assert )"1" "kk!1" )"1" assert )nil )))))))))))))))))"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!1" )"2" replace -2 -1 rl)"2" "2" assert )"2" "2" "j!1" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" (skosimp*)"2" "n!1" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!1" )"2" "y!1" )"2" expand "extend" )"2" nil )))))))))))))))))))"2" (skosimp*)"2" (lemma "connected_domain" )"2" "a!1" "b!1" "y!1" )"2" (assert ) nil )))))))"3" (skosimp*)"3" (lemma "connected_domain" )"3" "a!1" "b!1" "x!1" )"3" (assert ) nil )))))))))))))))"2" (inst + "epsi!1" )"2" (skosimp*)"2" (inst 2 "N!1" )"2" (skosimp*)"2" (inst + "x!1" "y!1" )"2" (assert ) nil )))))))))))))))"3" (hide 2)"3" (skosimp*)"3" (typepred "y!1" )"3" (expand "extend" ) (("3" (ground) nil )))))))))"4" (hide 2)"4" (skosimp*)"4" (typepred "x!1" )"4" (expand "extend" )"4" (ground) nil ))))))))))))))))))))";;; developed with shostak decision procedures") "bool" convergence_functions nil )) nil )nil 3324907680"" (skosimp*)"" (assert )"" (flatten)"" (expand "uniformly_continuous?" )"" (skosimp*)"" case " EXISTS (N: posnat): AND xx <= b!1}))):") "1" (skosimp*) (("1" (inst + "1/N!1" ) nil nil )) nil )"2" (hide 2)"2" case "EXISTS (eps: posreal): FORALL (N: posnat): AND xx <= b!1}))):AND abs(f!1(x) - f!1(y)) >= eps") "1" (skosimp*)"1" (hide 1)"1" (lemma "getem_scaf4" )"1" "(LAMBDA (x,y: real,n:posnat): abs(x - y) < 1 / n AND a!1 <= x AND x <= b!1 AND a!1 <= y AND y <= b!1 AND abs(f!1(x) - f!1(y)) >= eps!1)" )"1" (split -1)"1" (hide -2)"1" "1" "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})" )"1" "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))" )"1" "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"1" case "a!1 <= CC AND CC <= b!1" )"1" "1" expand "continuous?" )"1" "CC" )"1" expand "convergence" )"1" "1" "eps!1/2" )"1" "1" expand "extend" )"1" case "EXISTS (kk: posnat): CC <= alpha(kk) AND alpha(kk) < CC + delta!1/2 AND 1/kk < delta!1/2" )"1" "1" case "EXISTS (nn: posnat): alpha(kk!1) - delta!1/2 < XX!1(nn) AND XX!1(nn) <= alpha(kk!1) AND nn >= kk!1" )"1" "1" "nn!1" )"1" "1" case "1/nn!1 < delta!1/2" )"1" case "CC - delta!1/2 <= XX!1(nn!1) AND XX!1(nn!1) <= CC + delta!1/2" )"1" case "CC - delta!1 < YY!1(nn!1) AND YY!1(nn!1) < CC + delta!1" )"1" "1" "triangle" )"1" "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))" )"1" assert )"1" "XX!1(nn!1)" )"1" "YY!1(nn!1)" )"1" "1" "1" "1" "abs(f!1(CC) - f!1(YY!1(nn!1))) = abs(f!1(YY!1(nn!1))-f!1(CC))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "xxnn" "XX!1(nn!1)" )"4" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "yynn" "YY!1(nn!1)" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "xxnn" "XX!1(nn!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" case "1/nn!1 <= 1/kk!1" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "lub(A(kk!1))" )"1" expand "least_upper_bound?" )"1" "1" "alpha(kk!1)- delta!1 / 2" )"1" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "j!1" )"2" assert )"2" replace "2" "2" case "CC <= XX!1(j!1)" )"1" assert )"1" replace "1" assert )"1" "XX!1(j!1)" )nil nil ))nil ))nil ))nil )"2" "XX!1(j!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace "1" assert )"1" "XX!1(kk!1)" )"1" "kk!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" replace "2" "CC+delta!1/2" )"2" assert )"2" "2" "s!1" )"2" "2" case "FORALL (ii: posnat): ii >= jj!1 IMPLIES alpha(ii) <= alpha(jj!1)" )"1" case "(EXISTS (jk: posnat): jk >= jj!1 AND 1/jk < delta!1/2)" )"1" "1" "jk!1" )"1" assert )"1" "jk!1" )"1" assert )"1" "alpha(jk!1)" )"1" assert )"1" "jk!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "archimedean" )"2" "delta!1/2" )"2" "2" "max(jj!1,n!1)" )"2" expand "max" )"2" "2" "2" case "1/jj!1 <= 1/n!1" )"1" assert )nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )"2" replace "2" "2" assert )"2" case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES ") "1" "1" assert )"1" "1" expand "subset?" )"1" expand "member" )"1" "1" "j!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" "b!1" )"2" expand "upper_bound?" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(ii!1)" )"1" "ii!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "lub(A!1)" )"2" "lub(B!1)" )"2" expand "least_upper_bound?" )"2" "2" "lub(B!1)" )"2" assert )"2" "2" expand "upper_bound?" )"2" "2" "s!2" )"2" expand "subset?" )"2" expand "member" )"2" "s!2" )"2" "s!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "extend" )"2" "2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"2" expand "greatest_lower_bound?" )"2" "2" expand "lower_bound?" )"2" "alpha(1)" )"1" replace -3)"1" case "alpha(1) <= b!1" )"1" assert )"1" "a!1" )"1" assert )"1" "1" "s!1" )"1" "1" replace "1" assert )"1" "1" replace "1" "1" assert )"1" "1" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "XX!1(jj!1)" )"1" assert )"1" "jj!1" )"1" assert )nil nil ))nil ))nil )"2" "jj!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!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 )"2" replace "2" assert )"2" "lub(A(1))" )"2" expand "least_upper_bound?" )"2" "2" "b!1" )"2" assert )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "alpha(1)" )"1" assert )"1" "1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_below?" )"2" expand "lower_bound?" )"2" "a!1" )"2" "2" "s!1" )"2" "2" replace "2" assert )"2" "2" replace "2" "2" assert )"2" "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})" )"1" expand "least_upper_bound?" )"1" "1" replace "1" "1" expand "upper_bound?" )"1" assert )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil )"2" "jj!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" "XX!1(jj!1)" )"1" "jj!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!2" )"2" "2" "j!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 )"2" "2" "1" expand "nonempty?" )"1" expand "empty?" )"1" expand "member" )"1" replace -2 -1 rl)"1" assert )"1" "XX!1(kk!1)" )"1" assert )"1" "kk!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "bounded_above?" )"2" expand "upper_bound?" )"2" "b!1" )"2" "2" "s!1" )"2" replace -2 -1 rl)"2" "2" assert )"2" "2" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" "n!1" )"2" "2" "x!1" "y!1" )"2" assert )"2" "x!1" )"2" "y!1" )"2" expand "extend" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "connected_domain" )"2" "a!1" "b!1" "y!1" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" (skosimp*)"3" (lemma "connected_domain" )"3" "a!1" "b!1" "x!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "epsi!1" )"2" (skosimp*)"2" (inst 2 "N!1" )"2" (skosimp*)"2" (inst + "x!1" "y!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*)"3" (typepred "y!1" )"3" (expand "extend" ) (("3" (ground) nil nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skosimp*)"4" (typepred "x!1" )"4" (expand "extend" ) (("4" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" convergence_functions nil )) nil )nil 3302349666"" (skosimp*)"" (assert )"" (flatten)"" (expand "uniformly_continuous?" )"" (skosimp*)"" case " EXISTS (N: posnat): AND xx <= b!1}))):") "1" (skosimp*) (("1" (inst + "1/N!1" ) nil nil )) nil )"2" (hide 2)"2" case "EXISTS (eps: posreal): FORALL (N: posnat): AND xx <= b!1}))):AND abs(f!1(x) - f!1(y)) >= eps") "1" (skosimp*)"1" (hide 1)"1" (lemma "getem_prep4" )"1" "(LAMBDA (x,y: real,n:posnat): abs(x - y) < 1 / n AND a!1 <= x AND x <= b!1 AND a!1 <= y AND y <= b!1 AND abs(f!1(x) - f!1(y)) >= eps!1)" )"1" (split -1)"1" (hide -2)"1" "1" "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})" )"1" "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))" )"1" "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})" )"1" case "a!1 <= CC AND CC <= b!1" )"1" "1" expand "continuous?" )"1" "CC" )"1" expand "convergence" )"1" "1" "eps!1/2" )"1" "1" expand "extend" )"1" case "EXISTS (kk: posnat): CC <= alpha(kk) AND alpha(kk) < CC + delta!1/2 AND 1/kk < delta!1/2" )"1" "1" case "EXISTS (nn: posnat): alpha(kk!1) - delta!1/2 < XX!1(nn) AND XX!1(nn) <= alpha(kk!1) AND nn >= kk!1" )"1" "1" "nn!1" )"1" "1" case "1/nn!1 < delta!1/2" )"1" case "CC - delta!1/2 <= XX!1(nn!1) AND XX!1(nn!1) <= CC + delta!1/2" )"1" case "CC - delta!1 < YY!1(nn!1) AND YY!1(nn!1) < CC + delta!1" )"1" "1" "triangle" )"1" "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))" )"1" assert )"1" "XX!1(nn!1)" )"1" "YY!1(nn!1)" )"1" "1" "1" "1" "abs(f!1(CC) - f!1(YY!1(nn!1))) = abs(f!1(YY!1(nn!1))-f!1(CC))" )"1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "xxnn" "XX!1(nn!1)" )"4" nil nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil )"4" "4" "yynn" "YY!1(nn!1)" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "connected_domain" )"2" "a!1" "b!1" "CC" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "xxnn" "XX!1(nn!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" assert )"2" "2" case "1/nn!1 <= 1/kk!1" )"1" assert )nil nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "lub(A(kk!1))" )"1" expand "least_upper_bound?" )"1" "1" "alpha(kk!1)- delta!1 / 2" )"1" "1" assert )"1" replace "1" assert )nil nil ))nil ))nil )"2" expand "upper_bound?" )"2" "2" "s!1" )"2" replace "2" assert )"2" "2" "j!1" )"2" assert )"2" replace "2" "2" case "CC <= XX!1(j!1)" )"1" assert )"1" replace
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.737Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
2026-05-26
