| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: library.mllib Sprache: LispOriginal von: PVS© |
|
||||||
|
(integral
(IMP_integral_def_TCC1 0 (IMP_integral_def_TCC1-1 nil 3611671301 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil integral nil)) nil)) (IMP_integral_def_TCC2 0 (IMP_integral_def_TCC2-1 nil 3611671301 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil integral nil)) nil)) (IMP_continuous_functions_more_TCC1 0 (IMP_continuous_functions_more_TCC1-1 nil 3611671301 ("" (skosimp*) (("" (lemma "connected_domain") (("" (expand "connected?") (("" (inst - "x!1" "y!1" "z!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral 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]" integral nil) (T formal-nonempty-subtype-decl nil integral nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def nil)) nil)) (IMP_continuous_functions_more_TCC2 0 (IMP_continuous_functions_more_TCC2-1 nil 3611671301 ("" (lemma "not_one_element") (("" (expand "not_one_element?") (("" (propax) nil nil)) nil)) nil) ((not_one_element? const-decl "bool" deriv_domain_def nil) (not_one_element formula-decl nil integral nil)) nil)) (Integrable?_a_to_a 0 (Integrable?_a_to_a-1 nil 3253535925 ("" (skosimp*) (("" (expand "Integrable?") (("" (propax) nil nil)) nil)) nil) ((Integrable? const-decl "bool" integral_def nil)) nil)) (Integrable?_inside 0 (Integrable?_inside-1 nil 3610710489 ("" (skeep) (("" (case "x < y") (("1" (lemma "integrable?_inside") (("1" (inst - "a" "b" "f" "x" "y") (("1" (assert) (("1" (expand "Integrable?") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "Integrable?") (("2" (assert) nil nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (Integrable? const-decl "bool" integral_def nil) (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) (integrable?_inside formula-decl nil integral_split nil)) shostak)) (Integral_a_to_a_TCC1 0 (Integral_a_to_a_TCC1-1 nil 3253535925 ("" (subtype-tcc) nil nil) ((Integrable? const-decl "bool" integral_def nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (Integral_a_to_a 0 (Integral_a_to_a-1 nil 3253535925 ("" (skosimp*) (("" (expand "Integral") (("" (propax) nil nil)) nil)) nil) ((Integral const-decl "real" integral_def nil)) nil)) (Integral_const_fun 0 (Integral_const_fun-1 nil 3253535925 ("" (skosimp*) (("" (lemma "trichotomy") (("" (inst - "b!1-a!1") (("" (lemma "integral_const_fun") (("" (expand "Integrable?") (("" (expand "Integral") (("" (split -2) (("1" (assert) (("1" (inst - "D!1" "a!1" "b!1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (inst - "D!1" "b!1" "a!1") (("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trichotomy formula-decl nil real_axioms nil) (integral_const_fun formula-decl nil integral_prep nil) (Integral const-decl "real" integral_def nil) (const_fun_continuous application-judgement "continuous_fun" integral nil) (constant_seq1 application-judgement "(convergent?)" convergence_ops nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integrable? const-decl "bool" integral_def nil) (real_times_real_is_real application-judgement "real" reals nil) (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (Integral_const_restrict 0 (Integral_const_restrict-1 nil 3292336721 ("" (skosimp*) (("" (lemma "trichotomy") (("" (inst - "b!1-a!1") (("" (lemma "integral_const_restrict") (("" (expand "Integral") (("" (expand "Integrable?") (("" (assert) (("" (split -2) (("1" (assert) (("1" (inst - "D!1" "a!1" "b!1" "f!1") (("1" (assert) (("1" (split -2) (("1" (lemma "integral_def") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (inst - "D!1" "b!1" "a!1" "f!1") (("3" (assert) (("3" (split -2) (("1" (lemma "integral_def") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trichotomy formula-decl nil real_axioms nil) (integral_const_restrict formula-decl nil integral_prep nil) (Integrable? const-decl "bool" integral_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integral_def formula-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (closed_interval type-eq-decl nil intervals_real "reals/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integral const-decl "real" integral_def nil) (real_times_real_is_real application-judgement "real" reals nil) (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (Integral_rev 0 (Integral_rev-1 nil 3253535925 ("" (skosimp*) (("" (grind :exclude "Integrable?") (("" (expand "Integrable?") (("" (prop) nil nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (Integral const-decl "real" integral_def nil) (minus_real_is_real application-judgement "real" reals nil) (Integrable? const-decl "bool" integral_def nil)) nil)) (continuous_Integrable? 0 (continuous_Integrable?-3 nil 3292321430 ("" (skosimp*) (("" (lemma "continuous_integrable") (("" (lemma "trichotomy") (("" (inst -1 "b!1-a!1") (("" (expand "Integrable?") (("" (split -1) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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_integrable formula-decl nil integral_cont nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (closed_interval type-eq-decl nil intervals_real "reals/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integrable? const-decl "bool" integral_def nil) (trichotomy formula-decl nil real_axioms nil)) nil) (continuous_Integrable?-2 nil 3292320550 ("" (skosimp*) (("" (lemma "cont_integrable") (("" (lemma "trichotomy") (("" (inst -1 "b!1-a!1") (("" (expand "Integrable?") (("" (split -1) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_integrable formula-decl nil integral_cont nil) (Integrable? const-decl "bool" integral_def nil)) nil) (continuous_Integrable?-1 nil 3253535925 ("" (skosimp*) (("" (lemma "continuous_integrable") (("" (lemma "trichotomy") (("" (inst -1 "b!1-a!1") (("" (expand "Integrable?") (("" (split -1) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (inst?) (("3" (assert) (("3" (skosimp*) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_integrable formula-decl nil integral_cont nil) (Integrable? const-decl "bool" integral_def nil)) nil)) (cont_Integrable? 0 (cont_Integrable?-1 nil 3320592805 ("" (skosimp*) (("" (lemma "continuous_Integrable?[T]") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (expand "continuous?" -1) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_Integrable? formula-decl nil integral nil) (continuous? const-decl "bool" continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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)) shostak)) (cont_fun_Integrable? 0 (cont_fun_Integrable?-1 nil 3313938422 ("" (skosimp*) (("" (lemma "continuous_Integrable?") (("" (inst?) (("" (assert) (("" (skosimp*) (("" (expand "continuous?" -1) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_Integrable? formula-decl nil integral nil) (continuous? const-decl "bool" continuous_functions nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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)) (Integral_scal 0 (Integral_scal-1 nil 3253535925 ("" (skosimp*) (("" (case-replace "D!1 = 0") (("1" (assert) (("1" (expand "*") (("1" (lemma "Integral_const_fun") (("1" (inst - "0" "a!1" "b!1") (("1" (flatten) (("1" (expand "const_fun") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "trichotomy") (("2" (inst -1 "b!1 - a!1") (("2" (expand "Integrable?") (("2" (expand "Integral") (("2" (split -1) (("1" (assert) (("1" (rewrite "integral_scal") nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (lemma "integral_scal") (("3" (inst -1 "D!1" "b!1" "a!1" "f!1") (("3" (assert) (("3" (flatten) (("3" (assert) 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) (= const-decl "[T, T -> boolean]" equalities 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) (* const-decl "[T -> real]" real_fun_ops "reals/") (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (Integral_const_fun formula-decl nil integral nil) (real_minus_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Integral const-decl "real" integral_def nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integral_scal formula-decl nil integral_prep nil) (Integrable? const-decl "bool" integral_def nil) (trichotomy formula-decl nil real_axioms nil)) nil)) (Integral_sum 0 (Integral_sum-1 nil 3253535925 ("" (skosimp*) (("" (lemma "integral_sum") (("" (lemma "trichotomy") (("" (inst -1 "b!1-a!1") (("" (expand "Integrable?") (("" (expand "Integral") (("" (split -1) (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (inst -2 "b!1" "a!1" "f!1" "g!1") (("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (integral_sum formula-decl nil integral_prep nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Integral const-decl "real" integral_def nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Integrable? const-decl "bool" integral_def nil) (trichotomy formula-decl nil real_axioms nil)) nil)) (Integral_diff 0 (Integral_diff-1 nil 3253535925 ("" (skosimp*) (("" (lemma "Integral_sum") (("" (inst -1 "a!1" "b!1" "f!1" "-g!1") (("" (assert) (("" (split -1) (("1" (flatten) (("1" (expand "-") (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (lemma "Integral_scal") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (case-replace "(LAMBDA (x: T): -g!1(x)) = -1* g!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "Integral_scal") (("2" (inst -1 "-1" "a!1" "b!1" "g!1") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "-") (("2" (case-replace "(LAMBDA (x: T): -g!1(x)) = -1* g!1") (("2" (hide-all-but 1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Integral_sum formula-decl nil integral nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (Integral_scal formula-decl nil integral nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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)) (Integral_split 0 (Integral_split-1 nil 3253535925 ("" (skosimp*) (("" (case-replace "a!1 = b!1") (("1" (expand "Integral") (("1" (propax) nil nil)) nil) ("2" (case-replace "b!1 = c!1") (("1" (expand "Integral") (("1" (propax) nil nil)) nil) ("2" (case-replace "a!1 = c!1") (("1" (expand "Integral") (("1" (assert) (("1" (expand "Integrable?") (("1" (assert) (("1" (case-replace "c!1 < b!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "integral_split") (("2" (case "a!1 < b!1 AND b!1 < c!1") (("1" (inst - "a!1" "b!1" "c!1" "f!1") (("1" (flatten) (("1" (assert) (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "a!1 < c!1 AND c!1 < b!1") (("1" (inst - "a!1" "c!1" "b!1" "f!1") (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (case "integrable?(a!1, c!1, f!1)") (("1" (assert) nil nil) ("2" (hide -3 6) (("2" (lemma "integrable?_split") (("2" (inst?) (("2" (inst -1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "b!1 < a!1 AND a!1 < c!1") (("1" (inst - "b!1" "a!1" "c!1" "f!1") (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (case "integrable?(a!1, c!1, f!1)") (("1" (assert) nil nil) ("2" (hide -3 7) (("2" (lemma "integrable?_split") (("2" (inst -1 "b!1" "a!1" "c!1" "f!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "b!1 < c!1 AND c!1 < a!1") (("1" (inst - "b!1" "c!1" "a!1" "f!1") (("1" (flatten) (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (assert) (("1" (assert) (("1" (case "integrable?(c!1, a!1, f!1)") (("1" (assert) nil nil) ("2" (hide -3 8) (("2" (lemma "integrable?_split") (("2" (inst -1 "b!1" "c!1" "a!1" "f!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "c!1 < a!1 AND a!1 < b!1") (("1" (inst - "c!1" "a!1" "b!1" "f!1") (("1" (flatten) (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (assert) (("1" (assert) (("1" (case "integrable?(c!1, a!1, f!1)") (("1" (assert) nil nil) ("2" (hide -3 9) (("2" (lemma "integrable?_split") (("2" (inst -1 "c!1" "a!1" "b!1" "f!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "c!1 < b!1 AND b!1 < a!1") (("1" (inst - "c!1" "b!1" "a!1" "f!1") (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (flatten) (("1" (assert) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 10) (("2" (ground) 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) (= const-decl "[T, T -> boolean]" equalities 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]" integral nil) (T formal-nonempty-subtype-decl nil integral nil) (Integral const-decl "real" integral_def nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (Integrable? const-decl "bool" integral_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integrable? const-decl "bool" integral_def nil) (integrable?_split formula-decl nil integral_split nil) (integral_split formula-decl nil integral_split nil)) nil)) (Integral_chg_one_pt 0 (Integral_chg_one_pt-1 nil 3292336972 ("" (skosimp*) (("" (lemma "trichotomy") (("" (inst - "b!1-a!1") (("" (lemma "integral_chg_one_pt") (("" (expand "Integrable?") (("" (expand "Integral") (("" (split -2) (("1" (assert) (("1" (inst - "a!1" "b!1" "f!1" "yv!1") (("1" (assert) (("1" (inst - "y!1") (("1" (typepred "y!1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) (("3" (inst - "b!1" "a!1" "f!1" "yv!1") (("3" (assert) (("3" (inst - "y!1") (("3" (typepred "y!1") (("3" (assert) (("3" (flatten) (("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trichotomy formula-decl nil real_axioms nil) (integral_chg_one_pt formula-decl nil integral_prep nil) (Integral const-decl "real" integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (Integrable? const-decl "bool" integral_def nil) (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (Integral_ge_0 0 (Integral_ge_0-1 nil 3292337187 ("" (skosimp*) (("" (lemma "integral_ge_0") (("" (inst?) (("" (inst?) (("" (assert) (("" (expand "Integrable?") (("" (expand "Integral") (("" (assert) (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (integral_ge_0 formula-decl nil integral_prep nil) (Integrable? const-decl "bool" integral_def nil) (closed_interval type-eq-decl nil intervals_real "reals/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (Integral const-decl "real" integral_def 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)) shostak)) (Integral_ge_0_open 0 (Integral_ge_0_open-2 nil 3322385346 ("" (expand "Integrable?") (("" (expand "Integral") (("" (skosimp*) (("" (expand "<=" -1) (("" (split -1) (("1" (assert) (("1" (lemma "integral_chg_one_pt" ("a" "a!1" "b" "b!1" "f" "f!1" "yv" "1")) (("1" (assert) (("1" (inst - "a!1") (("1" (assert) (("1" (flatten) (("1" (lemma "integral_chg_one_pt" ("a" "a!1" "b" "b!1" "f" "f!1 WITH [(a!1) := 1]" "yv" "1")) (("1" (assert) (("1" (inst - "b!1") (("1" (assert) (("1" (flatten) (("1" (lemma "integral_ge_0" ("a" "a!1" "b" "b!1" "f" "f!1 WITH [(a!1) := 1, (b!1) := 1]")) (("1" (assert) (("1" (hide-all-but (-7 1)) (("1" (skosimp) (("1" (case-replace "x!1=a!1") (("1" (assert) nil nil) ("2" (case-replace "x!1=b!1") (("1" (assert) nil nil) ("2" (inst - "x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Integral const-decl "real" integral_def nil) (<= const-decl "bool" reals 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (Open_interval type-eq-decl nil intervals_real "reals/") (x!1 skolem-const-decl "closed_interval[T](a!1, b!1)" integral nil) (b!1 skolem-const-decl "T" integral nil) (a!1 skolem-const-decl "T" integral nil) (< const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (closed_interval type-eq-decl nil intervals_real "reals/") (integral_ge_0 formula-decl nil integral_prep nil) (integral_chg_one_pt formula-decl nil integral_prep 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]" integral nil) (T formal-nonempty-subtype-decl nil integral nil) (Integrable? const-decl "bool" integral_def nil)) nil) (Integral_ge_0_open-1 nil 3322385296 ("" (postpone) nil nil) nil shostak)) (Integral_bound 0 (Integral_bound-1 nil 3253535925 ("" (skosimp*) (("" (lemma "integral_bound") (("" (inst?) (("" (inst -1 "M!1" "f!1") (("" (assert) (("" (expand "Integrable?") (("" (expand "Integral") (("" (assert) (("" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (integral_bound formula-decl nil integral_prep nil) (Integrable? const-decl "bool" integral_def nil) (closed_interval type-eq-decl nil intervals_real "reals/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (Integral const-decl "real" integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (Integral_bounded 0 (Integral_bounded-1 nil 3253535925 ("" (skosimp*) (("" (lemma "integral_bound") (("" (expand "Integral") (("" (lemma "trichotomy") (("" (inst -1 "b!1-a!1") (("" (split -1) (("1" (expand "Integrable?") (("1" (assert) (("1" (inst -2 "M!1" "a!1" "b!1" "f!1" "-M!1") (("1" (assert) (("1" (split -2) (("1" (hide -3 -4) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (expand "abs") (("2" (assert) (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil) ("3" (inst -2 "M!1" "b!1" "a!1" "f!1" "-M!1") (("3" (assert) (("3" (split -2) (("1" (hide -3 -4) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand "Integrable?") (("2" (propax) nil nil)) nil) ("3" (skosimp*) (("3" (inst?) (("3" (hide 2) (("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (integral_bound formula-decl nil integral_prep nil) (trichotomy formula-decl nil real_axioms 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) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (closed_interval type-eq-decl nil intervals_real "reals/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Integrable? const-decl "bool" integral_def nil) (abs_nat formula-decl nil abs_lems "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (Integral const-decl "real" integral_def nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (Integral_le 0 (Integral_le-1 nil 3297783496 ("" (skosimp*) (("" (expand "Integral") (("" (assert) (("" (expand "Integrable?") (("" (rewrite "integral_le") nil nil)) nil)) nil)) nil)) nil) ((Integral const-decl "real" integral_def nil) (Integrable? const-decl "bool" integral_def nil) (T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (integral_le formula-decl nil integral_prep nil) (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)) shostak)) (Integrable_bounded_TCC1 0 (Integrable_bounded_TCC1-1 nil 3282493335 ("" (lemma "connected_domain") (("" (skosimp*) (("" (hide -2) (("" (expand "min") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (connected_domain formula-decl nil integral nil)) shostak)) (Integrable_bounded_TCC2 0 (Integrable_bounded_TCC2-1 nil 3282493335 ("" (skosimp*) (("" (lemma "connected_domain") (("" (expand "max") (("" (lift-if) (("" (ground) nil nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)) shostak)) (Integrable_bounded 0 (Integrable_bounded-2 nil 3477657390 ("" (auto-rewrite "xis_lem") (("" (skosimp*) (("" (expand "Integrable?") (("" (lemma "integrable_bounded[T]") (("1" (split -2) (("1" (inst?) (("1" (hide -2) (("1" (replace -1) (("1" (expand "bounded_on?") (("1" (inst + "abs(f!1(a!1))") (("1" (skosimp*) (("1" (assert) (("1" (typepred "x!1") (("1" (expand "min") (("1" (expand "max") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst?) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (inst - "b!1" "a!1" "f!1") (("3" (assert) (("3" (hide -2) (("3" (expand "min") (("3" (expand "max") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (integrable_bounded formula-decl nil integral_bounded nil) (connected? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (closed_interval type-eq-decl nil intervals_real "reals/") (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (bounded_on? const-decl "bool" integral_bounded nil) (connected_domain formula-decl nil integral nil) (Integrable? const-decl "bool" integral_def nil)) nil) (Integrable_bounded-1 nil 3282492658 ("" (skosimp*) (("" (expand "Integrable?") (("" (lemma "integrable_bounded[T]") (("1" (split -2) (("1" (inst?) (("1" (hide -2) (("1" (replace -1) (("1" (expand "bounded_on?") (("1" (inst + "abs(f!1(a!1))") (("1" (skosimp*) (("1" (assert) (("1" (typepred "x!1") (("1" (expand "min") (("1" (expand "max") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst?) (("2" (assert) (("2" (expand "min") (("2" (expand "max") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (inst - "b!1" "a!1" "f!1") (("3" (assert) (("3" (hide -2) (("3" (expand "min") (("3" (expand "max") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((Integrable? const-decl "bool" integral_def nil) (bounded_on? const-decl "bool" integral_bounded nil) (closed_interval type-eq-decl nil intervals_real "reals/") (integrable_bounded formula-decl nil integral_bounded nil)) shostak)) (Integral_neg 0 (Integral_neg-1 nil 3322385450 ("" (skosimp) (("" (lemma "Integral_const_fun" ("a" "a!1" "b" "b!1" "D" "0")) (("" (flatten) (("" (expand "const_fun") (("" (lemma "Integral_diff" ("a" "a!1" "b" "b!1" "g" "f!1" "f" "LAMBDA (x: T): 0")) (("" (assert) (("" (flatten) (("" (assert) (("" (replace -4) (("" (expand "-" 1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-subtype-decl nil integral nil) (T_pred const-decl "[real -> boolean]" integral 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) (Integral_const_fun formula-decl nil integral nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (Integral_diff formula-decl nil integral nil)) nil)) (Integral_restr_eq 0 (Integral_restr_eq-1 nil 3610458272 ("" (skeep) (("" (case-replace "b = a") (("1" (rewrite "Integrable?_a_to_a") (("1" (rewrite "Integrable?_a_to_a") (("1" (rewrite "Integral_a_to_a") (("1" (rewrite "Integral_a_to_a") nil nil)) nil)) nil)) nil) ("2" (lemma "integral_restr_eq") (("2" (case "a < b") (("1" (inst - "a" "b" "f" "g") (("1" (assert) (("1" (split -2) (("1" (flatten) (("1" (expand "Integrable?") (("1" (expand "Integral") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "Integrable?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "Integrable?") (("2" (assert) (("2" (expand "Integral") (("2" (inst - "b" "a" "f" "g") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 4) (("2" (skosimp*) (("2" (inst?) (("2" (assert) 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) (= const-decl "[T, T -> boolean]" equalities 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]" integral nil) (T formal-nonempty-subtype-decl nil integral nil) (Integral_a_to_a formula-decl nil integral nil) (Integrable?_a_to_a formula-decl nil integral nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (Open_interval type-eq-decl nil intervals_real "reals/") (b skolem-const-decl "T" integral nil) (x!1 skolem-const-decl "T" integral nil) (a skolem-const-decl "T" integral nil) (Integral const-decl "real" integral_def nil) (Integrable? const-decl "bool" integral_def nil) (x!1 skolem-const-decl "T" integral nil) (integral_restr_eq formula-decl nil integral_prep nil)) shostak))) ¤ Dauer der Verarbeitung: 0.135 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 |
