|
(complex_finite_measures
(mu_TCC1 0
(mu_TCC1-1 nil 3509628901
("" (typepred "S")
(("" (expand "sigma_algebra?")
(("" (expand "subset_algebra_empty?")
(("" (expand "member") (("" (flatten) nil nil)) nil)) nil))
nil))
nil)
((finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(member const-decl "bool" sets nil)
(subset_algebra_empty? const-decl "bool" subset_algebra_def
"measure_integration/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil complex_finite_measures 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[T]" complex_finite_measures
nil))
nil))
(q_integrable_is_p_integrable 0
(q_integrable_is_p_integrable-1 nil 3509631321
("" (skosimp)
(("" (expand "p_integrable?")
(("" (flatten)
(("" (assert)
(("" (lemma "abs_expt_measurable[T,S]" ("g" "f!1" "a" "p!1"))
(("1"
(lemma "abs_expt_measurable[T,S]" ("g" "f!1" "a" "q!1"))
(("1" (assert)
(("1" (name "g!1" "abs(f!1)")
(("1" (case "forall (x:T): g!1(x)>=0")
(("1" (replace -2)
(("1"
(lemma
"integrable_nz_finite[T,S,to_measure(mu)]"
("f" "abs(f!1) ^ q!1" "epsilon" "1"))
(("1" (flatten)
(("1" (name "EE" "{x: T | g!1(x) >= 1}")
(("1"
(case-replace
"{x: T | abs((abs(f!1) ^ q!1)(x)) >= 1}=EE")
(("1"
(hide -1)
(("1"
(lemma
"measurable_complement[T,S]"
("a" "EE"))
(("1"
(lemma
"phi_is_simple[T,S]"
("X" "EE"))
(("1"
(lemma
"phi_is_simple[T,S]"
("X" "complement(EE)"))
(("1"
(lemma
"indefinite_integrable[T,S,to_measure(mu)]"
("E"
"EE"
"f"
"abs(f!1) ^ q!1"))
(("1"
(case
"integrable?[T, S, to_measure(mu)](phi[T,S](complement(EE)))")
(("1"
(lemma
"integral.integrable_add"
("f1"
"phi(complement(EE))"
"f2"
"lambda (x:T): phi(EE)(x) * (abs(f!1) ^ q!1)(x)"))
(("1"
(expand "+" -1)
(("1"
(name
"FF"
"(LAMBDA (x_1: T):
phi(complement(EE))(x_1) +
phi(EE)(x_1) * (abs(f!1) ^ q!1)(x_1))")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma
"integral_ae_abs"
("h"
"abs(f!1) ^ p!1"
"f"
"FF"))
(("1"
(assert)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(expand
"FF")
(("1"
(expand
"ae_le?")
(("1"
(expand
"pointwise_ae?")
(("1"
(expand
"ae?")
(("1"
(expand
"fullset")
(("1"
(expand
"ae_in?")
(("1"
(inst
+
"emptyset[T]")
(("1"
(skosimp)
(("1"
(expand
"member")
(("1"
(hide
1)
(("1"
(expand
"complement")
(("1"
(expand
"phi")
(("1"
(expand
"member")
(("1"
(replace
-11)
(("1"
(hide-all-but
(-10
-14
1))
(("1"
(expand
"EE")
(("1"
(expand
"abs")
(("1"
(expand
"^")
(("1"
(case-replace
"g!1(x!1) >= 1")
(("1"
(expand
">="
-1)
(("1"
(expand
"<="
-1)
(("1"
(split)
(("1"
(lemma
"both_sides_real_expt_gt1_le"
("gt1x"
"g!1(x!1)"
"a"
"p!1"
"b"
"q!1"))
(("1"
(lemma
"real_expt_pos"
("px"
"g!1(x!1)"
"a"
"p!1"))
(("1"
(expand
"abs")
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(replace
-1
*
rl)
(("2"
(rewrite
"real_expt_1a")
(("2"
(rewrite
"real_expt_1a")
(("2"
(expand
"abs")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"g!1(x!1)<1")
(("1"
(hide
1)
(("1"
(assert)
(("1"
(lemma
"both_sides_real_expt_lt"
("x"
"g!1(x!1)"
"y"
"1"
"pa"
"p!1"))
(("1"
(rewrite
"real_expt_1a")
(("1"
(expand
"abs")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "*" -2)
(("2"
(propax)
nil
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2"
(lemma
"isf_is_integrable[T, S, to_measure(mu)]")
(("2"
(inst
-
"phi[T, S](complement(EE))")
(("2"
(expand "isf?")
(("2"
(assert)
(("2"
(expand "mu_fin?")
(("2"
(expand
"to_measure")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil))
nil)
("2"
(expand "measurable_set?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace -1 * rl)
(("2"
(replace -5)
(("2"
(hide-all-but (-4 1))
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "^")
(("2"
(inst - "x!1")
(("2"
(case-replace
"g!1(x!1) >= 1")
(("1"
(lemma
"both_sides_real_expt_le"
("y"
"g!1(x!1)"
"x"
"1"
"pa"
"q!1"))
(("1"
(rewrite
"real_expt_1a")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"both_sides_real_expt_ge"
("x"
"g!1(x!1)"
"y"
"1"
"pa"
"q!1"))
(("2"
(rewrite
"real_expt_1a")
(("2"
(assert)
(("2"
(expand "abs")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -1 1 rl)
(("2" (expand "abs")
(("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((p_integrable? const-decl "bool" p_integrable_def nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_measurable_def formula-decl nil complex_measurable nil)
(T formal-type-decl nil complex_finite_measures 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[T]" complex_finite_measures
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(measurable_complement judgement-tcc nil measure_space_def
"measure_integration/")
(set type-eq-decl nil sets nil)
(measurable_set? const-decl "bool" measure_space_def
"measure_integration/")
(measurable_set nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(complement const-decl "set" sets 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(phi const-decl "nat" measure_space "measure_integration/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(integral_ae_abs formula-decl nil integral "measure_integration/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(FF skolem-const-decl "[T -> nnreal]" complex_finite_measures nil)
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(fullset const-decl "set" sets nil)
(null_emptyset name-judgement "null_set[T, S, to_measure(mu)]"
complex_finite_measures nil)
(subset_algebra_emptyset name-judgement "(S)"
complex_finite_measures nil)
(finite_emptyset name-judgement "finite_set[T]" sigma_countable
"sigma_set/")
(finite_emptyset name-judgement "finite_set[T]" step_fun_props
"analysis/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets nil)
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(negligible_set? const-decl "bool" measure_theory
"measure_integration/")
(member const-decl "bool" sets nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(TRUE const-decl "bool" booleans nil)
(<= const-decl "bool" reals nil)
(real_expt_1a formula-decl nil real_expt "power/")
(both_sides_real_expt_gt1_le formula-decl nil real_expt "power/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_expt_pos formula-decl nil real_expt "power/")
(both_sides_real_expt_lt formula-decl nil real_expt "power/")
(abs_nat formula-decl nil abs_lems "reals/")
(< const-decl "bool" reals nil)
(EE skolem-const-decl "[T -> bool]" complex_finite_measures nil)
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(measurable_fullset name-judgement "measurable_set[T, S]"
complex_finite_measures nil)
(subset_algebra_fullset name-judgement "(S)"
complex_finite_measures nil)
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(integrable_add judgement-tcc nil integral "measure_integration/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(isf nonempty-type-eq-decl nil isf "measure_integration/")
(isf? const-decl "bool" isf "measure_integration/")
(mu_fin? const-decl "bool" measure_props "measure_integration/")
(isf_is_integrable judgement-tcc nil integral
"measure_integration/")
(indefinite_integrable formula-decl nil integral
"measure_integration/")
(phi_is_simple judgement-tcc nil measure_space
"measure_integration/")
(both_sides_real_expt_ge formula-decl nil real_expt "power/")
(both_sides_real_expt_le formula-decl nil real_expt "power/")
(integrable_nz_finite formula-decl nil integral
"measure_integration/")
(integrable? const-decl "bool" integral "measure_integration/")
(integrable nonempty-type-eq-decl nil integral
"measure_integration/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(nnreal type-eq-decl nil real_types nil)
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(mu formal-const-decl "finite_measure[T, S]"
complex_finite_measures nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(real_gt_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)
(abs_expt_measurable formula-decl nil complex_measurable 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)
(>= const-decl "bool" reals 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)
(complex type-decl nil complex_types "complex_alt/")
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex_measurable nonempty-type-eq-decl nil complex_measurable
nil))
shostak))
(essentially_bounded_is_p_integrable 0
(essentially_bounded_is_p_integrable-1 nil 3509633053
("" (skosimp)
(("" (expand "p_integrable?")
(("" (expand "essentially_bounded?")
(("" (flatten)
(("" (replace -1)
(("" (lemma "abs_expt_measurable" ("g" "f!1" "a" "p!1"))
(("1" (name "g!1" "abs(f!1) ^ p!1")
(("1" (replace -1)
(("1" (lemma "essential_bound_def2" ("f" "f!1"))
(("1"
(case "ae_le?(g!1, LAMBDA (x: T): essential_bound(f!1)^p!1)")
(("1" (typepred "essential_bound(f!1)")
(("1"
(name-replace "KK" "essential_bound(f!1)")
(("1" (hide -3 -4 -6 -7)
(("1"
(lemma "integral_ae_abs"
("h"
"g!1"
"f"
"LAMBDA (x: T): KK ^ p!1"))
(("1"
(assert)
(("1"
(hide 2 -3)
(("1"
(expand "ae_le?")
(("1"
(expand "pointwise_ae?")
(("1"
(expand "ae?")
(("1"
(expand "fullset")
(("1"
(expand "ae_in?")
(("1"
(skosimp)
(("1"
(inst + "E!1")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(expand
"abs")
(("1"
(typepred
"g!1(x!1)")
(("1"
(expand
"abs"
2
1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(hide 2)
(("3"
(lemma
"isf_is_integrable[T, S, to_measure(mu)]")
(("3"
(inst - "phi[T,S](fullset[T])")
(("1"
(lemma
"integral.integrable_scal"
("c"
" KK ^ p!1"
"f"
"phi[T, S](fullset[T])"))
(("1"
(expand "*" -1)
(("1"
(expand "phi" -1)
(("1"
(expand "fullset")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2"
(lemma
"phi_is_simple[T,S]"
("X" "fullset[T]"))
(("2"
(expand "isf?")
(("2"
(expand "mu_fin?")
(("2"
(expand "to_measure")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "ae_le?")
(("2" (expand "pointwise_ae?")
(("2" (expand "ae?")
(("2"
(expand "fullset")
(("2"
(expand "ae_in?")
(("2"
(skosimp)
(("2"
(expand "member")
(("2"
(inst + "E!1")
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2"
(replace 1)
(("2"
(replace -2 2 rl)
(("2"
(expand "^" 2 1)
(("2"
(expand "abs" 2 1)
(("2"
(lemma
"both_sides_real_expt_le"
("x"
"abs(f!1)(x!1)"
"y"
"essential_bound(f!1)"
"pa"
"p!1"))
(("2"
(assert)
(("2"
(expand
"abs"
-1
1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3" (expand "essentially_bounded?")
(("3" (assert) nil nil)) nil))
nil))
nil)
("2" (expand "essentially_bounded?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand "complex_measurable?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((p_integrable? const-decl "bool" p_integrable_def nil)
(S formal-const-decl "sigma_algebra[T]" complex_finite_measures
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-type-decl nil complex_finite_measures nil)
(complex_measurable nonempty-type-eq-decl nil complex_measurable
nil)
(complex_measurable? const-decl "bool" complex_measurable nil)
(complex type-decl nil complex_types "complex_alt/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-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)
(abs_expt_measurable formula-decl nil complex_measurable nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Im const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(Re const-decl "[T -> real]" complex_fun_ops "complex_alt/")
(measurable_function? const-decl "bool" measure_space_def
"measure_integration/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(ae_le? const-decl "bool" measure_theory "measure_integration/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "nnreal" real_expt "power/")
(essential_bound const-decl "nnreal" essentially_bounded nil)
(integral_ae_abs formula-decl nil integral "measure_integration/")
(integrable? const-decl "bool" integral "measure_integration/")
(integrable nonempty-type-eq-decl nil integral
"measure_integration/")
(measurable_function nonempty-type-eq-decl nil measure_space_def
"measure_integration/")
(pointwise_ae? const-decl "bool" measure_theory
"measure_integration/")
(fullset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(TRUE const-decl "bool" booleans nil)
(abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(set type-eq-decl nil sets nil)
(negligible_set? const-decl "bool" measure_theory
"measure_integration/")
(negligible nonempty-type-eq-decl nil measure_theory
"measure_integration/")
(ae_in? const-decl "bool" measure_theory "measure_integration/")
(ae? const-decl "bool" measure_theory "measure_integration/")
(measurable_fullset name-judgement "measurable_set[T, S]"
complex_finite_measures nil)
(subset_algebra_fullset name-judgement "(S)"
complex_finite_measures nil)
(isf_is_integrable judgement-tcc nil integral
"measure_integration/")
(phi_is_simple judgement-tcc nil measure_space
"measure_integration/")
(mu_fin? const-decl "bool" measure_props "measure_integration/")
(integrable_scal judgement-tcc nil integral "measure_integration/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(isf nonempty-type-eq-decl nil isf "measure_integration/")
(phi const-decl "nat" measure_space "measure_integration/")
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(isf? const-decl "bool" isf "measure_integration/")
(phi_is_simple application-judgement "simple[T, S]"
complex_finite_measures nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(both_sides_real_expt_le formula-decl nil real_expt "power/")
(complex_measurable_def formula-decl nil complex_measurable nil)
(mu formal-const-decl "finite_measure[T, S]"
complex_finite_measures nil)
(to_measure const-decl "measure_type" generalized_measure_def
"measure_integration/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(finite_measure nonempty-type-eq-decl nil generalized_measure_def
"measure_integration/")
(finite_measure? const-decl "bool" generalized_measure_def
"measure_integration/")
(essentially_bounded nonempty-type-eq-decl nil essentially_bounded
nil)
(essential_bound_def2 formula-decl nil essentially_bounded nil)
(abs const-decl "[T -> nonneg_real]" complex_fun_ops
"complex_alt/")
(^ const-decl "[T -> nnreal]" real_fun_power "power/")
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(essentially_bounded? const-decl "bool" essentially_bounded nil))
shostak)))
¤ Dauer der Verarbeitung: 0.121 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.
|
