| products/Sources/formale Sprachen/PVS/measure_integration/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: pointwise_convergence.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(pointwise_convergence
(pointwise_bounded_def 0 (pointwise_bounded_def-1 nil 3391993987 ("" (skosimp) (("" (expand "pointwise_bounded?") (("" (expand "pointwise_bounded_above?") (("" (expand "pointwise_bounded_below?") (("" (expand "pointwise?") (("" (split) (("1" (flatten) (("1" (split) (("1" (skosimp) (("1" (inst - "x!1") (("1" (rewrite "bounded_seq_def") (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst - "x!1") (("2" (rewrite "bounded_seq_def") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (rewrite "bounded_seq_def") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_bounded? const-decl "bool" pointwise_convergence nil) (pointwise_bounded_below? const-decl "bool" pointwise_convergence nil) (T formal-type-decl nil pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (bounded_seq_def formula-decl nil convergence_aux "metric_space/") (pointwise? const-decl "bool" pointwise_convergence nil) (pointwise_bounded_above? const-decl "bool" pointwise_convergence nil)) shostak)) (pointwise_bounded_above_TCC1 0 (pointwise_bounded_above_TCC1-1 nil 3391989427 ("" (expand "zero_seq") (("" (expand "pointwise_bounded_above?") (("" (expand "bounded_above?") (("" (expand "pointwise?") (("" (expand "bounded_above?") (("" (expand "fullset") (("" (expand "image") (("" (expand "upper_bound?") (("" (skosimp*) (("" (inst + "0") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_bounded_above? const-decl "bool" pointwise_convergence nil) (pointwise? const-decl "bool" pointwise_convergence nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bounded_above? const-decl "bool" real_fun_preds "reals/") (zero_seq const-decl "real" pointwise_convergence nil)) nil)) (pointwise_bounded_below_TCC1 0 (pointwise_bounded_below_TCC1-1 nil 3391989427 ("" (expand "pointwise_bounded_below?") (("" (expand "pointwise?") (("" (expand "bounded_below?") (("" (expand "bounded_below?") (("" (skosimp) (("" (inst + "0") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise? const-decl "bool" pointwise_convergence nil) (zero_seq const-decl "real" pointwise_convergence 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) (bounded_below? const-decl "bool" real_fun_preds "reals/") (pointwise_bounded_below? const-decl "bool" pointwise_convergence nil)) nil)) (pointwise_bounded_TCC1 0 (pointwise_bounded_TCC1-1 nil 3391989427 ("" (expand "pointwise_bounded?") (("" (expand "pointwise?") (("" (expand "bounded_seq?") (("" (expand "bounded?") (("" (skosimp) (("" (inst + "0" "1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise? const-decl "bool" pointwise_convergence nil) (bounded? const-decl "bool" metric_space_def "metric_space/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (zero_seq const-decl "real" pointwise_convergence nil) (image const-decl "set[R]" function_image nil) (member const-decl "bool" sets nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (subset? const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (bounded_seq? const-decl "bool" convergence_aux "metric_space/") (pointwise_bounded? const-decl "bool" pointwise_convergence nil)) nil)) (pointwise_bounded_is_bounded_above 0 (pointwise_bounded_is_bounded_above-1 nil 3391989427 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "pointwise_bounded_def") (("" (flatten) nil nil)) nil)) nil)) nil) ((pointwise_bounded nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_bounded? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil pointwise_convergence nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pointwise_bounded_def formula-decl nil pointwise_convergence nil)) nil)) (pointwise_bounded_is_bounded_below 0 (pointwise_bounded_is_bounded_below-1 nil 3391989427 ("" (skosimp) (("" (typepred "x!1") (("" (rewrite "pointwise_bounded_def") (("" (flatten) nil nil)) nil)) nil)) nil) ((pointwise_bounded nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_bounded? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil pointwise_convergence nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pointwise_bounded_def formula-decl nil pointwise_convergence nil)) nil)) (pointwise_convergent_TCC1 0 (pointwise_convergent_TCC1-1 nil 3391989427 ("" (expand "pointwise_convergent?") (("" (inst + "lambda x: 0") (("" (expand "pointwise_convergence?") (("" (skosimp) (("" (rewrite "metric_convergence_def" *) (("" (expand "metric_converges_to") (("" (skosimp) (("" (inst + "0") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil pointwise_convergence nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (member const-decl "bool" sets nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (real_minus_real_is_real application-judgement "real" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (zero_seq const-decl "real" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (metric_convergence_def formula-decl nil metric_space "metric_space/") (pointwise_convergence? const-decl "bool" pointwise_convergence nil) (pointwise_convergent? const-decl "bool" pointwise_convergence nil)) nil)) (pointwise_convergence_sum 0 (pointwise_convergence_sum-1 nil 3392121345 ("" (skosimp*) (("" (expand "pointwise_convergence?") (("" (skosimp) (("" (inst - "x!1") (("" (inst - "x!1") (("" (rewrite "metric_convergence_def" *) (("" (rewrite "metric_convergence_def" *) (("" (rewrite "metric_convergence_def" *) (("" (expand "metric_converges_to") (("" (skosimp) (("" (inst - "r!1/2") (("" (inst - "r!1/2") (("" (skosimp*) (("" (inst + "max(n!1,n!2)") (("" (skosimp) (("" (inst - "i!1") (("" (inst - "i!1") (("" (assert) (("" (expand "ball") (("" (hide -3) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_convergence? const-decl "bool" pointwise_convergence nil) (T formal-type-decl nil pointwise_convergence nil) (metric_convergence_def formula-decl nil metric_space "metric_space/") (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "sequence[[T -> real]]" pointwise_convergence nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (nonneg_rat_max application-judgement "{s: nonneg_rat | s >= q AND s >= r}" real_defs nil) (nat_max application-judgement "{k: nat | i <= k AND j <= k}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (ball_is_metric_open application-judgement "metric_open[real, (LAMBDA (x, y: real): abs(x - y))]" convergence_aux "metric_space/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/")) shostak)) (pointwise_convergence_scal 0 (pointwise_convergence_scal-1 nil 3392121446 ("" (skosimp) (("" (expand "pointwise_convergence?") (("" (skosimp) (("" (inst - "x!1") (("" (rewrite "metric_convergence_def" *) (("" (rewrite "metric_convergence_def" *) (("" (expand "metric_converges_to") (("" (skosimp) (("" (expand "ball") (("" (expand "member") (("" (case-replace "c!1=0") (("1" (expand "*") (("1" (expand "*") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst - "r!1/abs(c!1)") (("1" (skosimp) (("1" (inst + "n!1") (("1" (skosimp) (("1" (inst - "i!1") (("1" (assert) (("1" (expand "*") (("1" (expand "*") (("1" (rewrite "div_mult_pos_lt2" -1) (("1" (rewrite "abs_mult" -1 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "r!1" "py" "abs(c!1)")) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_convergence? const-decl "bool" pointwise_convergence nil) (T formal-type-decl nil pointwise_convergence nil) (* const-decl "sequence[[T -> real]]" pointwise_convergence nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/= const-decl "boolean" notequal nil) (c!1 skolem-const-decl "real" pointwise_convergence nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (r!1 skolem-const-decl "posreal" pointwise_convergence nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_mult formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (ball const-decl "set[T]" metric_space_def "metric_space/") (real_minus_real_is_real application-judgement "real" reals nil) (metric_converges_to const-decl "bool" metric_space_def "metric_space/") (- 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (metric_convergence_def formula-decl nil metric_space "metric_space/")) shostak)) (pointwise_convergence_opp 0 (pointwise_convergence_opp-1 nil 3392115698 ("" (skosimp) (("" (lemma "pointwise_convergence_scal" ("u" "u!1" "f" "f!1" "c" "-1")) (("" (assert) (("" (expand "*") (("" (expand "-") (("" (expand "-" 1) (("" (expand "*" -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (T formal-type-decl nil pointwise_convergence nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (pointwise_convergence_scal formula-decl nil pointwise_convergence nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "sequence[[T -> real]]" pointwise_convergence nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "sequence[[T -> real]]" pointwise_convergence nil) (- const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (pointwise_convergence_diff 0 (pointwise_convergence_diff-1 nil 3392115828 ("" (skosimp) (("" (lemma "pointwise_convergence_opp" ("u" "v!1" "f" "f1!1")) (("" (assert) (("" (lemma "pointwise_convergence_sum" ("u" "u!1" "f0" "f0!1" "v" "-v!1" "f1" "-f1!1")) (("" (assert) (("" (expand "+") (("" (expand "-") (("" (expand "-") (("" (expand "+") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (T formal-type-decl nil pointwise_convergence nil) (pointwise_convergence_opp formula-decl nil pointwise_convergence nil) (- const-decl "sequence[[T -> real]]" pointwise_convergence nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (pointwise_convergence_sum formula-decl nil pointwise_convergence nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "sequence[[T -> real]]" pointwise_convergence nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (- const-decl "sequence[[T -> real]]" pointwise_convergence nil) (- const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (pointwise_convergent_sum 0 (pointwise_convergent_sum-1 nil 3392115342 ("" (skosimp) (("" (typepred "w0!1") (("" (typepred "w1!1") (("" (expand "pointwise_convergent?") (("" (skosimp*) (("" (inst + "f!2+f!1") (("" (lemma "pointwise_convergence_sum" ("u" "w0!1" "v" "w1!1" "f0" "f!2" "f1" "f!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_convergent nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_convergent? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil pointwise_convergence nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (pointwise_convergence_sum formula-decl nil pointwise_convergence nil)) nil)) (pointwise_convergent_scal 0 (pointwise_convergent_scal-1 nil 3392115342 ("" (skosimp) (("" (typepred "w!1") (("" (expand "pointwise_convergent?") (("" (skosimp) (("" (inst + "c!1*f!1") (("" (lemma "pointwise_convergence_scal" ("u" "w!1" "f" "f!1" "c" "c!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_convergent nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_convergent? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil pointwise_convergence nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pointwise_convergence_scal formula-decl nil pointwise_convergence nil) (* const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (pointwise_convergent_opp 0 (pointwise_convergent_opp-1 nil 3392115342 ("" (skosimp) (("" (typepred "w!1") (("" (expand "pointwise_convergent?") (("" (skosimp) (("" (inst + "-f!1") (("" (lemma "pointwise_convergence_opp" ("u" "w!1" "f" "f!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_convergent nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_convergent? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil pointwise_convergence nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (pointwise_convergence_opp formula-decl nil pointwise_convergence nil) (- const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (pointwise_convergent_diff 0 (pointwise_convergent_diff-1 nil 3392115342 ("" (skosimp) (("" (typepred "w0!1") (("" (typepred "w1!1") (("" (expand "pointwise_convergent?") (("" (skosimp*) (("" (inst + "f!2-f!1") (("" (lemma "pointwise_convergence_diff" ("u" "w0!1" "v" "w1!1" "f0" "f!2" "f1" "f!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pointwise_convergent nonempty-type-eq-decl nil pointwise_convergence nil) (pointwise_convergent? const-decl "bool" pointwise_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil pointwise_convergence nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (pointwise_convergence_diff formula-decl nil pointwise_convergence nil)) nil)) (pointwise_convergent_is_pointwise_bounded 0 (pointwise_convergent_is_pointwise_bounded-1 nil 3391989427 ("" (skolem + ("u!1")) (("" (expand "pointwise_bounded?") (("" (expand "pointwise?") (("" (skosimp) (("" (rewrite "bounded_seq_def") (("" (typepred "u!1") (("" (expand "pointwise_convergent?") (("" (skosimp) (("" (expand "pointwise_convergence?") (("" (inst - "x!1") (("" (rewrite "metric_convergence_def" *) (("" (expand "metric_converges_to") (("" (expand "ball") (("" (expand "member") (("" (split) (("1" (inst - "1") (("1" (skosimp) (("1" (expand "bounded_above?") (("1" (case-replace "n!1=0") (("1" (inst + "f!1(x!1)+1") (("1" (skosimp) (("1" (inst - "x!2") (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (case "forall (i:posnat): nonempty?[real] (image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < i})) AND above_bounded[real] (image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < i}))") (("1" (inst - "n!1") (("1" (inst + "max(lub(image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1})),f!1(x!1)+1)") (("1" (typepred "lub(image[nat, real] (LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (case "x!2 (("1" (inst - "u!1(x!2)(x!1)") (("1" (hide-all-but (-2 2)) (("1" (name-replace "LUB" "lub(image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))") (("1" (grind) nil nil)) nil)) nil) ("2" (expand "image") (("2" (inst + "x!2") nil nil)) nil)) nil) ("2" (inst -5 "x!2") (("2" (name-replace "LUB" "lub(image[nat, real] (LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))") (("2" (hide-all-but (-5 3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (replace -1) (("2" (expand "bounded_above?") (("2" (expand "above_bounded") (("2" (skosimp) (("2" (inst + "n!2") (("2" (expand "upper_bound?") (("2" (expand "upper_bound") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "above_bounded") (("2" (expand "bounded_above?") (("2" (skosimp) (("2" (inst + "n!2") (("2" (expand "upper_bound?") (("2" (expand "upper_bound") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "i") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil) ("4" (skosimp*) (("4" (case-replace "j!1=0") (("1" (hide-all-but 1) (("1" (split) (("1" (expand "image") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "u!1(0)(x!1)") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "image") (("2" (expand "above_bounded") (("2" (expand "upper_bound") (("2" (inst + "u!1(0)(x!1)") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (case-replace "j!1>0") (("1" (hide -4 1) (("1" (split) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "image") (("1" (expand "member") (("1" (inst -1 "u!1(0)(x!1)") (("1" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "above_bounded") (("2" (skosimp) (("2" (inst + "max(n!2,u!1(j!1)(x!1))") (("2" (expand "image") (("2" (expand "upper_bound") (("2" (skosimp) (("2" (typepred "z!1") (("2" (skosimp) (("2" (typepred "x!2") (("2" (case-replace "x!2=j!1") (("1" (hide-all-but (-3 1)) (("1" (grind) nil nil)) nil) ("2" (inst - "z!1") (("1" (hide -4) (("1" (grind) nil nil)) nil) ("2" (inst + "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "1") (("2" (skosimp) (("2" (case-replace "n!1>0") (("1" (case "forall (i:posnat): nonempty?[real] (image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < i})) AND below_bounded[real] (image[nat, real](LAMBDA (n: nat): u!1(n)(x!1), {n | n < i}))") (("1" (inst - "n!1") (("1" (flatten) (("1" (expand "bounded_below?") (("1" (typepred "glb(image[nat, real] (LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))") (("1" (name-replace "GLB" "glb(image[nat, real] (LAMBDA (n: nat): u!1(n)(x!1), {n | n < n!1}))") (("1" (inst + "min(GLB,f!1(x!1)-1)") (("1" (expand "greatest_lower_bound?") (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (case "x!2 (("1" (inst - "u!1(x!2)(x!1)") (("1" (hide -3 -4 -5) (("1" (grind) nil nil)) nil) ("2" (expand "image") (("2" (inst + "x!2") nil nil)) nil)) nil) ("2" (inst -6 "x!2") (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.44 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
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.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
