| products/Sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: finite_enumeration.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(integral_split_scaf
(IMP_step_fun_def_TCC1 0 (IMP_step_fun_def_TCC1-1 nil 3292238135 ("" (skosimp*) (("" (lemma "connected_domain") (("" (expand "connected?") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_split_scaf nil)) shostak)) (IMP_step_fun_def_TCC2 0 (IMP_step_fun_def_TCC2-1 nil 3292238135 ("" (skosimp*) (("" (lemma "not_one_element") (("" (expand "not_one_element?") (("" (inst?) nil nil)) nil)) nil)) nil) ((not_one_element formula-decl nil integral_split_scaf nil)) shostak)) (diff_step_is_step_on 0 (diff_step_is_step_on-1 nil 3292237292 ("" (skosimp*) (("" (expand "step_function_on?") (("" (skosimp*) (("" (inst - "ii!1") (("" (inst - "ii!1") (("" (skosimp*) (("" (inst + "fv!1-fv!2") (("" (skosimp*) (("" (inst - "x!1") (("" (inst - "x!1") (("" (expand "-") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((step_function_on? const-decl "bool" step_fun_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil nat_types nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (open_interval type-eq-decl nil intervals_real "reals/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (se_not_on_TCC1 0 (se_not_on_TCC1-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (se_not_on 0 (se_not_on-1 nil 3282569138 ("" (skosimp*) (("" (typepred "x!1") (("" (case "ii!1 = jj!1") (("1" (assert) nil nil) ("2" (lemma "parts_order[T]") (("2" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1") (("2" (assert) (("2" (case "ii!1 + 1 = jj!1") (("1" (assert) nil nil) ("2" (assert) (("2" (replace -4) (("2" (hide -4) (("2" (lemma "parts_order[T]") (("2" (inst - "a!1" "b!1" "P!1" "jj!1" "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((open_interval type-eq-decl nil intervals_real "reals/") (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (parts_order formula-decl nil integral_def nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (find_P_sec_TCC1 0 (find_P_sec_TCC1-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (find_P_sec_TCC2 0 (find_P_sec_TCC2-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (find_P_sec_TCC3 0 (find_P_sec_TCC3-1 nil 3282569216 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, partition[T](a, b), (LAMBDA (x: T): a <= x AND x <= b)]): choose({ii: below(length(d`3) - 1) | seq(d`3)(ii) <= d`4 AND d`4 <= seq(d`3)(1 + ii)}))") (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "part_in[T]") (("1" (inst - "d!1`1" "d!1`2" "d!1`4" "d!1`3") (("1" (assert) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "connected_domain") (("2" (expand "connected?") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (part_in formula-decl nil integral_def 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) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (find_P_sec_TCC4 0 (find_P_sec_TCC4-1 nil 3610725744 ("" (inst + "(LAMBDA (d: [a: T, b: {x: T | a < x}, partition[T](a, b), (LAMBDA (x: T): a <= x AND x <= b)]): choose({ii: below(length(d`3) - 1) | seq(d`3)(ii) <= d`4 AND d`4 <= seq(d`3)(1 + ii)}))") (("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (lemma "part_in[T]") (("" (inst - "d!1`1" "d!1`2" "d!1`4" "d!1`3") (("" (assert) (("" (assert) (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (part_in formula-decl nil integral_def 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) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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) (T formal-subtype-decl nil integral_split_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (find_P_sec_lem_TCC1 0 (find_P_sec_lem_TCC1-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (find_P_sec_lem_TCC2 0 (find_P_sec_lem_TCC2-1 nil 3282569216 ("" (skosimp*) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers 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)) shostak)) (find_P_sec_lem 0 (find_P_sec_lem-1 nil 3282569175 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (find_P_sec_in_TCC1 0 (find_P_sec_in_TCC1-1 nil 3282569217 ("" (skosimp*) (("" (assert) (("" (typepred "x!1") (("" (assert) nil nil)) nil)) nil)) 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (partition type-eq-decl nil integral_def nil) (open_interval type-eq-decl nil intervals_real "reals/")) shostak)) (find_P_sec_in 0 (find_P_sec_in-1 nil 3282569204 ("" (skosimp*) (("" (typepred "find_P_sec(a!1, b!1, P!1, x!1)") (("1" (name-replace "FP" "find_P_sec(a!1, b!1, P!1, x!1)") (("1" (typepred "x!1") (("1" (case-replace "x!1 = seq(P!1)(FP) ") (("1" (hide -1) (("1" (hide -5) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "ii!1+1" "FP") (("1" (assert) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "FP" "ii!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "x!1 = seq(P!1)(FP+1) ") (("1" (hide -7) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "FP+1" "ii!1") (("1" (assert) (("1" (lemma "parts_order[T]") (("1" (inst - "a!1" "b!1" "P!1" "ii!1+1" "FP") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "parts_disjoint[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil) ((open_interval type-eq-decl nil intervals_real "reals/") (find_P_sec const-decl "{ii: below(length(P) - 1) | seq(P)(ii) <= xx AND xx <= seq(P)(ii + 1)}" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (< const-decl "bool" reals 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) (parts_disjoint formula-decl nil integral_def nil) (parts_order formula-decl nil integral_def nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (F1_TCC1 0 (F1_TCC1-1 nil 3280167871 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props 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)) shostak)) (F1_TCC2 0 (F1_TCC2-1 nil 3280167872 ("" (skosimp*) (("" (lemma "connected_domain") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((connected_domain formula-decl nil integral_split_scaf 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)) shostak)) (F1_TCC3 0 (F1_TCC3-1 nil 3280167872 ("" (skosimp*) (("" (assert) nil nil)) nil) ((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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)) shostak)) (F1_TCC4 0 (F1_TCC4-1 nil 3280230046 ("" (skosimp*) (("" (assert) (("" (typepred "f!1") (("" (expand "bnded_on?") (("" (expand "bounded_on_all?") (("" (assert) (("" (expand "bounded_on?") (("" (skosimp*) (("" (inst + "B!1") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (typepred "x!2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (j!1 skolem-const-decl "below(P!1`length - 1)" integral_split_scaf nil) (x!2 skolem-const-decl "closed_interval[T](P!1`seq(j!1), P!1`seq(1 + j!1))" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_on? const-decl "bool" integral_bounded nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (< const-decl "bool" reals nil) (bnded_on? const-decl "bool" integral_bounded nil)) shostak)) (F1_TCC5 0 (F1_TCC5-1 nil 3280230046 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "bnded_on?") (("" (expand "bounded_on?") (("" (expand "bounded_on_all?") (("" (skosimp*) (("" (expand "bounded_on?") (("" (assert) (("" (inst + "B!1") (("" (skosimp*) (("" (inst?) (("" (assert) (("" (typepred "x!2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bnded_on? const-decl "bool" integral_bounded nil) (< const-decl "bool" reals nil) (T formal-subtype-decl nil integral_split_scaf nil) (T_pred const-decl "[real -> boolean]" integral_split_scaf 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_on? const-decl "bool" integral_bounded nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "{x: T | a!1 < x}" integral_split_scaf nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (j!1 skolem-const-decl "below(P!1`length - 1)" integral_split_scaf nil) (x!2 skolem-const-decl "closed_interval[T](finseq_appl[closed_interval[T](a!1, b!1)](P!1)(j!1), finseq_appl[closed_interval[T](a!1, b!1)](P!1)(1 + j!1))" integral_split_scaf nil) (partition type-eq-decl nil integral_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (bounded_on_all? const-decl "bool" integral_bounded nil)) shostak)) (F1_F2_lem_TCC1 0 (F1_F2_lem_TCC1-1 nil 3280838608 ("" (skosimp*) (("" (expand "bnded_on?") (("" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((bnded_on? const-decl "bool" integral_bounded nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integrable_bounded formula-decl nil integral_bounded 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_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil)) shostak)) (F1_F2_lem 0 (F1_F2_lem-3 nil 3306071410 ("" (skosimp*) (("" (prop) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (expand "F1") (("1" (assert) (("1" (inst + "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (expand "F2") (("2" (assert) (("2" (inst + "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (expand "F1") (("1" (assert) (("1" (lift-if) (("1" (lemma "MIN_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (ground) (("1" (lemma "MINj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "connected_domain") (("1" (lemma "integrable_bounded_on_all[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "F2") (("2" (assert) (("2" (lemma "MAX_ALL_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("1" (inst?) (("1" (lift-if) (("1" (ground) (("1" (lemma "MAXj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (connected_domain formula-decl nil integral_split_scaf nil) (bnd_on_lem formula-decl nil integral_bounded nil) (integrable_bounded formula-decl nil integral_bounded nil) (NOT const-decl "[bool -> bool]" booleans nil) (open_interval type-eq-decl nil intervals_real "reals/") (find_P_sec_in formula-decl nil integral_split_scaf nil) (int_minus_int_is_int application-judgement "int" integers nil) (se_not_on formula-decl nil integral_split_scaf nil) (find_P_sec const-decl "{ii: below(length(P) - 1) | seq(P)(ii) <= xx AND xx <= seq(P)(ii + 1)}" integral_split_scaf nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (MINj const-decl "real" integral_bounded 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_split_scaf nil) (T formal-subtype-decl nil integral_split_scaf nil) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (a!1 skolem-const-decl "T" integral_split_scaf nil) (b!1 skolem-const-decl "T" integral_split_scaf nil) (closed_interval type-eq-decl nil intervals_real "reals/") (finite_sequence type-eq-decl nil finite_sequences nil) (partition type-eq-decl nil integral_def nil) (P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split_scaf nil) (f!1 skolem-const-decl "[T -> real]" integral_split_scaf nil) (F1 const-decl "real" integral_split_scaf nil) (step_function_on? const-decl "bool" step_fun_def nil) (MAXj const-decl "real" integral_bounded nil) (F2 const-decl "real" integral_split_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (MINj_lem formula-decl nil integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (MAXj_lem formula-decl nil integral_bounded nil)) nil) (F1_F2_lem-2 nil 3282501343 ("" (skosimp*) (("" (prop) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (expand "F1") (("1" (assert) (("1" (inst + "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (expand "F2") (("2" (assert) (("2" (inst + "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("2" (inst?) (("2" (inst -1 "ii!1" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("3" (inst - "a!1" "b!1") (("3" (assert) (("3" (inst - "P!1") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "bnd_on_lem[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (lemma "integrable_bounded[T]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (expand "F1") (("1" (assert) (("1" (lift-if) (("1" (lemma "MIN_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (ground) (("1" (lemma "MINj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "connected_domain") (("1" (lemma "integrable_bounded_on_all[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "F2") (("2" (assert) (("2" (lemma "MAX_ALL_lem[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) (("1" (inst?) (("1" (lift-if) (("1" (ground) (("1" (lemma "MAXj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all[T]") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bnd_on_lem formula-decl nil integral_bounded nil) (integrable_bounded formula-decl nil integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (step_function_on? const-decl "bool" step_fun_def nil) (MAXj const-decl "real" integral_bounded nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (integrable_bounded_on_all formula-decl nil integral_bounded nil) (MINj_lem formula-decl nil integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (MAXj_lem formula-decl nil integral_bounded nil)) nil) (F1_F2_lem-1 nil 3280168909 ("" (skosimp*) (("" (prop) (("1" (expand "step_function_on?") (("1" (skosimp*) (("1" (expand "F1") (("1" (assert) (("1" (inst + "MINj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst - "P!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil) ("3" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) (("1" (lemma "bnd_on_lem") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "step_function_on?") (("2" (skosimp*) (("2" (expand "F2") (("2" (assert) (("2" (inst + "MAXj(a!1, b!1, P!1, ii!1, f!1)") (("1" (skosimp*) (("1" (lift-if) (("1" (typepred "x!1") (("1" (ground) (("1" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "se_not_on[T]") (("1" (inst?) (("1" (inst -1 "ii!1" "x!1") (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "find_P_sec_in[T]") (("1" (inst - "a!1" "b!1") (("1" (assert) (("1" (inst - "P!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil) ("3" (lemma "bnd_on_lem") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) (("3" (hide 2) (("3" (lemma "integrable_bounded[T]") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (prop) (("1" (expand "F1") (("1" (assert) (("1" (lift-if) (("1" (lemma "MIN_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (ground) (("1" (lemma "MINj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "connected_domain") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "integrable_bounded_on_all") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "F2") (("2" (assert) (("2" (lemma "MAX_ALL_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (lift-if) (("1" (ground) (("1" (lemma "MAXj_lem[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil) ("3" (lemma "integrable_bounded_on_all") (("3" (inst?) (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "integrable_bounded_on_all") (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((integrable_bounded formula-decl nil integral_bounded nil) (MINj const-decl "real" integral_bounded nil) (partition type-eq-decl nil integral_def nil) (bounded_on_all? const-decl "bool" integral_bounded nil) (step_function_on? const-decl "bool" step_fun_def nil) (MAXj const-decl "real" integral_bounded nil) (MIN_ALL_lem formula-decl nil integral_bounded nil) (MINj_lem formula-decl nil integral_bounded nil) (MAX_ALL_lem formula-decl nil integral_bounded nil) (MAXj_lem formula-decl nil integral_bounded nil)) shostak)) (epsilon_is_0 0 (epsilon_is_0-2 nil 3276521074 ("" (skosimp*) (("" (inst - "abs(xv!1)/2") (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (xv!1 skolem-const-decl "real" integral_split_scaf nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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 "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) (posreal nonempty-type-eq-decl nil real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.143 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 |
