| products/sources/formale Sprachen/PVS/probability/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: patch-108.lisp Sprache: LispOriginal von: PVS© |
|
||||||
|
(conditional
(P_TCC1 0 (P_TCC1-1 nil 3322190760 ("" (skosimp) (("" (expand "null?") (("" (propax) nil nil)) nil)) nil) ((null? const-decl "bool" conditional nil)) shostak)) (P_TCC2 0 (P_TCC2-1 nil 3322190760 ("" (skosimp) (("" (split) (("1" (expand "null?") (("1" (typepred "P(B!1)") (("1" (expand ">=" -1) (("1" (expand "<=" -1) (("1" (split -1) (("1" (typepred "P(intersection[T](A!1, B!1))") (("1" (lemma "both_sides_div_pos_le1" ("pz" "P(B!1)" "x" "0" "y" "P(intersection[T](A!1, B!1))")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "P_subset_le" ("A" "intersection[T](A!1, B!1)" "B" "B!1" "P" "P")) (("2" (split -1) (("1" (expand "null?") (("1" (rewrite "div_mult_pos_le1" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((P formal-const-decl "probability_measure" conditional nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (S formal-const-decl "sigma_algebra" conditional nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-nonempty-type-decl nil conditional 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) (intersection const-decl "set" sets nil) (set type-eq-decl nil sets nil) (subset_algebra_intersection application-judgement "(S)" conditional nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (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) (both_sides_div_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (null? const-decl "bool" conditional nil) (div_mult_pos_le1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas_aux "measure_integration/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (P_subset_le formula-decl nil probability_measure nil)) shostak)) (conditional_complement 0 (conditional_complement-1 nil 3322191770 ("" (skosimp) (("" (case "union(intersection(A!1,B!1),intersection(A!1,complement(B!1))) = A!1") (("1" (lemma "P_disjointunion") (("1" (inst - "intersection(A!1, B!1)" "intersection(A!1, complement(B!1))" "_") (("1" (inst - "P") (("1" (expand "P") (("1" (lemma "P_complement" ("A" "B!1")) (("1" (inst - "P") (("1" (expand "null?") (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "P(B!1) = 0") (("1" (assert) (("1" (assert) (("1" (lemma "P0_intersection" ("A" "B!1" "B" "A!1")) (("1" (inst - "P") (("1" (assert) (("1" (rewrite "intersection_commutative") (("1" (assert) (("1" (hide-all-but 1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case-replace "P(complement(B!1)) = 0") (("1" (rewrite "div_cancel2" 2) (("1" (assert) (("1" (lemma "P0_intersection" ("A" "complement(B!1)" "B" "A!1")) (("1" (inst - "P") (("1" (assert) (("1" (rewrite "intersection_commutative") (("1" (assert) (("1" (replace -1) (("1" (replace -4 *) (("1" (case-replace "P(B!1)=1") (("1" (assert) (("1" (split -4) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (rewrite "P_complement") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "div_cancel2" 3) (("2" (assert) (("2" (replace -2) (("2" (split -1) (("1" (rewrite "P_complement" 1) (("1" (assert) (("1" (lemma "div_cancel1" ("n0z" "1-P(B!1)" "x" "P(intersection(A!1, complement(B!1)))")) (("1" (replace -1 -2 :dir rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality :hide? t) (("2" (expand "complement") (("2" (expand "intersection") (("2" (expand "union") (("2" (expand "member") (("2" (case-replace "A!1(x!1)") (("1" (assert) (("1" (flatten) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complement const-decl "set" sets nil) (S formal-const-decl "sigma_algebra" conditional nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (intersection const-decl "set" sets nil) (union const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil conditional nil) (subset_algebra_union application-judgement "(S)" conditional nil) (subset_algebra_intersection application-judgement "(S)" conditional nil) (subset_algebra_complement application-judgement "(S)" conditional nil) (P const-decl "probability" conditional nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (intersection_commutative formula-decl nil sets_lemmas nil) (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (P0_intersection formula-decl nil probability_measure nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_times_real_is_real application-judgement "real" reals nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (div_cancel2 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (null? const-decl "bool" conditional nil) (P_complement formula-decl nil probability_measure nil) (P formal-const-decl "probability_measure" conditional nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability nonempty-type-eq-decl nil probability_measure nil) (<= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types 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) (P_disjointunion formula-decl nil probability_measure nil)) shostak)) (conditional_partition_TCC1 0 (conditional_partition_TCC1-1 nil 3384894049 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (measurable_fullset name-judgement "measurable_set[T, S]" conditional nil) (subset_algebra_fullset name-judgement "(S)" conditional nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas_aux "measure_integration/") (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)) nil)) (conditional_partition 0 (conditional_partition-1 nil 3322222909 ("" (skosimp) (("" (name "SS" "LAMBDA (i:nat): IF i <= n!1 THEN intersection(A!1,BB!1(i)) ELSE emptyset[T] ENDIF") (("" (case "A!1 = IUnion(SS)") (("1" (lemma "P_convergence" ("SS" "SS")) (("1" (inst - "P") (("1" (lemma "zero_tail_series" ("n" "n!1" "a" "P o SS")) (("1" (split -1) (("1" (assert) (("1" (replace -4 -1 rl) (("1" (replace -4) (("1" (replace -3 * rl) (("1" (lemma "convergence_sequences.unique_limit" ("u" "series(P o SS)" "l1" "P(A!1)" "l2" "series(P o SS)(n!1)")) (("1" (assert) (("1" (hide -2 -3 -5 -6) (("1" (hide -2) (("1" (expand "series") (("1" (expand "o ") (("1" (expand "SS") (("1" (rewrite "P_emptyset") (("1" (expand "P" 1 2) (("1" (expand "null?") (("1" (lemma "sigma_eq[nat]" ("low" "0" "high" "n!1" "F" "LAMBDA (x: nat): IF x <= n!1 THEN P(intersection(A!1, BB!1(x))) ELSE 0 ENDIF" "G" "LAMBDA (i_1: nat): IF P(BB!1(i_1)) = 0 THEN 0 ELSE P(intersection(A!1, BB!1(i_1))) / P(BB!1(i_1)) ENDIF * P(BB!1(i_1))")) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1 2) (("2" (skosimp*) (("2" (typepred "n!2") (("2" (assert) (("2" (case-replace "P(BB!1(n!2)) = 0") (("1" (lemma "P_subset_le" ("A" "intersection(A!1, BB!1(n!2))" "B" "BB!1(n!2)")) (("1" (inst - "P") (("1" (split) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "intersection") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 2) (("2" (skosimp) (("2" (expand "SS") (("2" (assert) (("2" (expand "o") (("2" (lemma "P_emptyset") (("2" (inst - "P") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (expand "SS") (("2" (expand "intersection") (("2" (expand "member") (("2" (expand "emptyset") (("2" (assert) (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "disjoint?") (("2" (skosimp) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (flatten) (("2" (prop) (("2" (hide -7) (("2" (typepred "BB!1") (("2" (expand "disjoint_indexed_measurable?") (("2" (expand "disjoint?") (("2" (inst - "i!1" "j!1") (("2" (assert) (("2" (expand "disjoint?") (("2" (expand "intersection") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -1) (("2" (apply-extensionality :hide? t) (("2" (expand "SS") (("2" (expand "IUnion") (("2" (expand "fullset" -1 2) (("2" (case-replace "A!1(x!1)") (("1" (rewrite "extensionality_postulate" -2 :dir rl) (("1" (inst - "x!1") (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "extend") (("1" (prop) (("1" (expand "image") (("1" (skosimp) (("1" (typepred "x!2") (("1" (assert) (("1" (expand "fullset") (("1" (inst + "x!2") (("1" (expand "intersection") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp) (("2" (expand "emptyset") (("2" (prop) (("2" (expand "intersection") (("2" (flatten) (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def "measure_integration/") (S formal-const-decl "sigma_algebra" conditional nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (intersection const-decl "set" sets nil) (<= const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil conditional nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (subset_algebra_intersection application-judgement "(S)" conditional nil) (fullset const-decl "set" sets nil) (TRUE const-decl "bool" booleans nil) (below type-eq-decl nil nat_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (image const-decl "set[R]" function_image nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (Union const-decl "set" sets nil) (extensionality_postulate formula-decl nil functions nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (P_convergence formula-decl nil probability_measure nil) (zero_tail_series formula-decl nil series_lems "series/") (sequence type-eq-decl nil sequences nil) (O const-decl "T3" function_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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (measurable_fullset name-judgement "measurable_set[T, S]" conditional nil) (subset_algebra_fullset name-judgement "(S)" conditional nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas_aux "measure_integration/") (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (unique_limit formula-decl nil convergence_sequences "analysis/") (series const-decl "sequence[real]" series "series/") (SS skolem-const-decl "[nat -> (S)]" conditional nil) (P const-decl "probability" conditional nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_eq formula-decl nil sigma "reals/") (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (P_subset_le formula-decl nil probability_measure nil) (null? const-decl "bool" conditional nil) (P_emptyset formula-decl nil probability_measure nil) (nnreal type-eq-decl nil real_types nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" conditional nil) (disjoint? const-decl "bool" indexed_sets_aux "sets_aux/") (disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (IUnion const-decl "set[T]" indexed_sets nil) (sigma_algebra_IUnion_rew application-judgement "(S)" conditional nil)) shostak)) (bayes_theorem_TCC1 0 (bayes_theorem_TCC1-1 nil 3351348898 ("" (skosimp*) (("" (expand "null?") (("" (lemma "conditional_partition" ("A" "B!1" "BB" "AA!1" "n" "n!1")) (("" (replace -2) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((null? const-decl "bool" conditional nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas_aux "measure_integration/") (subset_algebra_fullset name-judgement "(S)" conditional nil) (measurable_fullset name-judgement "measurable_set[T, S]" conditional nil) (conditional_partition formula-decl nil conditional nil) (T formal-nonempty-type-decl nil conditional nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (S formal-const-decl "sigma_algebra" conditional nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def "measure_integration/") (disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def "measure_integration/")) nil)) (bayes_theorem 0 (bayes_theorem-1 nil 3351348901 ("" (skosimp*) (("" (lemma "conditional_partition" ("A" "B!1" "BB" "AA!1" "n" "n!1")) (("" (replace -2 -1) (("" (replace -1 2 rl) (("" (expand "null?") (("" (rewrite "div_cancel4") (("" (hide -1 -2) (("" (expand "P") (("" (expand "null?") (("" (assert) (("" (case-replace "P(AA!1(j!1)) = 0") (("1" (lemma "P0_intersection" ("A" "AA!1(j!1)" "B" "B!1")) (("1" (inst - "P") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "div_cancel2" 3) (("2" (rewrite "div_cancel2" 3) (("2" (rewrite "intersection_commutative") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint_indexed_measurable nonempty-type-eq-decl nil generalized_measure_def "measure_integration/") (disjoint_indexed_measurable? const-decl "bool" generalized_measure_def "measure_integration/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (S formal-const-decl "sigma_algebra" conditional nil) (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def "measure_integration/") (sigma_algebra? const-decl "bool" subset_algebra_def "measure_integration/") (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-nonempty-type-decl nil conditional nil) (conditional_partition formula-decl nil conditional nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (div_cancel4 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (nnreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (probability nonempty-type-eq-decl nil probability_measure nil) (probability_measure? const-decl "bool" probability_measure nil) (probability_measure nonempty-type-eq-decl nil probability_measure nil) (P formal-const-decl "probability_measure" conditional nil) (P const-decl "probability" conditional nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (subset_algebra_intersection application-judgement "(S)" conditional nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (intersection_commutative formula-decl nil sets_lemmas nil) (div_cancel2 formula-decl nil real_props nil) (set type-eq-decl nil sets nil) (intersection const-decl "set" sets nil) (P0_intersection formula-decl nil probability_measure nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (null? const-decl "bool" conditional nil)) shostak))) ¤ Dauer der Verarbeitung: 0.52 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 |
