| products/Sources/formale Sprachen/PVS/topology/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: topological_convergence.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(topological_convergence
(limit_TCC1 0 (limit_TCC1-1 nil 3454592307 ("" (existence-tcc) 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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil topological_convergence nil) (sequence type-eq-decl nil sequences nil) (convergent? const-decl "bool" topological_convergence nil) (convergent type-eq-decl nil topological_convergence nil) (convergence? const-decl "bool" topological_convergence nil)) nil)) (limit_lemma 0 (limit_lemma-1 nil 3358827431 ("" (skosimp) (("" (typepred "v!1") (("" (expand "convergent?") (("" (skosimp) (("" (expand "limit") (("" (lemma "epsilon_ax" ("p" "LAMBDA l: convergence?(v!1,l)")) (("" (split -1) (("1" (assert) nil nil) ("2" (inst + "l!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent type-eq-decl nil topological_convergence nil) (convergent? const-decl "bool" topological_convergence nil) (sequence type-eq-decl nil sequences nil) (T formal-type-decl nil topological_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) (convergence? const-decl "bool" topological_convergence nil) (pred type-eq-decl nil defined_types nil) (epsilon_ax formula-decl nil epsilons nil) (limit const-decl "T" topological_convergence nil)) shostak)) (limit_accumulation 0 (limit_accumulation-1 nil 3358827716 ("" (skosimp) (("" (expand "accumulation?") (("" (expand "convergence?") (("" (skosimp*) (("" (inst - "U!1") (("" (assert) (("" (skosimp) (("" (inst + "max(n!1,n!2)") (("" (inst - "max(n!1,n!2)") (("" (expand "max") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((accumulation? const-decl "bool" topological_convergence nil) (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) (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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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) (open nonempty-type-eq-decl nil topology nil) (open? const-decl "bool" topology nil) (S formal-const-decl "topology[T]" topological_convergence nil) (topology nonempty-type-eq-decl nil topology_prelim nil) (topology? const-decl "bool" topology_prelim nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil topological_convergence nil) (convergence? const-decl "bool" topological_convergence nil)) shostak)) (convergence_subsequence 0 (convergence_subsequence-1 nil 3358829042 ("" (skosimp) (("" (expand "subseq?") (("" (expand "convergence?") (("" (skosimp*) (("" (inst - "U!1") (("" (assert) (("" (skosimp) (("" (inst + "n!1") (("" (skosimp) (("" (inst - "f!1(i!1)") (("" (inst - "i!1") (("" (replace -2) (("" (split -1) (("1" (propax) nil nil) ("2" (hide -1 -2 2) (("2" (case "forall n: n <= f!1(n)") (("1" (inst - "i!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (induct "n") (("1" (assert) nil nil) ("2" (skosimp*) (("2" (typepred "f!1") (("2" (expand "strict_increasing?") (("2" (inst - "j!1" "j!1+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) ((subseq? const-decl "bool" subseq 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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (<= const-decl "bool" reals nil) (open nonempty-type-eq-decl nil topology nil) (open? const-decl "bool" topology nil) (S formal-const-decl "topology[T]" topological_convergence nil) (topology nonempty-type-eq-decl nil topology_prelim nil) (topology? const-decl "bool" topology_prelim nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil topological_convergence nil) (convergence? const-decl "bool" topological_convergence nil)) shostak))) ¤ Dauer der Verarbeitung: 0.1 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 |
