|
(monotone_classes
(monotone_finite_measures_TCC1 0
(monotone_finite_measures_TCC1-1 nil 3453992461
("" (skosimp)
(("" (skolem + "a!1")
(("" (typepred "a!1")
(("" (lemma "generated_sigma_algebra_subset1" ("X" "C"))
(("" (expand "subset?")
(("" (inst - "a!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(generated_sigma_algebra_subset1 formula-decl nil
subset_algebra_def nil)
(subset_algebra_complement application-judgement "(S)"
sigma_algebra nil)
(subset_algebra_intersection application-judgement "(S)"
sigma_algebra nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(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 monotone_classes nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(C formal-const-decl "(nonempty?[set[T]])" monotone_classes nil))
nil))
(monotone_finite_measures 0
(monotone_finite_measures-2 nil 3454001130
("" (skosimp)
(("" (name "S" "generated_sigma_algebra(C)")
(("" (name "TT" "{E:(S) | mu!1(E)=nu!1(E)}")
(("1" (case "forall (x:set[T]): S(x) => TT(x)")
(("1" (skosimp)
(("1" (typepred "x!1")
(("1" (inst - "x!1")
(("1" (expand "S")
(("1" (expand "TT") (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2"
(case "generated_sigma_algebra(generated_subset_algebra(C))=S")
(("1"
(lemma "monotone_class[T]"
("B" "generated_subset_algebra[T](C)" "C"
"{x:set[T] | S(x) & mu!1(x) = nu!1(x)}"))
(("1" (replace -2 -1)
(("1" (split)
(("1" (expand "subset?")
(("1" (inst - "x!1")
(("1" (expand "member")
(("1" (assert)
(("1"
(expand "TT")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -3 2)
(("2" (expand "subset?")
(("2" (skosimp)
(("2" (expand "member")
(("2"
(lemma
"disjoint_algebra_construction"
("NX" "C"))
(("2"
(replace -7)
(("2"
(expand "member")
(("2"
(lemma
"generated_sigma_algebra_subset1[T]"
("X"
"generated_subset_algebra(C)"))
(("2"
(expand "subset?" -1)
(("2"
(inst - "x!2")
(("2"
(expand "member")
(("2"
(assert)
(("2"
(replace -2 -3)
(("2"
(hide-all-but
(-3 -9 1))
(("2"
(expand
"finite_disjoint_unions")
(("2"
(expand
"fullset")
(("2"
(expand
"extend")
(("2"
(prop)
(("2"
(expand
"finite_disjoint_union?")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(typepred
"mu!1")
(("2"
(typepred
"nu!1")
(("2"
(expand
"finite_measure?")
(("2"
(flatten)
(("2"
(case
"disjoint_indexed_measurable?[T, (generated_sigma_algebra(C))](E!1)")
(("1"
(inst
-
"E!1")
(("1"
(inst
-
"E!1")
(("1"
(replace
-7
*
rl)
(("1"
(hide
-1
-6
-7)
(("1"
(lemma
"zero_tail_series_limit"
("n"
"n!1"
"a"
"nu!1 o E!1"))
(("1"
(split)
(("1"
(lemma
"zero_tail_series_limit"
("n"
"n!1"
"a"
"mu!1 o E!1"))
(("1"
(split)
(("1"
(rewrite
"convergence_sequences.limit_def"
-4
:dir
rl)
(("1"
(rewrite
"convergence_sequences.limit_def"
-6
:dir
rl)
(("1"
(replace
-1)
(("1"
(replace
-2)
(("1"
(replace
-4
*
rl)
(("1"
(replace
-6
*
rl)
(("1"
(hide
-1
-2
-4
-6)
(("1"
(expand
"o ")
(("1"
(expand
"series")
(("1"
(lemma
"sigma_eq"
("low"
"0"
"high"
"n!1"
"F"
"LAMBDA (x: nat): mu!1(E!1(x))"
"G"
"LAMBDA (x: nat): nu!1(E!1(x))"))
(("1"
(assert)
(("1"
(hide
2)
(("1"
(skosimp)
(("1"
(inst
-3
"n!2")
(("1"
(flatten)
(("1"
(assert)
(("1"
(typepred
"n!2")
(("1"
(expand
"<="
-2)
(("1"
(split)
(("1"
(assert)
(("1"
(inst
-7
"E!1(n!2)")
nil
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"o ")
(("2"
(inst
-7
"m!1")
(("2"
(flatten)
(("2"
(assert)
(("2"
(rewrite
"emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(expand
"o ")
(("2"
(inst
-6
"m!1")
(("2"
(flatten)
(("2"
(assert)
(("2"
(rewrite
"emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
-1
-2
-3
-4
2)
(("2"
(expand
"disjoint_indexed_measurable?")
(("2"
(propax)
nil
nil))
nil))
nil)
("3"
(hide
-1
-2
-3
-4
-6
2
-8)
(("3"
(skolem
+
"n!2")
(("3"
(inst
-
"n!2")
(("3"
(flatten)
(("3"
(case-replace
"n!2)
(("1"
(lemma
"generated_sigma_algebra_subset1[T]"
("X"
"C"))
(("1"
(expand
"subset?")
(("1"
(inst
-
"E!1(n!2)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"emptyset_is_empty?")
(("2"
(typepred
"generated_sigma_algebra[T](C)")
(("2"
(expand
"sigma_algebra?")
(("2"
(flatten)
(("2"
(expand
"subset_algebra_empty?")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 -3)
(("2" (expand "monotone?")
(("2" (skosimp)
(("2" (expand "member")
(("2"
(lemma "sigma_algebra_IUnion[T,S]"
("SS" "E!1"))
(("1"
(lemma "sigma_algebra_IIntersection[T,S]"
("SS" "E!1"))
(("1"
(expand "member")
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(split)
(("1"
(flatten)
(("1"
(lemma
"m_increasing_convergence[T,S,to_measure(mu!1)]"
("E" "E!1"))
(("1"
(assert)
(("1"
(lemma
"m_increasing_convergence[T,S,to_measure(nu!1)]"
("E" "E!1"))
(("1"
(assert)
(("1"
(expand "to_measure")
(("1"
(name-replace
"MU"
"mu!1(IUnion(E!1))")
(("1"
(name-replace
"NU"
"nu!1(IUnion(E!1))")
(("1"
(expand "o ")
(("1"
(expand
"x_converges?")
(("1"
(case-replace
"convergence_sequences.convergent?(LAMBDA (i:nat): nu!1(E!1(i)))")
(("1"
(case-replace
"convergence_sequences.convergent?(LAMBDA (i:nat): mu!1(E!1(i)))")
(("1"
(lemma
"convergence_sequences.limit_lemma"
("v"
"LAMBDA (i: nat): nu!1(E!1(i))"))
(("1"
(lemma
"convergence_sequences.limit_lemma"
("v"
"LAMBDA (i: nat): mu!1(E!1(i))"))
(("1"
(replace
-5
*
rl)
(("1"
(replace
-6
*
rl)
(("1"
(lemma
"cnv_seq_diff"
("s1"
"LAMBDA (i: nat): mu!1(E!1(i))"
"l1"
"MU"
"s2"
"LAMBDA (i: nat): nu!1(E!1(i))"
"l2"
"NU"))
(("1"
(assert)
(("1"
(lemma
"cnv_seq_const"
("a"
"0"))
(("1"
(expand
"const_fun")
(("1"
(expand
"-"
-2)
(("1"
(case-replace
"(LAMBDA (x: nat): mu!1(E!1(x)) - nu!1(E!1(x)))=(LAMBDA (x: nat): 0)")
(("1"
(lemma
"convergence_sequences.unique_limit"
("u"
"LAMBDA (x: nat): 0"
"l1"
"0"
"l2"
"MU-NU"))
(("1"
(assert)
nil
nil))
nil)
("2"
(apply-extensionality
:hide?
t)
(("1"
(inst
-12
"x!2")
(("1"
(flatten)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(inst
-12
"x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(propax)
nil
nil))
nil)
("2"
(propax)
nil
nil)
("3"
(skosimp)
(("3"
(assert)
(("3"
(inst
-8
"i!1")
(("3"
(flatten)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil)
("3"
(skosimp)
(("3"
(inst
-7
"i!1")
(("3"
(flatten)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil)
("3"
(skosimp)
(("3"
(inst
-6
"i!1")
(("3"
(flatten)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(split)
(("1"
(skosimp)
(("1"
(assert)
(("1"
(replace -8)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1 -9))
(("2"
(typepred
"to_measure[T, (generated_sigma_algebra(C))](nu!1)")
(("2"
(expand
"measure?")
(("2"
(expand
"to_measure")
(("2"
(expand
"measure_empty?")
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand
"measure_countably_additive?")
(("2"
(skosimp)
(("2"
(typepred
"X!1")
(("2"
(expand
"o ")
(("2"
(inst
-
"X!1")
(("2"
(hide
2)
(("2"
(split)
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"disjoint_indexed_measurable?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skolem + "n!1")
(("2"
(expand
"measurable_set?")
(("2"
(inst - "n!1")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil)
("3"
(split)
(("1"
(skosimp)
(("1"
(replace -7)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(typepred
"to_measure[T, (generated_sigma_algebra(C))](mu!1)")
(("2"
(hide-all-but
(-1 1 -8))
(("2"
(expand "measure?")
(("2"
(flatten)
(("2"
(expand
"measure_empty?")
(("2"
(expand
"to_measure")
(("2"
(assert)
(("2"
(hide -1)
(("2"
(expand
"measure_countably_additive?")
(("2"
(skosimp)
(("2"
(inst
-
"X!1")
(("1"
(expand
"o ")
(("1"
(propax)
nil
nil))
nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.65Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
