| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lebesgue/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 104 kB |
|
Quelle bounded_interval_props.prfSprache: 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<z!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<a!1") (("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<sup(A!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<sup(A!1)") (("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<z!2") (("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)<z!2") (("1" (hide 1) (("1" (typepred "z!2") (("1" (case "sup(B!1)<sup(A!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<a!1") (("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)) 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) ("2" (replace -1) (("2" (hide -1 1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (inst - "b!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (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/") (lower_bound const-decl "bool" bound_defs "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (< const-decl "bool" reals nil) (bounded_interval3 formula-decl nil bounded_interval_props nil) (bounded_interval1 formula-decl nil bounded_interval_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (intersection const-decl "set" sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (disjoint? const-decl "bool" sets nil) (bounded_interval2 formula-decl nil bounded_interval_props nil) (interval? const-decl "bool" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (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/") (bounded? const-decl "bool" real_topology "metric_space/")) shostak)) (bounded_interval5 0 (bounded_interval5-1 nil 3472202242 ("" (skosimp) (("" (lemma "bounded_interval4" ("A" "A!1" "B" "B!1" "a" "a!1" "b" "b!1")) (("" (assert) (("" (expand "<=" -5) (("" (split -5) (("1" (typepred "A!1") (("1" (typepred "B!1") (("1" (expand "bounded_interval?") (("1" (expand "bounded?") (("1" (flatten) (("1" (split -2) (("1" (expand "empty?") (("1" (inst - "b!1") (("1" (assert) nil nil)) nil)) nil) ("2" (split -4) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (flatten) (("2" (skosimp) (("2" (typepred "sup(A!1)") (("2" (typepred "inf(B!1)") (("2" (expand "greatest_lower_bound") (("2" (expand "least_upper_bound") (("2" (expand "upper_bound") (("2" (expand "lower_bound") (("2" (flatten) (("2" (inst - "y!1") (("2" (inst -3 "x!1") (("2" (case "x!1<=y!1") (("1" (expand "<=" -1) (("1" (split) (("1" (propax) nil nil) ("2" (typepred "x!1") (("2" (replace -2) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (inst -17 "y!1") (("2" (expand "intersection") (("2" (expand "member") (("2" (propax) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "disjoint?") (("2" (expand "empty?") (("2" (inst - "b!1") (("2" (expand "intersection") (("2" (expand "member") (("2" (propax) 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) (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) (bounded_interval4 formula-decl nil bounded_interval_props nil) (<= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (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/") (lower_bound const-decl "bool" bound_defs "reals/") (intersection const-decl "set" sets nil) (disjoint? const-decl "bool" sets nil) (upper_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (least_upper_bound const-decl "bool" bound_defs "reals/") (nonempty? const-decl "bool" sets nil) (setof type-eq-decl nil defined_types nil) (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/") (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (bounded? const-decl "bool" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (bounded_interval_disjoint_union1 0 (bounded_interval_disjoint_union1-1 nil 3472200526 ("" (skosimp) (("" (lemma "bounded_interval4" ("A" "A!1" "B" "B!1" "a" "a!1" "b" "b!1")) (("" (expand "<=" -1 2) (("" (replace 1 -1) (("" (split -1) (("1" (lemma "bounded_interval1" ("A" "A!1" "a" "a!1")) (("1" (lemma "bounded_interval1" ("A" "B!1" "a" "b!1")) (("1" (assert) (("1" (flatten) (("1" (hide 1 -2 -3) (("1" (name "XX" "(inf(B!1)+sup(A!1))/2") (("1" (case "sup(A!1)<XX & XX < inf(B!1)") (("1" (flatten) (("1" (expand "union") (("1" (expand "bounded_interval?") (("1" (expand "member") (("1" (flatten) (("1" (expand "interval?") (("1" (inst -8 "a!1" "b!1" "XX") (("1" (assert) (("1" (split -8) (("1" (typepred "sup(A!1)") (("1" (expand "least_upper_bound") (("1" (expand "upper_bound") (("1" (flatten) (("1" (inst - "XX") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "inf(B!1)") (("2" (expand "greatest_lower_bound") (("2" (expand "lower_bound") (("2" (flatten) (("2" (inst - "XX") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil) ("4" (propax) nil nil) ("5" (propax) 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) (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) (bounded_interval4 formula-decl nil bounded_interval_props nil) (bounded_interval1 formula-decl nil bounded_interval_props nil) (real_le_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) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (interval? const-decl "bool" real_topology "metric_space/") (real_plus_real_is_real application-judgement "real" reals nil) (lower_bound const-decl "bool" bound_defs "reals/") (B!1 skolem-const-decl "bounded_interval" bounded_interval_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound const-decl "bool" bound_defs "reals/") (A!1 skolem-const-decl "bounded_interval" bounded_interval_props nil) (XX skolem-const-decl "real" bounded_interval_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonempty? const-decl "bool" sets 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/") (pred type-eq-decl nil defined_types nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (sup_set type-eq-decl nil bounded_reals "reals/") (least_upper_bound const-decl "bool" bound_defs "reals/") (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (<= const-decl "bool" reals nil)) shostak)) (bounded_interval_disjoint_union2 0 (bounded_interval_disjoint_union2-1 nil 3472214456 ("" (skosimp) (("" (lemma "bounded_interval_disjoint_union1" ("A" "A!1" "B" "B!1" "a" "a!1" "b" "b!1")) (("" (assert) (("" (expand "bounded_interval?") (("" (flatten) (("" (expand "union") (("" (expand "member") (("" (expand "interval?") (("" (inst - "a!1" "b!1" "inf(B!1)") (("" (typepred "inf(B!1)") (("" (expand "greatest_lower_bound") (("" (expand "lower_bound") (("" (flatten) (("" (inst - "b!1") (("" (typepred "sup(A!1)") (("" (expand "least_upper_bound") (("" (expand "upper_bound") (("" (flatten) (("" (inst - "a!1") (("" (assert) 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) (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) (bounded_interval_disjoint_union1 formula-decl nil bounded_interval_props nil) (union const-decl "set" sets nil) (interval? const-decl "bool" real_topology "metric_space/") (NOT const-decl "[bool -> bool]" booleans nil) (lower_bound const-decl "bool" bound_defs "reals/") (upper_bound const-decl "bool" bound_defs "reals/") (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/") (inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}" bounded_reals "reals/") (<= const-decl "bool" reals nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (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) (OR const-decl "[bool, bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (bounded_interval_disjoint_union3_TCC1 0 (bounded_interval_disjoint_union3_TCC1-1 nil 3472200220 ("" (skosimp) (("" (expand "bounded_interval?") (("" (flatten) (("" (expand "bounded?") (("" (split -5) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (expand "union") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval? const-decl "bool" real_topology "metric_space/") (bounded? const-decl "bool" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (union const-decl "set" sets nil) (member const-decl "bool" 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (bounded_interval_disjoint_union3 0 (bounded_interval_disjoint_union3-1 nil 3472214689 ("" (skosimp) (("" (typepred "inf(A!1)") (("" (typepred "inf(union[real](A!1, B!1))") (("" (case "inf(union[real](A!1, B!1)) <= inf(A!1)") (("1" (case "inf(A!1)<=inf(union[real](A!1, B!1))") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (expand "greatest_lower_bound") (("2" (expand "lower_bound") (("2" (flatten) (("2" (inst -2 "inf(A!1)") (("2" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (expand "union") (("3" (expand "member") (("3" (split -1) (("1" (inst -3 "z!1") nil nil) ("2" (lemma "bounded_interval1" ("A" "B!1" "a" "z!1")) (("2" (assert) (("2" (flatten) (("2" (lemma "bounded_interval3" ("A" "A!1")) (("2" (split -1) (("1" (lemma "bounded_interval4" ("A" "A!1" "B" "B!1" "a" "a!1" "b" "b!1")) (("1" (assert) nil nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "a!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) ("2" (hide 2) (("2" (expand "greatest_lower_bound") (("2" (expand "lower_bound") (("2" (flatten) (("2" (inst -4 "inf(union[real](A!1, B!1))") (("2" (split -4) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (inst -2 "z!1") (("3" (expand "union") (("3" (expand "member") (("3" (propax) 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/") (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) (set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil) (greatest_lower_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types 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) (lower_bound const-decl "bool" bound_defs "reals/") (z!1 skolem-const-decl "{x: real | union[real](A!1, B!1)(x)}" bounded_interval_props nil) (B!1 skolem-const-decl "bounded_interval" bounded_interval_props nil) (A!1 skolem-const-decl "bounded_interval" bounded_interval_props nil) (bounded_interval3 formula-decl nil bounded_interval_props nil) (empty? const-decl "bool" sets nil) (bounded_interval4 formula-decl nil bounded_interval_props nil) (bounded_interval1 formula-decl nil bounded_interval_props nil) (member const-decl "bool" sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (z!1 skolem-const-decl "{x: real | A!1(x)}" bounded_interval_props nil) (union const-decl "set" sets nil)) shostak)) (bounded_interval_disjoint_union4_TCC1 0 (bounded_interval_disjoint_union4_TCC1-1 nil 3472201355 ("" (skosimp) (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split -5) (("1" (expand "empty?") (("1" (inst - "a!1") (("1" (expand "union") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bounded_interval? const-decl "bool" real_topology "metric_space/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (empty? const-decl "bool" sets nil) (union const-decl "set" sets nil) (member const-decl "bool" 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (bounded? const-decl "bool" real_topology "metric_space/")) nil)) (bounded_interval_disjoint_union4_TCC2 0 (bounded_interval_disjoint_union4_TCC2-1 nil 3472201355 ("" (skosimp) (("" (typepred "B!1") (("" (expand "bounded_interval?") (("" (expand "bounded?") (("" (flatten) (("" (split -2) (("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_interval_disjoint_union4 0 (bounded_interval_disjoint_union4-1 nil 3472215109 ("" (skosimp) (("" (case "sup(union[real](A!1, B!1)) <= sup(B!1)") (("1" (case "sup(B!1)<=sup(union[real](A!1, B!1))") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (typepred "sup(union[real](A!1, B!1))") (("2" (typepred "sup(B!1)") (("2" (expand "least_upper_bound") (("2" (expand "upper_bound") (("2" (flatten) (("2" (inst -2 "sup(union[real](A!1, B!1))") (("2" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (inst -3 "z!1") (("3" (expand "union") (("3" (expand "member") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "sup(B!1)") (("2" (typepred "sup(union[real](A!1, B!1))") (("2" (expand "least_upper_bound") (("2" (expand "upper_bound") (("2" (flatten) (("2" (inst -2 "sup(B!1)") (("2" (split -2) (("1" (propax) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (typepred "z!1") (("3" (expand "union" -1) (("3" (expand "member") (("3" (split -1) (("1" (lemma "bounded_interval1" ("A" "A!1" "a" "z!1")) (("1" (assert) (("1" (flatten) (("1" (lemma "bounded_interval1" ("A" "B!1" "a" "b!1")) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "bounded_interval4" ("A" "A!1" "B" "B!1" "a" "a!1" "b" "b!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -3 "z!1") 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/") (union const-decl "set" sets nil) (sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals "reals/") (least_upper_bound const-decl "bool" bound_defs "reals/") (pred type-eq-decl nil defined_types nil) (sup_set type-eq-decl nil bounded_reals "reals/") (above_bounded const-decl "bool" bounded_reals "reals/") (setof type-eq-decl nil defined_types nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets 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) (upper_bound const-decl "bool" bound_defs "reals/") (A!1 skolem-const-decl "bounded_interval" bounded_interval_props nil) (B!1 skolem-const-decl "bounded_interval" bounded_interval_props nil) (z!1 skolem-const-decl "{x: real | B!1(x)}" bounded_interval_props nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (z!1 skolem-const-decl "{x: real | union[real](A!1, B!1)(x)}" bounded_interval_props nil) (bounded_interval1 formula-decl nil bounded_interval_props nil) (bounded_interval4 formula-decl nil bounded_interval_props nil)) shostak)))
¤ Dauer der Verarbeitung: 0.49 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26