| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 759 kB |
|
Quelle unif_cont_fun.prfSprache: Lisp |
|||||||||||||||
|
(unif_cont_fun (getem_scaf4 0 (getem_scaf4-1 nil 3324907658 ("" (skosimp*) (("" (inst 1 "(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) ((P3!1 skolem-const-decl "[[real, real, posnat] -> bool]" unif_cont_fun nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (choose const-decl "(p)" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) nil)) (unif_cont_interval 0 (unif_cont_interval-5 "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})): abs(x - y) < 1/N IMPLIES abs(f!1(x) - f!1(y)) < epsi!1") (("1" (skosimp*) (("1" (inst + "1/N!1") nil nil)) nil) ("2" (hide 2) (("2" (case "EXISTS (eps: posreal): FORALL (N: posnat): EXISTS (x, y: ({xx: T | a!1 <= xx AND xx <= b!1})): abs(x - y) < 1 / N AND abs(f!1(x) - f!1(y)) >= eps") (("1" (skosimp*) (("1" (hide 1) (("1" (lemma "getem_scaf4") (("1" (inst -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" (split -1) (("1" (hide -2) (("1" (skosimp*) (("1" (name "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})") (("1" (name "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))") (("1" (name "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("1" (case "a!1 <= CC AND CC <= b!1") (("1" (flatten) (("1" (rewrite "continuous_on_def") (("1" (inst -8 "CC") (("1" (expand "convergence") (("1" (flatten) (("1" (inst -9 "eps!1/2") (("1" (skosimp*) (("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" (skosimp*) (("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" (skosimp*) (("1" (inst -12 "nn!1") (("1" (flatten) (("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" (flatten) (("1" (lemma "triangle") (("1" (inst -1 "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))") (("1" (assert) (("1" (inst-cp -26 "XX!1(nn!1)") (("1" (inst -26 "YY!1(nn!1)") (("1" (split -26) (("1" (split -27) (("1" (hide -4 -5 -7 -8 -9 -11) (("1" (case-replace "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" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-5 -6 1)) (("4" (name-replace "xxnn" "XX!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-2 -3 1)) (("4" (name-replace "yynn" "YY!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst - "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -14 1)) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (-1 -2 -3 -5 -6 -7 -8 -9 1)) (("2" (name-replace "xxnn" "XX!1(nn!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (hide-all-but (-3 -6 1)) (("2" (case "1/nn!1 <= 1/kk!1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -9 -11 -12) (("2" (typepred "lub(A(kk!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst -2 "alpha(kk!1)- delta!1 / 2") (("1" (split -2) (("1" (assert) (("1" (replace -9 -1 rl) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -10 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (case "CC <= XX!1(j!1)") (("1" (assert) (("1" (replace -10 * rl) (("1" (assert) (("1" (inst - "XX!1(j!1)") nil nil)) nil)) nil)) nil) ("2" (inst - "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" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -9 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (inst + "kk!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -9 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (reveal -1) (("2" (inst -1 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (replace -5 -) (("2" (inst -2 "CC+delta!1/2") (("2" (assert) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("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" (skosimp*) (("1" (inst 2 "jk!1") (("1" (assert) (("1" (inst -3 "jk!1") (("1" (assert) (("1" (inst -5 "alpha(jk!1)") (("1" (assert) (("1" (inst + "jk!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "archimedean") (("2" (inst -1 "delta!1/2") (("2" (skosimp*) (("2" (inst + "max(jj!1,n!1)") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (case "1/jj!1 <= 1/n!1") (("1" (assert) nil nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -10 -11 2 3) (("2" (skosimp*) (("2" (replace -2 * rl) (("2" (assert) (("2" (replace -3 * rl) (("2" (hide -2 -3) (("2" (assert) (("2" (case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES lub(A) <= lub(B))") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(ii!1)") (("1" (inst + "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (hide -2 -3 -4) (("2" (typepred "lub(A!1)") (("2" (typepred "lub(B!1)") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -4 "lub(B!1)") (("2" (assert) (("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst -5 "s!2") (("2" (inst -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" (ground) (("2" (lemma "connected_domain") (("2" (assert) (("2" (expand "connected?") (("2" (inst -1 "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -6) (("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (inst -1 "alpha(1)") (("1" (replace -3) (("1" (case "alpha(1) <= b!1") (("1" (assert) (("1" (inst -3 "a!1") (("1" (assert) (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -5 * rl) (("1" (assert) (("1" (hide -5) (("1" (replace -5 * rl) (("1" (hide -5) (("1" (assert) (("1" (hide -2 -3 -4) (("1" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -1 "XX!1(jj!1)") (("1" (assert) (("1" (inst -4 "jj!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst 1 "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "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 -4 * rl) (("2" (assert) (("2" (typepred "lub(A(1))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -2 "b!1") (("2" (assert) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (hide -4 -5 -6) (("2" (replace -4 - rl) (("2" (assert) (("2" (skosimp*) (("2" (inst -5 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "alpha(1)") (("1" (assert) (("1" (inst + "1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (expand "lower_bound?") (("2" (inst 1 "a!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (replace -2 -1 rl) (("2" (assert) (("2" (hide -2) (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (expand "upper_bound?") (("1" (assert) (("1" (inst -1 "XX!1(jj!1)") (("1" (inst -3 "jj!1") (("1" (assert) nil nil)) nil) ("2" (inst + "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "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" (skosimp*) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -2 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (assert) (("1" (inst + "kk!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (skosimp*) (("2" (inst -3 "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" (inst -1 "n!1") (("2" (skosimp*) (("2" (inst + "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" (inst -1 "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" (inst -1 "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) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (uniformly_continuous? const-decl "bool" unif_cont_fun nil) (posreal nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil unif_cont_fun nil) (T_pred const-decl "[real -> boolean]" unif_cont_fun nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (b!1 skolem-const-decl "T" unif_cont_fun nil) (a!1 skolem-const-decl "T" unif_cont_fun nil) (= const-decl "[T, T -> boolean]" equalities nil) (bounded_below? const-decl "bool" bounded_real_defs nil) (greatest_lower_bound? const-decl "bool" bounded_real_defs nil) (glb const-decl "{x | greatest_lower_bound?(x, SB)}" bounded_real_defs nil) (jj!1 skolem-const-decl "posnat" unif_cont_fun nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (A skolem-const-decl "[posnat -> [real -> boolean]]" unif_cont_fun nil) (alpha skolem-const-decl "[kk: posnat -> {x | least_upper_bound?(x, A(kk))}]" unif_cont_fun nil) (CC skolem-const-decl "{x | greatest_lower_bound?(x, {alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})}" unif_cont_fun nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (triangle formula-decl nil real_props nil) (connected_domain formula-decl nil unif_cont_fun nil) (connected? const-decl "bool" deriv_domain_def nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (lower_bound? const-decl "bool" bounded_real_defs nil) (B!1 skolem-const-decl "(bounded_above?)" unif_cont_fun nil) (A!1 skolem-const-decl "(bounded_above?)" unif_cont_fun nil) (s!2 skolem-const-decl "(A!1)" unif_cont_fun nil) (ii!1 skolem-const-decl "posnat" unif_cont_fun nil) (XX!1 skolem-const-decl "[posnat -> real]" unif_cont_fun nil) (jj!1 skolem-const-decl "posnat" unif_cont_fun nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (jk!1 skolem-const-decl "posnat" unif_cont_fun nil) (archimedean formula-decl nil real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (posint_max application-judgement "{k: posint | i <= k AND j <= k}" real_defs nil) (posrat_max application-judgement "{s: posrat | s >= q AND s >= r}" real_defs nil) (extend const-decl "R" extend nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (convergence const-decl "bool" convergence_functions nil) (continuous_on_def formula-decl nil continuous_functions nil) (setof type-eq-decl nil defined_types nil) (jj!1 skolem-const-decl "posnat" unif_cont_fun nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (getem_scaf4 formula-decl nil unif_cont_fun nil)) nil) (OWRE "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})): abs(x - y) < 1/N IMPLIES abs(f!1(x) - f!1(y)) < epsi!1") (("1" (skosimp*) (("1" (inst + "1/N!1") nil nil)) nil) ("2" (hide 2) (("2" (case "EXISTS (eps: posreal): FORALL (N: posnat): EXISTS (x, y: ({xx: T | a!1 <= xx AND xx <= b!1})): abs(x - y) < 1 / N IMPLIES abs(f!1(x) - f!1(y)) >= eps") (("1" (skosimp*) (("1" (hide 1) (("1" (lemma "getem_scaf4") (("1" (inst -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" (split -1) (("1" (hide -2) (("1" (skosimp*) (("1" (name "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})") (("1" (name "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))") (("1" (name "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("1" (case "a!1 <= CC AND CC <= b!1") (("1" (flatten) (("1" (expand "continuous?") (("1" (inst -8 "CC") (("1" (expand "convergence") (("1" (flatten) (("1" (inst -9 "eps!1/2") (("1" (skosimp*) (("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" (skosimp*) (("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" (skosimp*) (("1" (inst -12 "nn!1") (("1" (flatten) (("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" (flatten) (("1" (lemma "triangle") (("1" (inst -1 "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))") (("1" (assert) (("1" (inst-cp -26 "XX!1(nn!1)") (("1" (inst -26 "YY!1(nn!1)") (("1" (split -26) (("1" (split -27) (("1" (hide -4 -5 -7 -8 -9 -11) (("1" (case-replace "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" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-5 -6 1)) (("4" (name-replace "xxnn" "XX!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-2 -3 1)) (("4" (name-replace "yynn" "YY!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (inst - "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -14 1)) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (-1 -2 -3 -5 -6 -7 -8 -9 1)) (("2" (name-replace "xxnn" "XX!1(nn!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (hide-all-but (-3 -6 1)) (("2" (case "1/nn!1 <= 1/kk!1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -9 -11 -12) (("2" (typepred "lub(A(kk!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst -2 "alpha(kk!1)- delta!1 / 2") (("1" (split -2) (("1" (assert) (("1" (replace -9 -1 rl) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -10 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (case "CC <= XX!1(j!1)") (("1" (assert) (("1" (replace -10 * rl) (("1" (assert) (("1" (inst - "XX!1(j!1)") nil nil)) nil)) nil)) nil) ("2" (inst - "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" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -9 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (inst + "kk!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -9 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (reveal -1) (("2" (inst -1 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (replace -5 -) (("2" (inst -2 "CC+delta!1/2") (("2" (assert) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("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" (skosimp*) (("1" (inst 2 "jk!1") (("1" (assert) (("1" (inst -3 "jk!1") (("1" (assert) (("1" (inst -5 "alpha(jk!1)") (("1" (assert) (("1" (inst + "jk!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "archimedean") (("2" (inst -1 "delta!1/2") (("2" (skosimp*) (("2" (inst + "max(jj!1,n!1)") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (case "1/jj!1 <= 1/n!1") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -10 -11 2 3) (("2" (skosimp*) (("2" (replace -2 * rl) (("2" (assert) (("2" (replace -3 * rl) (("2" (hide -2 -3) (("2" (assert) (("2" (case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES lub(A) <= lub(B))") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(ii!1)") (("1" (inst + "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (hide -2 -3 -4) (("2" (typepred "lub(A!1)") (("2" (typepred "lub(B!1)") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -4 "lub(B!1)") (("2" (assert) (("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst -5 "s!2") (("2" (inst -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" (ground) (("2" (lemma "connected_domain") (("2" (inst -1 "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -6) (("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (inst -1 "alpha(1)") (("1" (replace -3) (("1" (case "alpha(1) <= b!1") (("1" (assert) (("1" (inst -3 "a!1") (("1" (assert) (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -5 * rl) (("1" (assert) (("1" (hide -5) (("1" (replace -5 * rl) (("1" (hide -5) (("1" (assert) (("1" (hide -2 -3 -4) (("1" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -1 "XX!1(jj!1)") (("1" (assert) (("1" (inst -4 "jj!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst 1 "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "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 -4 * rl) (("2" (assert) (("2" (typepred "lub(A(1))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -2 "b!1") (("2" (assert) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (hide -4 -5 -6) (("2" (replace -4 - rl) (("2" (assert) (("2" (skosimp*) (("2" (inst -5 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "alpha(1)") (("1" (assert) (("1" (inst + "1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (expand "lower_bound?") (("2" (inst 1 "a!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (replace -2 -1 rl) (("2" (assert) (("2" (hide -2) (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (expand "upper_bound?") (("1" (assert) (("1" (inst -1 "XX!1(jj!1)") (("1" (inst -3 "jj!1") (("1" (assert) nil nil)) nil) ("2" (inst + "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "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" (skosimp*) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -2 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (assert) (("1" (inst + "kk!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (skosimp*) (("2" (inst -3 "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" (inst -1 "n!1") (("2" (skosimp*) (("2" (inst + "x!1" "y!1") (("2" (assert) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst -1 "a!1" "b!1" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst -1 "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) (unif_cont_interval-4 nil 3399972710 (";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" (skosimp*) ((";;; 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" (flatten) ((";;; 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" (skosimp*) ((";;; Proof unif_cont_interval-4 for formula unif_cont_fun.unif_cont_interval" (case " EXISTS (N: posnat): FORALL (x, y: (extend[real, T, bool, FALSE] ({xx: T | a!1 <= xx AND xx <= b!1}))): abs(x - y) < 1/N IMPLIES abs(f!1(x) - f!1(y)) < epsi!1") (("1" (skosimp*) (("1" (inst + "1/N!1") nil))) ("2" (hide 2) (("2" (case "EXISTS (eps: posreal): FORALL (N: posnat): EXISTS (x, y: (extend[real, T, bool, FALSE] ({xx: T | a!1 <= xx AND xx <= b!1}))): abs(x - y) < 1/N AND abs(f!1(x) - f!1(y)) >= eps") (("1" (skosimp*) (("1" (hide 1) (("1" (lemma "getem_scaf4") (("1" (inst -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" (split -1) (("1" (hide -2) (("1" (skosimp*) (("1" (name "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})") (("1" (name "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))") (("1" (name "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("1" (case "a!1 <= CC AND CC <= b!1") (("1" (flatten) (("1" (expand "continuous?") (("1" (inst -8 "CC") (("1" (expand "convergence") (("1" (flatten) (("1" (inst -9 "eps!1/2") (("1" (skosimp*) (("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" (skosimp*) (("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" (skosimp*) (("1" (inst -12 "nn!1") (("1" (flatten) (("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" (flatten) (("1" (lemma "triangle") (("1" (inst -1 "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))") (("1" (assert) (("1" (inst-cp -26 "XX!1(nn!1)") (("1" (inst -26 "YY!1(nn!1)") (("1" (split -26) (("1" (split -27) (("1" (hide -4 -5 -7 -8 -9 -11) (("1" (case-replace "abs(f!1(CC) - f!1(YY!1(nn!1))) = abs(f!1(YY!1(nn!1))-f!1(CC))") (("1" (assert) nil) ("2" (hide-all-but 1) (("2" (grind) nil))))))) ("2" (propax) nil) ("3" (propax) nil) ("4" (hide-all-but (-5 -6 1)) (("4" (name-replace "xxnn" "XX!1(nn!1)") (("4" (grind) nil))))))) ("2" (propax) nil) ("3" (propax) nil) ("4" (hide-all-but (-2 -3 1)) (("4" (name-replace "yynn" "YY!1(nn!1)") (("4" (grind) nil))))))))))))) ("2" (lemma "connected_domain") (("2" (inst - "a!1" "b!1" "CC") (("2" (assert) nil))))))))))) ("2" (hide-all-but (-1 -2 -14 1)) (("2" (flatten) (("2" (grind) nil))))))) ("2" (assert) (("2" (hide-all-but (-1 -2 -3 -5 -6 -7 -8 -9 1)) (("2" (name-replace "xxnn" "XX!1(nn!1)") (("2" (assert) nil))))))))) ("2" (assert) (("2" (assert) (("2" (hide-all-but (-3 -6 1)) (("2" (case "1/nn!1 <= 1/kk!1") (("1" (assert) nil) ("2" (hide -2 2) (("2" (cross-mult 1) (("2" (assert) nil))))))))))))))))))))) ("2" (hide -9 -11 -12) (("2" (typepred "lub(A(kk!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst -2 "alpha(kk!1)- delta!1 / 2") (("1" (split -2) (("1" (assert) (("1" (replace -9 -1 rl) (("1" (assert) nil))))) ("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -10 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (case "CC <= XX!1(j!1)") (("1" (assert) (("1" (replace -10 * rl) (("1" (assert) (("1" (inst - "XX!1(j!1)") nil))))))) ("2" (inst - "XX!1(j!1)") (("2" (assert) nil))))))))))))))))))))))))))))))))) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -9 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (inst + "kk!1") (("1" (assert) nil))))))))))))))) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -9 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (reveal -1) (("2" (inst -1 "j!1") (("2" (assert) nil))))))))))))))))))))))))))))))))) ("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (replace -5 -) (("2" (inst -2 "CC+delta!1/2") (("2" (assert) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("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" (skosimp*) (("1" (inst 2 "jk!1") (("1" (assert) (("1" (inst -3 "jk!1") (("1" (assert) (("1" (inst -5 "alpha(jk!1)") (("1" (assert) (("1" (inst + "jk!1") nil))))))))))))))) ("2" (hide-all-but 1) (("2" (lemma "archimedean") (("2" (inst -1 "delta!1/2") (("2" (skosimp*) (("2" (inst + "max(jj!1,n!1)") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (case "1/jj!1 <= 1/n!1") (("1" (assert) nil) ("2" (cross-mult 1) (("2" (assert) nil))))))))))))))))))))))) ("2" (hide -1 -2 -3 -4 -5 -10 -11 2 3) (("2" (skosimp*) (("2" (replace -2 * rl) (("2" (assert) (("2" (replace -3 * rl) (("2" (hide -2 -3) (("2" (assert) (("2" (case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES lub(A) <= lub(B))") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil))))))))))))) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil))))))))))) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil))))))))))))))))))) ("3" (hide 2) (("3" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(ii!1)") (("1" (inst + "ii!1") (("1" (assert) nil))))))))))) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil))))))))))))))))))))) ("2" (hide 2) (("2" (skosimp*) (("2" (hide -2 -3 -4) (("2" (typepred "lub(A!1)") (("2" (typepred "lub(B!1)") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -4 "lub(B!1)") (("2" (assert) (("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst -5 "s!2") (("2" (inst -2 "s!2") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (expand "extend") (("2" (ground) (("2" (lemma "connected_domain") (("2" (inst -1 "a!1" "b!1" "CC") (("2" (assert) nil))))))))))))))) ("2" (assert) (("2" (hide -6) (("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (inst -1 "alpha(1)") (("1" (replace -3) (("1" (case "alpha(1) <= b!1") (("1" (assert) (("1" (inst -3 "a!1") (("1" (assert) (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -5 * rl) (("1" (assert) (("1" (hide -5) (("1" (replace -5 * rl) (("1" (hide -5) (("1" (assert) (("1" (hide -2 -3 -4) (("1" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -1 "XX!1(jj!1)") (("1" (assert) (("1" (inst -4 "jj!1") (("1" (assert) nil))))) ("2" (inst + "jj!1") (("2" (assert) nil))))))))))) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil))))))))))) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst 1 "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))) ("2" (replace -4 * rl) (("2" (assert) (("2" (typepred "lub(A(1))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -2 "b!1") (("2" (assert) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (hide -4 -5 -6) (("2" (replace -4 - rl) (("2" (assert) (("2" (skosimp*) (("2" (inst -5 "j!1") (("2" (assert) nil))))))))))))))))))))))))))))))))))) ("2" (inst + "1") nil))))))))))))))))) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "alpha(1)") (("1" (assert) (("1" (inst + "1") nil))))))))))) ("2" (expand "bounded_below?") (("2" (expand "lower_bound?") (("2" (inst 1 "a!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (replace -2 -1 rl) (("2" (assert) (("2" (hide -2) (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (expand "upper_bound?") (("1" (assert) (("1" (inst -1 "XX!1(jj!1)") (("1" (inst -3 "jj!1") (("1" (assert) nil))) ("2" (inst + "jj!1") (("2" (assert) nil))))))))))))))))) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil))))))))))) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -2 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (assert) (("1" (inst + "kk!1") (("1" (assert) nil))))))))))))))))) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (skosimp*) (("2" (inst -3 "j!1") (("2" (assert) nil))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (inst -1 "n!1") (("2" (skosimp*) (("2" (inst + "x!1" "y!1") (("2" (assert) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (expand "extend") (("2" (ground) nil))))))))))))))))))) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (inst -1 "a!1" "b!1" "y!1") (("2" (assert) nil))))))) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst -1 "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") ((convergence const-decl "bool" convergence_functions nil)) nil) (unif_cont_interval-3 nil 3324907680 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "uniformly_continuous?") (("" (skosimp*) (("" (case " EXISTS (N: posnat): FORALL (x, y: (extend[real, T, bool, FALSE] ({xx: T | a!1 <= xx AND xx <= b!1}))): abs(x - y) < 1/N IMPLIES abs(f!1(x) - f!1(y)) < epsi!1") (("1" (skosimp*) (("1" (inst + "1/N!1") nil nil)) nil) ("2" (hide 2) (("2" (case "EXISTS (eps: posreal): FORALL (N: posnat): EXISTS (x, y: (extend[real, T, bool, FALSE] ({xx: T | a!1 <= xx AND xx <= b!1}))): abs(x - y) < 1/N AND abs(f!1(x) - f!1(y)) >= eps") (("1" (skosimp*) (("1" (hide 1) (("1" (lemma "getem_scaf4") (("1" (inst -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" (split -1) (("1" (hide -2) (("1" (skosimp*) (("1" (name "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})") (("1" (name "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))") (("1" (name "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("1" (case "a!1 <= CC AND CC <= b!1") (("1" (flatten) (("1" (expand "continuous?") (("1" (inst -8 "CC") (("1" (expand "convergence") (("1" (flatten) (("1" (inst -9 "eps!1/2") (("1" (skosimp*) (("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" (skosimp*) (("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" (skosimp*) (("1" (inst -12 "nn!1") (("1" (flatten) (("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" (flatten) (("1" (lemma "triangle") (("1" (inst -1 "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))") (("1" (assert) (("1" (inst-cp -26 "XX!1(nn!1)") (("1" (inst -26 "YY!1(nn!1)") (("1" (split -26) (("1" (split -27) (("1" (hide -4 -5 -7 -8 -9 -11) (("1" (case-replace "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" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-5 -6 1)) (("4" (name-replace "xxnn" "XX!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-2 -3 1)) (("4" (name-replace "yynn" "YY!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (inst - "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -14 1)) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (-1 -2 -3 -5 -6 -7 -8 -9 1)) (("2" (name-replace "xxnn" "XX!1(nn!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (hide-all-but (-3 -6 1)) (("2" (case "1/nn!1 <= 1/kk!1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -9 -11 -12) (("2" (typepred "lub(A(kk!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst -2 "alpha(kk!1)- delta!1 / 2") (("1" (split -2) (("1" (assert) (("1" (replace -9 -1 rl) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -10 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (case "CC <= XX!1(j!1)") (("1" (assert) (("1" (replace -10 * rl) (("1" (assert) (("1" (inst - "XX!1(j!1)") nil nil)) nil)) nil)) nil) ("2" (inst - "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" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -9 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (inst + "kk!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -9 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (reveal -1) (("2" (inst -1 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (replace -5 - *rl) (("2" (inst -2 "CC+delta!1/2") (("2" (assert) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("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" (skosimp*) (("1" (inst 2 "jk!1") (("1" (assert) (("1" (inst -3 "jk!1") (("1" (assert) (("1" (inst -5 "alpha(jk!1)") (("1" (assert) (("1" (inst + "jk!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "archimedean") (("2" (inst -1 "delta!1/2") (("2" (skosimp*) (("2" (inst + "max(jj!1,n!1)") (("2" (expand "max") (("2" (lift-if) (("2" (ground) (("2" (case "1/jj!1 <= 1/n!1") (("1" (assert) nil nil) ("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 -4 -5 -10 -11 2 3) (("2" (skosimp*) (("2" (replace -2 * rl) (("2" (assert) (("2" (replace -3 * rl) (("2" (hide -2 -3) (("2" (assert) (("2" (case "(FORALL (A,B: (bounded_above?)): subset?(A,B) IMPLIES lub(A) <= lub(B))") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (inst + "j!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (inst + "b!1") (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(ii!1)") (("1" (inst + "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (hide -2 -3 -4) (("2" (typepred "lub(A!1)") (("2" (typepred "lub(B!1)") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -4 "lub(B!1)") (("2" (assert) (("2" (hide 2) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (expand "subset?") (("2" (expand "member") (("2" (inst -5 "s!2") (("2" (inst -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" (ground) (("2" (lemma "connected_domain") (("2" (inst -1 "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -6) (("2" (typepred "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("2" (expand "greatest_lower_bound?") (("2" (flatten) (("2" (expand "lower_bound?") (("2" (inst -1 "alpha(1)") (("1" (replace -3) (("1" (case "alpha(1) <= b!1") (("1" (assert) (("1" (inst -3 "a!1") (("1" (assert) (("1" (skosimp*) (("1" (typepred "s!1") (("1" (skosimp*) (("1" (replace -5 * rl) (("1" (assert) (("1" (hide -5) (("1" (replace -5 * rl) (("1" (hide -5) (("1" (assert) (("1" (hide -2 -3 -4) (("1" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (inst -1 "XX!1(jj!1)") (("1" (assert) (("1" (inst -4 "jj!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst + "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst 1 "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "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 -4 * rl) (("2" (assert) (("2" (typepred "lub(A(1))") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst -2 "b!1") (("2" (assert) (("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (hide -4 -5 -6) (("2" (replace -4 - rl) (("2" (assert) (("2" (skosimp*) (("2" (inst -5 "j!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "alpha(1)") (("1" (assert) (("1" (inst + "1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_below?") (("2" (expand "lower_bound?") (("2" (inst 1 "a!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (skosimp*) (("2" (replace -2 -1 rl) (("2" (assert) (("2" (hide -2) (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (typepred "lub({xx: real | EXISTS (j: posnat): j >= jj!1 AND xx = XX!1(j)})") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (replace -3 * rl) (("1" (hide -3) (("1" (expand "upper_bound?") (("1" (assert) (("1" (inst -1 "XX!1(jj!1)") (("1" (inst -3 "jj!1") (("1" (assert) nil nil)) nil) ("2" (inst + "jj!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst -1 "XX!1(jj!1)") (("1" (inst + "jj!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!2") (("2" (skosimp*) (("2" (inst -4 "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" (skosimp*) (("2" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (replace -2 -1 rl) (("1" (assert) (("1" (inst -1 "XX!1(kk!1)") (("1" (assert) (("1" (inst + "kk!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_above?") (("2" (expand "upper_bound?") (("2" (inst + "b!1") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -2 -1 rl) (("2" (hide -2) (("2" (assert) (("2" (skosimp*) (("2" (inst -3 "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" (inst -1 "n!1") (("2" (skosimp*) (("2" (inst + "x!1" "y!1") (("2" (assert) (("2" (typepred "x!1") (("2" (typepred "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" (inst -1 "a!1" "b!1" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (lemma "connected_domain") (("3" (inst -1 "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) ((convergence const-decl "bool" convergence_functions nil)) nil) (unif_cont_interval-2 nil 3302349666 ("" (skosimp*) (("" (assert) (("" (flatten) (("" (expand "uniformly_continuous?") (("" (skosimp*) (("" (case " EXISTS (N: posnat): FORALL (x, y: (extend[real, T, bool, FALSE] ({xx: T | a!1 <= xx AND xx <= b!1}))): abs(x - y) < 1/N IMPLIES abs(f!1(x) - f!1(y)) < epsi!1") (("1" (skosimp*) (("1" (inst + "1/N!1") nil nil)) nil) ("2" (hide 2) (("2" (case "EXISTS (eps: posreal): FORALL (N: posnat): EXISTS (x, y: (extend[real, T, bool, FALSE] ({xx: T | a!1 <= xx AND xx <= b!1}))): abs(x - y) < 1/N AND abs(f!1(x) - f!1(y)) >= eps") (("1" (skosimp*) (("1" (hide 1) (("1" (lemma "getem_prep4") (("1" (inst -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" (split -1) (("1" (hide -2) (("1" (skosimp*) (("1" (name "A" "(LAMBDA (kk: posnat): {xx: real | EXISTS (j: posnat): j >= kk AND xx = XX!1(j)})") (("1" (name "alpha" "(LAMBDA (kk: posnat): lub(A(kk)))") (("1" (name "CC" "glb({alphs: real | EXISTS (jj: posnat): alphs = alpha(jj)})") (("1" (case "a!1 <= CC AND CC <= b!1") (("1" (flatten) (("1" (expand "continuous?") (("1" (inst -8 "CC") (("1" (expand "convergence") (("1" (flatten) (("1" (inst -9 "eps!1/2") (("1" (skosimp*) (("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" (skosimp*) (("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" (skosimp*) (("1" (inst -12 "nn!1") (("1" (flatten) (("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" (flatten) (("1" (lemma "triangle") (("1" (inst -1 "f!1(XX!1(nn!1)) -f!1(CC)" "f!1(CC) - f!1(YY!1(nn!1))") (("1" (assert) (("1" (inst-cp -26 "XX!1(nn!1)") (("1" (inst -26 "YY!1(nn!1)") (("1" (split -26) (("1" (split -27) (("1" (hide -4 -5 -7 -8 -9 -11) (("1" (case-replace "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" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-5 -6 1)) (("4" (name-replace "xxnn" "XX!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (hide-all-but (-2 -3 1)) (("4" (name-replace "yynn" "YY!1(nn!1)") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (inst - "a!1" "b!1" "CC") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 -14 1)) (("2" (flatten) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide-all-but (-1 -2 -3 -5 -6 -7 -8 -9 1)) (("2" (name-replace "xxnn" "XX!1(nn!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (assert) (("2" (hide-all-but (-3 -6 1)) (("2" (case "1/nn!1 <= 1/kk!1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -9 -11 -12) (("2" (typepred "lub(A(kk!1))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (inst -2 "alpha(kk!1)- delta!1 / 2") (("1" (split -2) (("1" (assert) (("1" (replace -9 -1 rl) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "upper_bound?") (("2" (skosimp*) (("2" (typepred "s!1") (("2" (replace -10 -1 rl) (("2" (assert) (("2" (skosimp*) (("2" (inst + "j!1") (("2" (assert) (("2" (replace -2) (("2" (hide -2) (("2" (case "CC <= XX!1(j!1)") (("1" (assert) (("1" (replace -10 --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.726 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26