| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/Isabelle/Tools/Argo/ (Beweissystem der NASA Version 6.0.9©) Datei vom 16.11.2025 mit Größe 6 kB |
|
Quelle bounded_interval_props.prf Sprache: Lisp |
|||||||||
|
(bounded_interval_props
(bounded_interval1_TCC1 0 (bounded_interval1_TCC1-1 nil 3472198769 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (flatten) (("" (expand "bounded?") (("" (split) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (bounded? const-decl "bool" real_topology "metric_space/")) nil)) (bounded_interval1_TCC2 0 (bounded_interval1_TCC2-1 nil 3472198769 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (bounded_interval1 0 (bounded_interval1-1 nil 3472198771 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (flatten) (("" (expand "bounded?") (("" (split) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (typepred "inf(A!1)") (("1" (typepred "sup(A!1)") (("1" (assert) (("1" (name-replace "INF" "inf(A!1)") (("1" (name-replace "SUP" "sup(A!1)") (("1" (hide -3 -4 -5) (("1" (expand "least_upper_bound") (("1" (expand "greatest_lower_bound") (("1" (expand "lower_bound") (("1" (expand "upper_bound") (("1" (flatten) (("1" (inst - "a!1") (("1" (inst -3 "a!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (setof type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (<= const-decl "bool" reals nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lower_bound const-decl "bool" bound_defs "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (least_upper_bound const-decl "bool" bound_defs "reals/") (bounded? const-decl "bool" real_topology "metric_space/")) shostak)) (bounded_interval2_TCC1 0 (bounded_interval2_TCC1-1 nil 3472198984 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (assert) (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (nonempty? const-decl "bool" sets nil)) nil)) (bounded_interval2_TCC2 0 (bounded_interval2_TCC2-1 nil 3472198984 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (assert) (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" sets nil)) nil)) (bounded_interval2 0 (bounded_interval2-1 nil 3472198985 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split) (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil) ("2" (flatten) (("2" (hide -1) (("2" (typepred "inf(A!1)") (("2" (typepred "sup(A!1)") (("2" (name-replace "INF" "inf(A!1)") (("2" (name-replace "SUP" "sup(A!1)") (("2" (expand "least_upper_bound") (("2" (expand "greatest_lower_bound") (("2" (expand "upper_bound") (("2" (expand "lower_bound") (("2" (flatten) (("2" (inst -2 "a!1") (("2" (split -2) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (case "a!1 (("1" (hide 1) (("1" (inst -5 "a!1") (("1" (split -5) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "z!2 (("1" (hide 1) (("1" (typepred "z!2") (("1" (expand "interval?") (("1" (inst - "z!2" "z!1" "a!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (nonempty? const-decl "bool" sets nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (lower_bound const-decl "bool" bound_defs "reals/") (< const-decl "bool" reals nil) (interval? const-decl "bool" real_topology "metric_space/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (upper_bound const-decl "bool" bound_defs "reals/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (<= const-decl "bool" reals nil) (setof type-eq-decl nil defined_types nil) (below_bounded const-decl "bool" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/")) shostak)) (bounded_interval3_TCC1 0 (bounded_interval3_TCC1-1 nil 3472199659 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split) (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (nonempty? const-decl "bool" sets nil)) nil)) (bounded_interval3 0 (bounded_interval3-1 nil 3472199660 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split) (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil) ("2" (flatten) (("2" (typepred "inf(A!1)") (("2" (typepred "sup(A!1)") (("2" (hide -7) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (lemma "bounded_interval1" ("a" "x!1" "A" "A!1")) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (nonempty? const-decl "bool" sets nil) (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (inf_set type-eq-decl nil bounded_reals "reals/") (below_bounded const-decl "bool" bounded_reals "reals/") (setof type-eq-decl nil defined_types nil) (<= const-decl "bool" reals nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_interval1 formula-decl nil bounded_interval_props nil) (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (least_upper_bound const-decl "bool" bound_defs "reals/")) shostak)) (bounded_interval4_TCC1 0 (bounded_interval4_TCC1-1 nil 3472213392 ("" (skosimp) (("" (typepred "A!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) nil)) (bounded_interval4_TCC2 0 (bounded_interval4_TCC2-1 nil 3472213392 ("" (skosimp) (("" (typepred "B!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split) (("1" (expand "empty?") (("1" (inst - "b!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval nonempty-type-eq-decl nil real_topology "metric_space/") (bounded_interval? const-decl "bool" real_topology "metric_space/") (set type-eq-decl nil sets 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) (bounded? const-decl "bool" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) nil)) (bounded_interval4 0 (bounded_interval4-1 nil 3472210500 ("" (skosimp) (("" (expand "<=" -4) (("" (split -4) (("1" (typepred "A!1") (("1" (typepred "B!1") (("1" (expand "bounded_interval?") (("1" (flatten) (("1" (hide -1 -3) (("1" (expand "bounded?") (("1" (split) (("1" (expand "empty?") (("1" (inst - "b!1") (("1" (assert) nil nil)) nil)) nil) ("2" (split) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (typepred "sup(A!1)") (("2" (typepred "inf(B!1)") (("2" (expand "greatest_lower_bound") (("2" (expand "lower_bound") (("2" (expand "least_upper_bound") (("2" (expand "upper_bound") (("2" (flatten) (("2" (inst -2 "sup(A!1)") (("2" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (case "z!1 (("1" (hide 1) (("1" (lemma "bounded_interval3" ("A" "A!1")) (("1" (assert) (("1" (expand "<=" -1) (("1" (split -1) (("1" (name "XX" "(max(inf(A!1),z!1)+sup(A!1))/2") (("1" (case "A!1(XX)") (("1" (case "B!1(XX)") (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (inst -17 "XX") (("1" (expand "intersection") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "XX (("1" (case "sup(A!1)<=sup(B!1)") (("1" (lemma "bounded_interval2" ("A" "B!1" "a" "XX")) (("1" (assert) (("1" (inst -8 "z!1") (("1" (name-replace "IB" "inf(B!1)") (("1" (name-replace "IA" "inf(A!1)") (("1" (name-replace "SA" "sup(A!1)") (("1" (hide-all-but (-2 -4 -5 -8 1)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "sup(A!1)") (("2" (typepred "sup(B!1)") (("2" (expand "least_upper_bound") (("2" (expand "upper_bound") (("2" (flatten) (("2" (inst -2 "sup(A!1)") (("2" (split -2) (("1" (assert) (("1" (inst -2 "b!1") (("1" (inst -4 "b!1") (("1" (assert) (("1" (skosimp) (("1" (typepred "z!2") (("1" (case "b!1 (("1" (typepred "A!1") (("1" (expand "bounded_interval?") (("1" (flatten) (("1" (expand "interval?") (("1" (inst - "a!1" "z!2" "b!1") (("1" (assert) (("1" (hide-all-but (-1 -26 -24)) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (inst - "b!1") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (case "sup(A!1) (("1" (hide 1) (("1" (typepred "z!2") (("1" (case "sup(B!1) (("1" (hide 1) (("1" (inst -4 "z!2") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name-replace "SA" "sup(A!1)") (("2" (name-replace "IA" "inf(A!1)") (("2" (hide-all-but (-2 -3 -4 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "bounded_interval2" ("A" "A!1" "a" "XX")) (("2" (assert) (("2" (name-replace "SA" "sup(A!1)") (("2" (name-replace "IA" "inf(A!1)") (("2" (hide-all-but (-1 -2 -3 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "sup(A!1)=a!1") (("1" (typepred "inf(B!1)") (("1" (expand "greatest_lower_bound") (("1" (expand "lower_bound") (("1" (flatten) (("1" (inst -2 "a!1") (("1" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!2") (("3" (case "z!2 (("1" (hide 1) (("1" (typepred "B!1") (("1" (expand "bounded_interval?") (("1" (flatten) (("1" (hide -2) (("1" (expand "interval?") (("1" (inst - "z!2" "b!1" "a!1") (("1" (assert) (("1" (expand "disjoint?") (("1" (expand "empty?") (("1" (inst -19 "a!1") (("1" (expand "intersection") (("1" (expand "member") (("1" (propax) 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) ("2" (hide-all-but (-1 1 -7 -8 -9 -15)) (("2" (lemma "bounded_interval1" ("A" "A!1" "a" "a!1")) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.32Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28