|
(riesz_bounded_functionals
(IMP_riesz_linear_functionals_TCC1 0
(IMP_riesz_linear_functionals_TCC1-1 nil 3492869758
("" (lemma "funs_subspace")
(("" (expand "bounded_linear_subspace?")
(("" (flatten)
(("" (skosimp*)
(("" (expand "funs_sum_closed?")
(("" (inst - "f!1" "g!1")
(("1" (expand "+")
(("1" (expand "extend") (("1" (assert) nil nil)) nil))
nil)
("2" (expand "extend")
(("2" (assert)
(("2" (expand "fullset") (("2" (propax) nil nil))
nil))
nil))
nil)
("3" (expand "extend")
(("3" (expand "fullset") (("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(f!1 skolem-const-decl "Funs" riesz_bounded_functionals nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(Funs formal-subtype-decl nil riesz_bounded_functionals nil)
(Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
riesz_bounded_functionals nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}"
riesz_bounded_functionals nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_bounded_functionals nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(g!1 skolem-const-decl "Funs" riesz_bounded_functionals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(funs_sum_closed? const-decl "bool" riesz_function_sets nil)
(funs_subspace formula-decl nil riesz_bounded_functionals nil))
nil))
(IMP_riesz_linear_functionals_TCC2 0
(IMP_riesz_linear_functionals_TCC2-1 nil 3492869758
("" (skeep)
(("" (lemma "funs_subspace")
(("" (expand "bounded_linear_subspace?")
(("" (flatten)
(("" (expand "funs_const_closed?")
(("" (inst - "f" "c")
(("1" (expand "extend") (("1" (assert) nil nil)) nil)
("2" (expand "extend")
(("2" (expand "fullset") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((funs_subspace formula-decl nil riesz_bounded_functionals nil)
(f skolem-const-decl "Funs" riesz_bounded_functionals nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(Funs formal-subtype-decl nil riesz_bounded_functionals nil)
(Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
riesz_bounded_functionals nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}"
riesz_bounded_functionals nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_bounded_functionals nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(funs_const_closed? const-decl "bool" riesz_function_sets nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil))
nil))
(IMP_riesz_linear_functionals_TCC3 0
(IMP_riesz_linear_functionals_TCC3-1 nil 3492875090
("" (lemma "funs_subspace")
(("" (expand "bounded_linear_subspace?")
(("" (flatten)
(("" (expand "funs_contain_constants?")
(("" (inst - "0")
(("" (expand "extend") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(funs_contain_constants? const-decl "bool" riesz_function_sets nil)
(extend const-decl "R" extend 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)
(funs_subspace formula-decl nil riesz_bounded_functionals nil))
nil))
(bounded_op?_TCC1 0
(bounded_op?_TCC1-1 nil 3492869758
("" (skeep)
(("" (lemma "funs_subspace")
(("" (expand "bounded_linear_subspace?")
(("" (flatten)
(("" (expand "funs_bounded?")
(("" (inst - "f")
(("" (expand "extend")
(("" (expand "fullset") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((funs_subspace formula-decl nil riesz_bounded_functionals 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)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_bounded_functionals nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{bb: real | a < bb}"
riesz_bounded_functionals nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
riesz_bounded_functionals nil)
(Funs formal-subtype-decl nil riesz_bounded_functionals nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil) (set type-eq-decl nil sets nil)
(fullset const-decl "set" sets nil)
(f skolem-const-decl "Funs" riesz_bounded_functionals nil)
(funs_bounded? const-decl "bool" riesz_function_sets nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil))
nil))
(op_norm_TCC1 0
(op_norm_TCC1-1 nil 3492869758
(""
(case "FORALL (L:(bounded_op?)): EXISTS (M:nnreal): (FORALL (f: Funs):
abs(L(f)) <= M * fun_norm[a, b](f))
AND
(FORALL (M1: real):
M1 < M IMPLIES
(EXISTS (f: Funs): abs(L(f)) > M1*fun_norm(f)))")
(("1"
(inst + "LAMBDA (L:(bounded_op?)): choose({M: nnreal |
(FORALL (f: Funs):
abs(L(f)) <= M * fun_norm[a, b](f))
AND
(FORALL (M1: real):
M1 < M IMPLIES
(EXISTS (f: Funs): abs(L(f)) > M1*fun_norm(f)))})")
(("1" (skeep)
(("1" (inst - "L")
(("1" (skosimp*)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (inst - "M!1") (("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (skeep)
(("2" (skeep)
(("2" (skeep)
(("2" (hide -)
(("2" (lemma "funs_subspace")
(("2" (expand "bounded_linear_subspace?")
(("2" (flatten)
(("2" (expand "funs_bounded?")
(("2" (inst - "f1")
(("2" (expand "extend")
(("2" (expand "fullset")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide -)
(("3" (skeep)
(("3" (lemma "funs_subspace")
(("3" (assert)
(("3" (expand "bounded_linear_subspace?")
(("3" (flatten)
(("3" (expand "funs_bounded?")
(("3" (inst - "f")
(("3" (expand "extend")
(("3" (expand "fullset")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skolem 1 "LL")
(("2"
(name "Aset"
"{M:nnreal | (FORALL (f: Funs): abs(LL(f)) <= M * fun_norm[a, b](f))}")
(("1" (name "MM" "glb(Aset)")
(("1" (inst + "MM")
(("1" (split +)
(("1" (skeep)
(("1" (case "fun_norm[a,b](f) = 0")
(("1" (replace -1)
(("1" (assert)
(("1" (typepred "LL")
(("1" (expand "bounded_op?")
(("1" (skosimp*)
(("1"
(inst - "f")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "MM")
(("2" (expand "greatest_lower_bound?")
(("2" (flatten)
(("2" (inst -2 "abs(LL(f))/fun_norm[a,b](f)")
(("1" (split -)
(("1" (cross-mult -) nil nil)
("2"
(expand "lower_bound?")
(("2"
(skosimp*)
(("2"
(typepred "s!1")
(("2"
(expand "extend" -1)
(("2"
(assert)
(("2"
(ground)
(("2"
(expand "Aset" -2)
(("2"
(inst - "f")
(("2"
(cross-mult +)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (typepred "MM")
(("2" (expand "greatest_lower_bound?")
(("2" (flatten)
(("2" (expand "lower_bound?" -1)
(("2" (inst - "M1")
(("1" (assert) nil nil)
("2" (expand "extend" +)
(("2"
(ground)
(("1"
(expand "Aset" +)
(("1"
(skosimp*)
(("1"
(inst + "f!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(name "ff1" "LAMBDA (y: INTab): 1")
(("2"
(case "fun_norm(ff1) = 1")
(("1"
(inst + "ff1")
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(lemma "funs_subspace")
(("2"
(expand
"bounded_linear_subspace?")
(("2"
(flatten)
(("2"
(expand
"funs_contain_constants?")
(("2"
(inst - "1")
(("2"
(expand "extend")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "fun_norm(ff1)")
(("2"
(inst - "a")
(("1"
(case "ff1(a) = 1")
(("1"
(replace -1)
(("1"
(assert)
(("1"
(inst - "1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand "ff1")
(("2" (propax) nil nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil)
("3"
(expand "bounded_on_int?" +)
(("3"
(inst + "1")
(("3"
(skosimp*)
(("3"
(expand "ff1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "MM")
(("2" (expand "greatest_lower_bound?")
(("2" (flatten)
(("2" (inst - "0")
(("2" (assert)
(("2" (expand "lower_bound?" +)
(("2" (skosimp*)
(("2" (typepred "s!1")
(("2"
(expand "extend" -1)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (assert)
(("2" (hide -)
(("2"
(typepred
"glb(extend[real, nnreal, bool, FALSE](Aset))")
(("2" (expand "greatest_lower_bound?")
(("2" (ground)
(("1" (expand "lower_bound?")
(("1" (skosimp*)
(("1" (inst - "s!1")
(("1"
(expand "extend" 1)
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst - "y!1")
(("2" (assert)
(("2"
(hide 1)
(("2"
(expand "lower_bound?")
(("2"
(skosimp*)
(("2"
(inst - "s!1")
(("2"
(assert)
(("2"
(typepred "s!1")
(("2"
(expand "extend" -1)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (split +)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (typepred "LL")
(("1" (expand "bounded_op?")
(("1" (skosimp*)
(("1" (inst -2 "M!1")
(("1"
(expand "extend")
(("1"
(expand "Aset")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "bounded_below?")
(("2" (name "ff1" "LAMBDA (y: INTab): 1")
(("2" (case "fun_norm(ff1) = 1")
(("1" (inst + "abs(LL(ff1))/fun_norm(ff1)")
(("1" (expand "lower_bound?")
(("1" (skosimp*)
(("1" (typepred "s!1")
(("1"
(expand "extend")
(("1"
(ground)
(("1"
(expand "Aset" -2)
(("1"
(inst - "ff1")
(("1" (cross-mult 1) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (lemma "funs_subspace")
(("3" (expand "bounded_linear_subspace?")
(("3" (flatten)
(("3"
(expand "funs_contain_constants?")
(("3"
(inst - "1")
(("3"
(expand "extend")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2)
(("2" (hide 2)
(("2" (typepred "fun_norm(ff1)")
(("2" (inst - "a")
(("1"
(inst - "1")
(("1"
(case "ff1(a) = 1")
(("1" (assert) nil nil)
("2"
(expand "ff1")
(("2" (propax) nil nil))
nil))
nil))
nil)
("2" (ground) nil nil))
nil))
nil))
nil))
nil)
("3" (expand "ff1" +)
(("3" (ground)
(("3" (hide (-2 2))
(("3" (expand "bounded_on_int?")
(("3"
(inst + "2")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skeep)
(("2" (lemma "funs_subspace")
(("2" (expand "bounded_linear_subspace?")
(("2" (flatten)
(("2" (expand "funs_bounded?")
(("2" (inst - "f")
(("2" (expand "extend")
(("2" (expand "fullset")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skeep)
(("3" (skeep)
(("3" (skeep)
(("3" (lemma "funs_subspace")
(("3" (expand "bounded_linear_subspace?")
(("3" (flatten)
(("3" (expand "funs_bounded?")
(("3" (inst - "f1")
(("3" (expand "extend")
(("3" (expand "fullset")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (hide 2)
(("4" (skeep)
(("4" (lemma "funs_subspace")
(("4" (expand "bounded_linear_subspace?")
(("4" (flatten)
(("4" (expand "funs_bounded?")
(("4" (inst - "f")
(("4" (expand "extend")
(("4" (expand "fullset") (("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((f skolem-const-decl "Funs" riesz_bounded_functionals nil)
(f1 skolem-const-decl "Funs" riesz_bounded_functionals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(ff1 skolem-const-decl "[INTab[a, b] -> posint]"
riesz_bounded_functionals nil)
(s!1 skolem-const-decl "(extend[real, nnreal, bool, FALSE](Aset))"
riesz_bounded_functionals nil)
(s!1 skolem-const-decl "(Aset)" riesz_bounded_functionals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Aset skolem-const-decl "[nnreal -> boolean]"
riesz_bounded_functionals nil)
(MM skolem-const-decl
"{x | greatest_lower_bound?(x, extend[real, nnreal, bool, FALSE](Aset))}"
riesz_bounded_functionals 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posint nonempty-type-eq-decl nil integers nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(abs_nat formula-decl nil abs_lems "reals/")
(ff1 skolem-const-decl "[INTab[a, b] -> posint]"
riesz_bounded_functionals nil)
(funs_contain_constants? const-decl "bool" riesz_function_sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(M1 skolem-const-decl "real" riesz_bounded_functionals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(lower_bound? const-decl "bool" bounded_real_defs nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(f skolem-const-decl "Funs" riesz_bounded_functionals nil)
(/= const-decl "boolean" notequal nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(glb const-decl "{x | greatest_lower_bound?(x, SB)}"
bounded_real_defs nil)
(greatest_lower_bound? const-decl "bool" bounded_real_defs nil)
(bounded_below? const-decl "bool" bounded_real_defs nil)
(f skolem-const-decl "Funs" riesz_bounded_functionals nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(funs_subspace formula-decl nil riesz_bounded_functionals nil)
(fullset const-decl "set" sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(f1 skolem-const-decl "Funs" riesz_bounded_functionals nil)
(funs_bounded? const-decl "bool" riesz_function_sets nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(f skolem-const-decl "Funs" riesz_bounded_functionals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals 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)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_bounded_functionals nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{bb: real | a < bb}"
riesz_bounded_functionals nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
riesz_bounded_functionals nil)
(Funs formal-subtype-decl nil riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_op? const-decl "bool" riesz_bounded_functionals nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(bounded_on_int? const-decl "bool" riesz_interval_funs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(fun_norm const-decl "{M: nnreal |
(FORALL (x): abs(f(x)) <= M) AND
(FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}"
riesz_interval_funs nil))
nil))
(op_norm_bound 0
(op_norm_bound-1 nil 3492874239
("" (skeep)
(("" (typepred "op_norm(L)") (("" (inst - "f") nil nil)) nil)) nil)
((op_norm const-decl "{M: nnreal |
(FORALL (f: Funs): abs(L(f)) <= M * fun_norm(f)) AND
(FORALL (M1: real):
M1 < M IMPLIES
(EXISTS (f: Funs): abs(L(f)) > M1 * fun_norm(f)))}"
riesz_bounded_functionals nil)
(fun_norm const-decl "{M: nnreal |
(FORALL (x): abs(f(x)) <= M) AND
(FORALL (M1: real): M1 < M IMPLIES (EXISTS (x): abs(f(x)) > M1))}"
riesz_interval_funs nil)
(> const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bounded_on_int? const-decl "bool" riesz_interval_funs nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(bounded_op? const-decl "bool" riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(Funs formal-subtype-decl nil riesz_bounded_functionals nil)
(Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
riesz_bounded_functionals nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}"
riesz_bounded_functionals nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_bounded_functionals nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans 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))
shostak)))
¤ Dauer der Verarbeitung: 0.26 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.
|
