|
(generalized_measure_def
(disjoint_indexed_measurable_TCC1 0
(disjoint_indexed_measurable_TCC1-1 nil 3396524895
("" (rewrite "S_empty") nil nil)
((S_empty formula-decl nil generalized_measure_def nil)) nil))
(disjoint_indexed_measurable_TCC2 0
(disjoint_indexed_measurable_TCC2-1 nil 3457497937
("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(T formal-type-decl nil generalized_measure_def 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)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(finite_intersection2 application-judgement "finite_set[T]"
countable_props "sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(disjoint_indexed_measurable_is_disjoint_indexed_set 0
(disjoint_indexed_measurable_is_disjoint_indexed_set-1 nil 3396524895
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "disjoint_indexed_measurable?")
(("" (propax) nil nil)) nil))
nil))
nil)
((disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil generalized_measure_def nil)
(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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(measure_type_TCC1 0
(measure_type_TCC1-1 nil 3390645281
("" (expand "zero_measure")
(("" (expand "measure?")
(("" (expand "measure_empty?")
(("" (expand "measure_countably_additive?")
(("" (skosimp)
(("" (expand "o ")
(("" (expand "x_sum")
(("" (expand "x_eq")
(("" (rewrite "zero_series_conv")
(("" (rewrite "zero_series_limit") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measure? const-decl "bool" generalized_measure_def nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(O const-decl "T3" function_props nil)
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(zero_series_limit formula-decl nil series "series/")
(zero_series_conv formula-decl nil series "series/")
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(measure_empty? const-decl "bool" generalized_measure_def nil)
(zero_measure const-decl "extended_nnreal" generalized_measure_def
nil))
nil))
(trivial_measure_TCC1 0
(trivial_measure_TCC1-1 nil 3396670582
("" (expand "measure?")
(("" (split)
(("1" (expand "measure_empty?")
(("1" (lift-if) (("1" (assert) (("1" (grind) nil nil)) nil))
nil))
nil)
("2" (expand "measure_countably_additive?")
(("2" (skosimp*)
(("2" (expand "o")
(("2" (case-replace "empty?[T](IUnion(X!1))")
(("1" (expand "x_eq")
(("1"
(case-replace "(LAMBDA (x: nat):
IF empty?[T](X!1(x)) THEN (TRUE, 0) ELSE (FALSE, 0) ENDIF) = lambda (n:nat): (TRUE, 0)")
(("1" (hide -1)
(("1" (expand "x_sum")
(("1" (rewrite "zero_series_conv")
(("1" (rewrite "zero_series_limit") nil nil))
nil))
nil))
nil)
("2" (hide 2 -2)
(("2" (apply-extensionality :hide? t)
(("2" (lift-if)
(("2" (prop)
(("2" (hide 2)
(("2" (expand "empty?")
(("2"
(skosimp)
(("2"
(inst - "x!2")
(("2"
(expand "member")
(("2"
(expand "IUnion")
(("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "x_eq")
(("2" (expand "x_sum")
(("2"
(case-replace
"FORALL i: IF empty?[T](X!1(i)) THEN TRUE ELSE FALSE ENDIF")
(("1" (hide -2)
(("1" (expand "empty?")
(("1" (expand "IUnion")
(("1" (expand "member")
(("1"
(skosimp)
(("1"
(skosimp*)
(("1"
(inst - "i!1")
(("1"
(prop)
(("1" (inst - "x!1") nil nil)
("2" (inst - "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 3) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(measure_empty? const-decl "bool" generalized_measure_def nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(T formal-type-decl nil generalized_measure_def nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets 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)
(IUnion const-decl "set[T]" indexed_sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(zero_series_limit formula-decl nil series "series/")
(zero_series_conv formula-decl nil series "series/")
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(O const-decl "T3" function_props nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(measure? const-decl "bool" generalized_measure_def nil))
nil))
(complete_measure_TCC1 0
(complete_measure_TCC1-1 nil 3396670582
("" (expand "complete_measure?")
(("" (expand "trivial_measure")
(("" (expand "measure_complete?")
(("" (skosimp*)
(("" (lift-if)
(("" (assert)
(("" (prop)
(("" (rewrite "emptyset_is_empty?")
(("" (replace -1)
(("" (hide -1)
(("" (expand "subset?")
(("" (expand "emptyset")
(("" (expand "member")
(("" (case-replace "x!1=emptyset[T]")
(("1"
(hide -1 -2)
(("1"
(assert)
(("1" (rewrite "S_empty") nil nil))
nil))
nil)
("2"
(hide 2)
(("2"
(apply-extensionality :hide? t)
(("2"
(expand "emptyset")
(("2" (inst - "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((trivial_measure const-decl "measure_type" generalized_measure_def
nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(T formal-type-decl nil generalized_measure_def nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(S_empty formula-decl nil generalized_measure_def nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(measure_complete? const-decl "bool" generalized_measure_def nil)
(complete_measure? const-decl "bool" generalized_measure_def nil))
nil))
(complete_measure_is_measure 0
(complete_measure_is_measure-1 nil 3396097125
("" (judgement-tcc) nil 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 generalized_measure_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(S formal-const-decl "setofsets[T]" generalized_measure_def 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)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(complete_measure? const-decl "bool" generalized_measure_def nil)
(complete_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(measure_complete? const-decl "bool" generalized_measure_def nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(measure_empty? const-decl "bool" generalized_measure_def nil)
(O const-decl "T3" function_props nil)
(series const-decl "sequence[real]" series "series/")
(convergence const-decl "bool" convergence_sequences "analysis/")
(convergent? const-decl "bool" convergence_sequences "analysis/")
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(measure? const-decl "bool" generalized_measure_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/"))
nil))
(measure_disjoint_union 0
(measure_disjoint_union-1 nil 3396802882
("" (skosimp)
(("" (expand "measure?")
(("" (flatten)
(("" (expand "measure_countably_additive?")
((""
(inst -
"lambda (i:nat): if i=0 then a!1 elsif i=1 then b!1 else emptyset endif")
(("1"
(case-replace "IUnion(LAMBDA (i: nat):
IF i = 0 THEN a!1
ELSIF i = 1 THEN b!1
ELSE emptyset
ENDIF)=union(a!1, b!1)")
(("1" (assert)
(("1" (hide -1)
(("1" (expand "o")
(("1"
(case "x_eq(x_add(f!1(a!1), f!1(b!1)),x_sum(LAMBDA (x: nat):
IF x = 0 THEN f!1(a!1)
ELSE IF x = 1 THEN f!1(b!1) ELSE f!1(emptyset) ENDIF
ENDIF))")
(("1" (name-replace "LHS" "f!1(union(a!1, b!1))")
(("1"
(name-replace "RHS"
"x_add(f!1(a!1), f!1(b!1))")
(("1" (expand "x_eq")
(("1" (flatten)
(("1"
(assert)
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2" (expand "measure_empty?")
(("2" (replace -1)
(("2" (expand "x_eq")
(("2"
(expand "x_add")
(("2"
(expand "x_sum")
(("2"
(case-replace
"f!1(a!1)`1 AND f!1(b!1)`1")
(("1"
(flatten)
(("1"
(replace -1)
(("1"
(replace -2)
(("1"
(assert)
(("1"
(lemma
"zero_tail_series_conv"
("a"
"LAMBDA (i:nat):
IF i = 0 THEN f!1(a!1)`2
ELSE IF i = 1 THEN f!1(b!1)`2 ELSE 0 ENDIF
ENDIF"
"n"
"1"))
(("1"
(lemma
"zero_tail_series_limit"
("a"
"LAMBDA (i:nat):
IF i = 0 THEN f!1(a!1)`2
ELSE IF i = 1 THEN f!1(b!1)`2 ELSE 0 ENDIF
ENDIF"
"n"
"1"))
(("1"
(case-replace
"FORALL (m:nat):
1 < m =>
(LAMBDA (i: nat):
IF i = 0 THEN f!1(a!1)`2
ELSE IF i = 1 THEN f!1(b!1)`2 ELSE 0 ENDIF
ENDIF)
(m)
= 0")
(("1"
(replace -3)
(("1"
(replace -2)
(("1"
(hide-all-but
1)
(("1"
(expand
"series")
(("1"
(expand
"sigma")
(("1"
(expand
"sigma")
(("1"
(expand
"sigma")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 -2 2)
(("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1)
(("2"
(assert)
(("2"
(case-replace "f!1(a!1)`1")
(("1"
(assert)
(("1"
(prop)
(("1"
(inst - "1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide 2)
(("2"
(prop)
(("2"
(inst - "0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3" (rewrite "S_empty") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality :hide? t)
(("2" (expand "union")
(("2" (expand "member")
(("2" (expand "IUnion")
(("2" (expand "emptyset")
(("2" (case-replace "a!1(x!1)")
(("1" (inst + "0") nil nil)
("2" (case-replace "b!1(x!1)")
(("1"
(inst + "1")
(("1" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-1 -2 1))
(("2" (expand "disjoint_indexed_measurable?")
(("2" (expand "disjoint?")
(("2" (hide -1)
(("2" (skosimp)
(("2" (case-replace "i!1=0")
(("1" (case-replace "j!1=1")
(("1" (assert)
(("1" (expand "disjoint?")
(("1" (propax) nil nil)) nil))
nil)
("2" (assert)
(("2" (expand "disjoint?")
(("2"
(hide-all-but 3)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case-replace "i!1=1")
(("1" (case-replace "j!1=0")
(("1"
(hide-all-but (-3 3))
(("1"
(expand "disjoint?")
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide-all-but 4)
(("2" (grind) nil nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(hide-all-but 4)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp) (("3" (rewrite "S_empty") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((measure? const-decl "bool" generalized_measure_def nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(disjoint? const-decl "bool" sets nil)
(disjoint? const-decl "bool" indexed_sets_aux "sets_aux/")
(finite_intersection2 application-judgement "finite_set[T]"
countable_props "sets_aux/")
(finite_intersection1 application-judgement "finite_set[T]"
countable_props "sets_aux/")
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(x_add const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(measure_empty? const-decl "bool" generalized_measure_def nil)
(zero_tail_series_conv formula-decl nil series_aux "series/")
(sequence type-eq-decl nil sequences nil)
(< const-decl "bool" reals nil)
(series const-decl "sequence[real]" series "series/")
(sigma_0_neg formula-decl nil sigma_nat "reals/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sigma def-decl "real" sigma "reals/")
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero_tail_series_limit formula-decl nil series_aux "series/")
(S_empty formula-decl nil generalized_measure_def nil)
(O const-decl "T3" function_props nil)
(member const-decl "bool" sets nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(a!1 skolem-const-decl "(S)" generalized_measure_def nil)
(b!1 skolem-const-decl "(S)" generalized_measure_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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil generalized_measure_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(set type-eq-decl nil sets nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/"))
shostak))
(finite_measure_TCC1 0
(finite_measure_TCC1-1 nil 3396670582
("" (expand "trivial_finite_measure")
(("" (expand "finite_measure?")
(("" (skosimp)
(("" (expand "o ")
((""
(lemma "single_nz_series"
("a" "(LAMBDA (x: nat): 0)" "n" "0"))
(("" (split -1)
(("1" (assert)
(("1" (expand "series")
(("1" (hide -1)
(("1" (expand "convergence")
(("1" (skosimp)
(("1" (inst + "0")
(("1" (skosimp)
(("1" (rewrite "sigma_zero")
(("1"
(expand "abs")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (skosimp) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_measure? const-decl "bool" generalized_measure_def nil)
(O const-decl "T3" function_props nil)
(single_nz_series formula-decl nil series_aux "series/")
(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)
(sequence type-eq-decl nil sequences nil)
(trivial_finite_measure const-decl "[nnreal]"
generalized_measure_def nil))
nil))
(complete_finite_measure_is_finite_measure 0
(complete_finite_measure_is_finite_measure-1 nil 3424581123
("" (skolem + ("mu!1"))
(("" (typepred "mu!1")
(("" (expand "complete_finite_measure?") (("" (flatten) nil nil))
nil))
nil))
nil)
((complete_finite_measure type-eq-decl nil generalized_measure_def
nil)
(complete_finite_measure? const-decl "bool" generalized_measure_def
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)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil generalized_measure_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(to_measure_TCC1 0
(to_measure_TCC1-1 nil 3424581123
("" (skosimp)
(("" (typepred "m!1")
(("" (expand "finite_measure?")
(("" (expand "measure?")
(("" (flatten)
(("" (split)
(("1" (expand "measure_empty?") (("1" (propax) nil nil))
nil)
("2" (expand "measure_countably_additive?")
(("2" (skosimp)
(("2" (inst - "X!1")
(("2" (assert)
(("2" (expand "o ")
(("2" (expand "x_sum")
(("2" (expand "x_eq")
(("2" (lift-if)
(("2"
(assert)
(("2"
(case-replace
"convergence_sequences.convergent?(series(LAMBDA i: m!1(X!1(i))))")
(("1"
(rewrite
"convergence_sequences.limit_def")
nil
nil)
("2"
(expand "convergent?")
(("2"
(inst + "m!1(IUnion(X!1))")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_measure nonempty-type-eq-decl nil generalized_measure_def
nil)
(finite_measure? const-decl "bool" generalized_measure_def 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)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil generalized_measure_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(measure? const-decl "bool" generalized_measure_def nil)
(measure_empty? const-decl "bool" generalized_measure_def nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/")
(series const-decl "sequence[real]" series "series/")
(convergent? const-decl "bool" convergence_sequences "analysis/")
(sequence type-eq-decl nil sequences nil)
(limit_def formula-decl nil convergence_sequences "analysis/")
(set type-eq-decl nil sets nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(O const-decl "T3" function_props nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(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)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil))
nil))
(x_sum_measure 0
(x_sum_measure-1 nil 3450431811
("" (skosimp)
(("" (expand "measure?")
(("" (split)
(("1" (expand "measure_empty?")
(("1" (expand "x_sum")
(("1"
(case-replace
"FORALL (i_1: nat): F!1(i_1)(emptyset[T]) = (TRUE,0)")
(("1"
(case-replace
"FORALL (i_1: nat): F!1(i_1)(emptyset[T])`1")
(("1" (hide -1)
(("1"
(case-replace
"(LAMBDA (i_1: nat): F!1(i_1)(emptyset[T])`2)=lambda i: 0")
(("1" (hide -1 -2)
(("1" (rewrite "zero_series_conv")
(("1" (rewrite "zero_series_limit") nil nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("1" (inst - "x!1")
(("1" (assert)
(("1" (replace -1) (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (rewrite "S_empty") nil nil))
nil))
nil)
("3" (rewrite "S_empty") nil nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "i!1") (("2" (assert) nil nil)) nil))
nil))
nil)
("3" (rewrite "S_empty") nil nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (typepred "F!1(i!1)")
(("2" (expand "measure?")
(("2" (expand "measure_empty?")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (rewrite "S_empty") nil nil))
nil))
nil))
nil)
("2" (expand "measure_countably_additive?")
(("2" (skosimp)
(("2" (case "forall i: measure?(F!1(i))")
(("1" (expand "measure?")
(("1" (expand "measure_countably_additive?")
(("1"
(case "forall i: x_eq(x_sum(F!1(i) o X!1), F!1(i)(IUnion(X!1)))")
(("1" (name-replace "AA" "IUnion(X!1)")
(("1" (hide -2)
(("1" (expand "o ")
(("1"
(lemma "double_x_sum_eq"
("U" "LAMBDA (i,j:nat): F!1(j)(X!1(i))"))
(("1" (assert)
(("1"
(name-replace
"LHS"
"x_sum(LAMBDA (x: nat): (x_sum(LAMBDA i: F!1(i)(X!1(x)))))")
(("1"
(case
"x_eq(x_sum(LAMBDA (j_1: nat):
x_sum(LAMBDA (i_1: nat): F!1(j_1)(X!1(i_1)))),x_sum(LAMBDA i: F!1(i)(AA)))")
(("1"
(hide -3)
(("1"
(expand "x_eq")
(("1"
(flatten)
(("1"
(assert)
(("1"
(flatten)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2 -1)
(("2"
(lemma
"x_sum_eq"
("S"
"LAMBDA (j_1: nat):
x_sum(LAMBDA (i_1: nat): F!1(j_1)(X!1(i_1)))"
"T"
"LAMBDA i: F!1(i)(AA)"))
(("2"
(split -1)
(("1" (propax) nil nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(inst - "i!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "i!1")
(("2" (flatten)
(("2" (inst - "X!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((measure? const-decl "bool" generalized_measure_def nil)
(measure_countably_additive? const-decl "bool"
generalized_measure_def nil)
(x_sum_eq formula-decl nil extended_nnreal "extended_nnreal/")
(double_x_sum_eq formula-decl nil extended_nnreal
"extended_nnreal/")
(x_eq const-decl "bool" extended_nnreal "extended_nnreal/")
(O const-decl "T3" function_props nil)
(disjoint_indexed_measurable? const-decl "bool"
generalized_measure_def nil)
(disjoint_indexed_measurable nonempty-type-eq-decl nil
generalized_measure_def nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(measure_empty? const-decl "bool" generalized_measure_def nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(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 "[T, T -> boolean]" equalities nil)
(T formal-type-decl nil generalized_measure_def nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(S formal-const-decl "setofsets[T]" generalized_measure_def nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal
"extended_nnreal/")
(measure_type nonempty-type-eq-decl nil generalized_measure_def
nil)
(sequence type-eq-decl nil sequences nil)
(set type-eq-decl nil sets nil)
(emptyset const-decl "set" sets nil)
(TRUE const-decl "bool" booleans nil)
(S_empty formula-decl nil generalized_measure_def nil)
(zero_series_limit formula-decl nil series "series/")
(zero_series_conv formula-decl nil series "series/")
(NOT const-decl "[bool -> bool]" booleans nil)
(x_sum const-decl "extended_nnreal" extended_nnreal
"extended_nnreal/"))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.28Angebot
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
|
