| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: HarmonicSeries.thy Sprache: LispOriginal von: PVS© |
|
||||||
|
(continuous_functions
(continuity_def 0 (continuity_def-2 nil 3445335715 ("" (auto-rewrite ("adherence_fullset[T]" "convergence_def[T]" "continuous?")) (("" (assert) nil nil)) nil) ((convergence_def formula-decl nil lim_of_functions nil) (adherence_fullset formula-decl nil lim_of_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (continuity_def-1 nil 3302273405 ("" (auto-rewrite ("adherence_fullset[T]" "convergence_def[T]" "continuous")) (("" (assert) nil nil)) nil) ((convergence_def formula-decl nil lim_of_functions nil) (adherence_fullset formula-decl nil lim_of_functions nil)) nil)) (continuity_def2 0 (continuity_def2-1 nil 3302273405 ("" (skolem!) (("" (rewrite "convergent_in_domain[T]") (("" (lemma "continuity_def") (("" (inst?) nil nil)) nil)) nil)) nil) ((convergent_in_domain formula-decl nil lim_of_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuity_def formula-decl nil continuous_functions nil)) nil)) (continuous_on_def 0 (continuous_on_def-1 nil 3473503534 ("" (skosimp*) (("" (expand "continuous_on?") (("" (expand "convergence") (("" (split +) (("1" (flatten) (("1" (skosimp*) (("1" (split +) (("1" (hide -1) (("1" (expand "adh") (("1" (expand "extend") (("1" (skosimp*) (("1" (typepred "y!1") (("1" (inst + "y!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst? -) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst + delta!1) (("2" (skosimp*) (("2" (inst?) (("1" (assert) nil nil) ("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (inst?) (("2" (flatten) (("2" (hide -1) (("2" (inst - "epsilon!1") (("2" (skosimp*) (("2" (inst + delta!1) (("2" (skosimp*) (("2" (inst?) (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (continuous_on? const-decl "bool" continuous_functions nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (E!1 skolem-const-decl "setof[T]" continuous_functions nil) (x!1 skolem-const-decl "T" continuous_functions nil) (real_lt_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) (extend const-decl "R" extend nil) (setof type-eq-decl nil defined_types nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (abs_nat formula-decl nil abs_lems "reals/") (adh const-decl "setof[real]" convergence_functions nil) (convergence const-decl "bool" convergence_functions nil)) shostak)) (sum_continuous 0 (sum_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "sum_fun_convergent[T]")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (sum_fun_convergent formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (diff_continuous 0 (diff_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "diff_fun_convergent[T]")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (diff_fun_convergent formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (prod_continuous 0 (prod_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "prod_fun_convergent[T]")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (prod_fun_convergent formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (const_continuous 0 (const_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "const_fun_convergent[T]" "adherence_fullset[T]")) nil nil) ((T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (adherence_fullset formula-decl nil lim_of_functions nil) (const_fun_convergent formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (scal_continuous 0 (scal_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "scal_fun_convergent[T]")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (scal_fun_convergent formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (neg_continuous 0 (neg_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "neg_fun_convergent[T]")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (neg_fun_convergent formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (div_continuous 0 (div_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite continuity_def2) (("" (rewrite continuity_def2) (("" (rewrite continuity_def2) (("" (lemma "convergent_in_domain[T]") (("" (inst - "g!1" "x0!1") (("" (assert) (("" (lemma "convergent_in_domain[T]") (("" (inst - "f!1" "x0!1") (("" (assert) (("" (hide -3 -4) (("" (expand "convergent?") (("" (inst + "f!1(x0!1)/g!1(x0!1)") (("" (lemma "cv_div[T]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuity_def2 formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (convergent? const-decl "bool" lim_of_functions nil) (cv_div formula-decl nil lim_of_functions nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (convergent_in_domain formula-decl nil lim_of_functions nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil)) nil)) (inv_continuous 0 (inv_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite continuity_def2) (("" (rewrite continuity_def2) (("" (rewrite "convergent_in_domain[T]") (("" (lemma "cv_inv[T]") (("" (inst?) (("" (expand "convergent?") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuity_def2 formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (convergent_in_domain formula-decl nil lim_of_functions nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (convergent? const-decl "bool" lim_of_functions nil) (cv_inv formula-decl nil lim_of_functions nil) (/ const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (identity_continuous 0 (identity_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuity_def2" "adherence_fullset[T]" "convergent_identity[T]")) nil nil) ((T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (adherence_fullset formula-decl nil lim_of_functions nil) (convergent_identity formula-decl nil lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil)) nil)) (expt_continuous 0 (expt_continuous-1 nil 3322394322 ("" (skolem 1 ("f" "_" "x0")) (("" (induct "n") (("1" (flatten) (("1" (lemma "const_continuous" ("u" "1")) (("1" (inst - "x0") (("1" (expand "const_fun") (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: T): 1" "g" "f^0")) (("1" (flatten) (("1" (hide -2) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) (("2" (lemma "prod_continuous" ("x0" "x0" "f1" "f" "f2" "f^j!1")) (("2" (assert) (("2" (lemma "extensionality_postulate" ("f" "f * f ^ j!1" "g" "f^(1+j!1)")) (("2" (flatten) (("2" (hide -2) (("2" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "*") (("2" (expand "^") (("2" (expand "^") (("2" (expand "expt" 1 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (^ const-decl "[T -> real]" real_fun_ops "reals/") (nat_induction formula-decl nil naturalnumbers nil) (const_continuous formula-decl nil continuous_functions nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation nil) (extensionality_postulate formula-decl nil functions nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (prod_continuous formula-decl nil continuous_functions nil)) nil)) (sum_set_continuous 0 (sum_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (grind :exclude "convergence" :rewrites ("convergence_sum[T]")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (convergence_sum formula-decl nil convergence_functions nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (diff_set_continuous 0 (diff_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (grind :exclude "convergence" :rewrites ("convergence_diff[T]")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (convergence_diff formula-decl nil convergence_functions nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (prod_set_continuous 0 (prod_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (grind :exclude "convergence" :rewrites ("convergence_prod[T]")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (convergence_prod formula-decl nil convergence_functions nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (const_set_continuous 0 (const_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (grind :exclude ("convergence" "adh") :rewrites ("convergence_const[T]" "member_adherent[T]")) nil nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (convergence_const formula-decl nil convergence_functions nil) (member_adherent formula-decl nil convergence_functions nil) (extend const-decl "R" extend nil)) nil)) (scal_set_continuous 0 (scal_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst - "y!1") (("" (grind :exclude "convergence" :rewrites ("convergence_scal[T]")) nil nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (convergence_scal formula-decl nil convergence_functions nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (neg_set_continuous 0 (neg_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst?) (("" (grind :exclude "convergence" :rewrites ("convergence_neg[T]")) nil nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (convergence_neg formula-decl nil convergence_functions nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (div_set_continuous 0 (div_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (grind :exclude "convergence" :rewrites ("convergence_div[T]")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (convergence_div formula-decl nil convergence_functions nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil)) nil)) (inv_set_continuous 0 (inv_set_continuous-1 nil 3302273405 ("" (skosimp*) (("" (rewrite "continuous_on_def") (("" (rewrite "continuous_on_def") (("" (skosimp*) (("" (inst - "y!1") (("" (grind :exclude "convergence" :rewrites ("convergence_inv[T]")) nil nil)) nil)) nil)) nil)) nil)) nil) ((continuous_on_def formula-decl nil continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (convergence_inv formula-decl nil convergence_functions nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/ const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (identity_set_continuous 0 (identity_set_continuous-1 nil 3302273405 ("" (grind :exclude ("convergence" "adh") :rewrites ("convergence_identity[T]" "member_adherent[T]")) nil nil) ((I_preserves application-judgement "S" identity_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (continuous_on? const-decl "bool" continuous_functions nil) (I const-decl "(bijective?[T, T])" identity nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs 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) (>= 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) (setof type-eq-decl nil defined_types nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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)) nil)) (continuous_def2 0 (continuous_def2-1 nil 3302273405 ("" (skosimp*) (("" (expand "continuous?") (("" (split +) (("1" (flatten) (("1" (expand "continuous_on?") (("1" (expand "continuous?") (("1" (skosimp*) (("1" (inst?) (("1" (inst - "epsilon!1") (("1" (assert) (("1" (skosimp*) (("1" (inst + delta!1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (expand "continuous_on?") (("2" (expand "continuous?") (("2" (skosimp*) (("2" (inst?) (("1" (inst - "epsilon!1") (("1" (skosimp*) (("1" (inst + delta!1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil) ("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "restrict") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions nil) (x!1 skolem-const-decl "T" continuous_functions nil) (x0!1 skolem-const-decl "T" continuous_functions nil) (continuous? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (restrict const-decl "R" restrict nil) (real_lt_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) (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) (continuous_on? const-decl "bool" continuous_functions nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (continuity_subset2 0 (continuity_subset2-1 nil 3302273405 ("" (skosimp*) (("" (expand "continuous?") (("" (expand "continuous?") (("" (expand "continuous_on?") (("" (skosimp*) (("" (inst?) (("" (inst - "epsilon!1") (("" (skosimp*) (("" (inst + "delta!1") (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions nil) (continuous_on? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (continuous? const-decl "bool" continuous_functions nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (continuous_fun_TCC1 0 (continuous_fun_TCC1-1 nil 3302273405 ("" (inst + "I[T]") (("" (rewrite "continuous_def2") (("" (rewrite "identity_set_continuous") (("" (rewrite "subset_reflexive") nil nil)) nil)) nil)) nil) ((continuous_def2 formula-decl nil continuous_functions nil) (identity_set_continuous formula-decl nil continuous_functions nil) (setof type-eq-decl nil defined_types nil) (restrict const-decl "R" restrict nil) (I const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (continuous? const-decl "bool" continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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)) nil)) (sum_fun_continuous 0 (sum_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "sum_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (sum_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (diff_fun_continuous 0 (diff_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "diff_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (diff_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (prod_fun_continuous 0 (prod_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "prod_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (prod_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (const_fun_continuous 0 (const_fun_continuous-1 nil 3302273405 ("" (expand "continuous?") (("" (grind :defs nil :rewrites ("const_continuous")) nil nil)) nil) ((const_continuous formula-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil)) nil)) (scal_fun_continuous 0 (scal_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "scal_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (scal_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (neg_fun_continuous 0 (neg_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "neg_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (neg_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (div_fun_continuous 0 (div_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "div_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (nz_continuous_fun type-eq-decl nil continuous_functions nil) (div_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (id_fun_continuous 0 (id_fun_continuous-1 nil 3302273405 ("" (expand "continuous?") (("" (skolem!) (("" (rewrite "identity_continuous") nil nil)) nil)) nil) ((T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (identity_continuous formula-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil)) nil)) (inv_fun_continuous 0 (inv_fun_continuous-1 nil 3302273405 ("" (grind :defs nil :rewrites ("continuous_def2" "inv_set_continuous" "subset_reflexive")) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (nz_continuous_fun type-eq-decl nil continuous_functions nil) (inv_set_continuous formula-decl nil continuous_functions nil) (continuous_def2 formula-decl nil continuous_functions nil)) nil)) (linear_fun_cont 0 (linear_fun_cont-1 nil 3320166004 ("" (skosimp*) (("" (case-replace "(LAMBDA x: m!1 * x + b!1) = m!1 * I[T] + const_fun(b!1)") (("1" (hide -1) (("1" (auto-rewrite "scal_fun_continuous") (("1" (auto-rewrite "sum_fun_continuous") (("1" (auto-rewrite "const_fun_continuous") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ((id_fun_continuous name-judgement "continuous_fun" continuous_functions nil) (scal_fun_continuous application-judgement "continuous_fun" continuous_functions nil) (const_fun_continuous application-judgement "continuous_fun" continuous_functions nil) (real_plus_real_is_real application-judgement "real" reals nil) (sum_fun_continuous application-judgement "continuous_fun" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (I const-decl "(bijective?[T, T])" identity nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (one_over_x_cont_TCC1 0 (one_over_x_cont_TCC1-1 nil 3320157836 ("" (subtype-tcc) nil nil) nil nil)) (one_over_x_cont 0 (one_over_x_cont-1 nil 3320166157 ("" (lemma "inv_fun_continuous") (("" (inst - "I") (("1" (expand "I") (("1" (expand "/") (("1" (flatten) nil nil)) nil)) nil) ("2" (expand "I") (("2" (skosimp*) (("2" (assert) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((id_fun_continuous name-judgement "continuous_fun" continuous_functions nil) (I const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (/= const-decl "boolean" notequal nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (nzreal nonempty-type-eq-decl nil reals nil) (continuous? const-decl "bool" continuous_functions nil) (nz_continuous_fun type-eq-decl nil continuous_functions nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (inv_fun_continuous formula-decl nil continuous_functions nil)) shostak)) (x_to_n_continuous_TCC1 0 (x_to_n_continuous_TCC1-1 nil 3320166272 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (x_to_n_continuous 0 (x_to_n_continuous-2 nil 3306078831 ("" (induct "n" 1) (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "const_fun_continuous") (("1" (inst?) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "(LAMBDA x: x ^ (j!1 + 1)) = (LAMBDA x: x*x ^ j!1)") (("1" (hide -1) (("1" (lemma "prod_fun_continuous") (("1" (inst -1 "(LAMBDA x: x)" "(LAMBDA x: x ^ j!1)") (("1" (expand "*") (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (lemma "id_fun_continuous") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (expand "^" 1) (("2" (expand "expt" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (j!1 skolem-const-decl "nat" continuous_functions nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (id_fun_continuous judgement-tcc nil continuous_functions nil) (I const-decl "(bijective?[T, T])" identity nil) (prod_fun_continuous judgement-tcc nil continuous_functions nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (const_fun_continuous judgement-tcc nil continuous_functions nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (continuous? const-decl "bool" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (pred type-eq-decl nil defined_types 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)) nil) (x_to_n_continuous-1 nil 3302273425 ("" (induct "n" 1) (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "const_fun_continuous[T]") (("1" (inst?) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case-replace "(LAMBDA x: x ^ (j!1 + 1)) = (LAMBDA x: x*x ^ j!1)") (("1" (hide -1) (("1" (lemma "prod_fun_continuous[T]") (("1" (inst -1 "(LAMBDA x: x)" "(LAMBDA x: x ^ j!1)") (("1" (expand "*") (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (lemma "id_fun_continuous[T]") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (apply-extensionality :hide? t) (("2" (expand "^" 1) (("2" (expand "expt" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops "reals/")) nil)) (expt_fun_continuous 0 (expt_fun_continuous-1 nil 3322394393 ("" (skosimp*) (("" (expand "continuous?") (("" (skosimp*) (("" (inst - "x0!1") (("" (lemma "expt_continuous") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (expt_continuous formula-decl nil continuous_functions nil)) shostak)) (sum_cont_fun 0 (sum_cont_fun-1 nil 3393866517 ("" (skosimp*) (("" (assert) (("" (expand "continuous?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (lemma "sum_fun_continuous") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bool nonempty-type-eq-decl nil booleans nil) (continuous_fun nonempty-type-eq-decl nil continuous_functions nil) (sum_fun_continuous judgement-tcc nil continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (continuous? const-decl "bool" continuous_functions nil)) shostak)) (diff_cont_fun 0 (diff_cont_fun-1 nil 3393866553 ("" (skosimp*) (("" (expand "continuous?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (rewrite "diff_continuous") nil nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (diff_continuous formula-decl nil continuous_functions nil)) shostak)) (prod_cont_fun 0 (prod_cont_fun-1 nil 3393866579 ("" (skosimp*) (("" (expand "continuous?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (rewrite "prod_continuous") nil nil)) nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (prod_continuous formula-decl nil continuous_functions nil)) shostak)) (const_cont_fun 0 (const_cont_fun-1 nil 3393866606 ("" (skosimp*) (("" (lemma "const_fun_continuous") (("" (inst?) nil nil)) nil)) nil) ((const_fun_continuous judgement-tcc nil continuous_functions 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)) shostak)) (scal_cont_fun 0 (scal_cont_fun-1 nil 3393866656 ("" (skosimp*) (("" (expand "continuous?") (("" (skosimp*) (("" (inst -1 "x0!1") (("" (rewrite "scal_continuous") nil nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (scal_continuous formula-decl nil continuous_functions nil)) shostak)) (neg_cont_fun 0 (neg_cont_fun-1 nil 3393866960 ("" (skosimp*) (("" (assert) (("" (expand "continuous?") (("" (skosimp*) (("" (inst?) (("" (rewrite "neg_continuous") nil nil)) nil)) nil)) nil)) nil)) nil) ((neg_continuous formula-decl nil continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (continuous? const-decl "bool" continuous_functions nil)) shostak)) (div_cont_fun 0 (div_cont_fun-1 nil 3393867018 ("" (skosimp*) (("" (assert) (("" (expand "continuous?") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (rewrite "div_continuous") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (div_continuous formula-decl nil continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (continuous? const-decl "bool" continuous_functions nil)) nil)) (inv_cont_fun 0 (inv_cont_fun-1 nil 3393867066 ("" (skosimp*) (("" (expand "continuous?") (("" (skosimp*) (("" (inst -1 "x0!1") (("" (rewrite "inv_continuous") nil nil)) nil)) nil)) nil)) nil) ((continuous? const-decl "bool" continuous_functions 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) (T_pred const-decl "[real -> boolean]" continuous_functions nil) (T formal-subtype-decl nil continuous_functions nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (inv_continuous formula-decl nil continuous_functions nil)) nil)) (identity_cont_fun 0 (identity_cont_fun-1 nil 3393867114 ("" (expand "continuous?") (("" (skosimp*) (("" (rewrite "identity_continuous") nil nil)) nil)) nil) ((T formal-subtype-decl nil continuous_functions nil) (T_pred const-decl "[real -> boolean]" continuous_functions 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) (identity_continuous formula-decl nil continuous_functions nil) (continuous? const-decl "bool" continuous_functions nil)) shostak)) (expt_cont_fun 0 (expt_cont_fun-1 nil 3393867172 --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.77 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 |
