|
(riesz_hahn_banach
(C_Bounded_Linear_Operator_TCC1 0
(C_Bounded_Linear_Operator_TCC1-1 nil 3493138877
("" (expand "bounded_linear_subspace?")
(("" (expand "extend")
(("" (expand "fullset")
(("" (split)
(("1" (expand "funs_sum_closed?")
(("1" (skosimp*)
(("1" (ground)
(("1" (expand "continuous_on_int?")
(("1" (lemma "sum_continuous")
(("1" (inst?)
(("1" (assert)
(("1" (typepred "f!1")
(("1" (typepred "g!1")
(("1" (expand "continuous_on_int?")
(("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "funs_const_closed?")
(("2" (skeep)
(("2" (ground)
(("2" (lemma "scal_continuous")
(("2" (inst?)
(("2" (expand "continuous_on_int?")
(("2" (inst?)
(("2" (assert)
(("2" (typepred "f")
(("2" (expand "continuous_on_int?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "funs_bounded?")
(("3" (skeep)
(("3" (lemma "continuous_implies_bounded[a,b]")
(("3" (inst - "f") nil nil)) nil))
nil))
nil)
("4" (grind) nil nil)
("5" (grind :exclude "continuous?") nil nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(continuous_on_int? const-decl "bool" riesz_interval_funs nil)
(FALSE const-decl "bool" booleans nil)
(TRUE const-decl "bool" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Intab const-decl "set[real]" riesz_interval_funs nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sum_continuous formula-decl nil metric_space_real_fun 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_hahn_banach nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(restrict const-decl "R" restrict nil)
(real_dist const-decl "nnreal" real_metric_space nil)
(funs_sum_closed? const-decl "bool" riesz_function_sets nil)
(scal_continuous formula-decl nil metric_space_real_fun nil)
(funs_const_closed? const-decl "bool" riesz_function_sets nil)
(Continuous_Function type-eq-decl nil riesz_interval_funs nil)
(continuous_implies_bounded formula-decl nil riesz_interval_funs
nil)
(funs_bounded? const-decl "bool" riesz_function_sets nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(ball const-decl "set[T]" metric_spaces nil)
(member const-decl "bool" sets nil)
(continuous_at? const-decl "bool" continuity_ms_def nil)
(continuous? const-decl "bool" continuity_ms_def nil)
(funs_contain_constants? const-decl "bool" riesz_function_sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(funs_contain_continuous? const-decl "bool" riesz_function_sets
nil)
(fullset const-decl "set" sets nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil))
nil))
(B_Bounded_Linear_Operator_TCC1 0
(B_Bounded_Linear_Operator_TCC1-1 nil 3493138877
("" (expand "bounded_linear_subspace?")
(("" (expand "extend")
(("" (expand "fullset")
(("" (split)
(("1" (expand "funs_sum_closed?")
(("1" (skosimp*)
(("1" (ground)
(("1" (typepred "f!1")
(("1" (typepred "g!1")
(("1" (expand "bounded_on_int?")
(("1" (skosimp*)
(("1" (inst + "M!1+M!2")
(("1" (skeep)
(("1" (inst - "x")
(("1"
(inst - "x")
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "funs_const_closed?")
(("2" (skeep)
(("2" (ground)
(("2" (typepred "f")
(("2" (expand "bounded_on_int?")
(("2" (skosimp*)
(("2" (inst + "M!1*abs(c)")
(("2" (skeep)
(("2" (inst - "x")
(("2" (expand "*")
(("2"
(rewrite "abs_mult")
(("2"
(mult-by -1 "abs(c)")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "funs_bounded?") (("3" (propax) nil nil)) nil)
("4" (expand "funs_contain_constants?")
(("4" (skeep)
(("4" (ground)
(("4" (expand "bounded_on_int?")
(("4" (inst + "abs(c)") (("4" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
("5" (expand "funs_contain_continuous?")
(("5" (skeep)
(("5" (ground)
(("5" (lemma "continuous_implies_bounded[a,b]")
(("5" (inst - "f") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(TRUE const-decl "bool" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(bounded_on_int? const-decl "bool" riesz_interval_funs nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(FALSE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real_plus_real_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)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(funs_sum_closed? const-decl "bool" riesz_function_sets nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(abs_mult formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(funs_const_closed? const-decl "bool" riesz_function_sets nil)
(funs_bounded? const-decl "bool" riesz_function_sets nil)
(funs_contain_constants? const-decl "bool" riesz_function_sets nil)
(continuous_implies_bounded formula-decl nil riesz_interval_funs
nil)
(Continuous_Function type-eq-decl nil riesz_interval_funs nil)
(continuous_on_int? const-decl "bool" riesz_interval_funs nil)
(funs_contain_continuous? const-decl "bool" riesz_function_sets
nil)
(fullset const-decl "set" sets nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil))
nil))
(lesseqp_TCC1 0
(lesseqp_TCC1-1 nil 3493984769 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(lesseqp_TCC2 0
(lesseqp_TCC2-1 nil 3493989932
("" (skeep)
(("" (expand "bounded_op?")
(("" (typepred "OE`Lop")
(("" (expand "bounded_linear_operator?")
(("" (flatten)
(("" (expand "bounded_op?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((bounded_op? const-decl "bool" riesz_bounded_functionals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(set type-eq-decl nil sets nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_linear_operator? const-decl "bool"
riesz_bounded_functionals nil)
(Op_Pair type-eq-decl nil riesz_hahn_banach nil))
nil))
(lesseqp_TCC3 0
(lesseqp_TCC3-1 nil 3493989932
("" (skeep)
(("" (typepred "OE`space")
(("" (expand "extend")
(("" (expand "fullset")
(("" (hide -2)
(("" (hide -2)
((""
(case "OE`space = (LAMBDA (t: [INTab[a, b] -> real]):
IF (OE`space)(t) THEN TRUE ELSE FALSE ENDIF)")
(("1" (assert) nil nil)
("2" (hide-all-but 1)
(("2" (decompose-equality)
(("2" (lift-if) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Op_Pair type-eq-decl nil riesz_hahn_banach nil)
(bounded_linear_operator? const-decl "bool"
riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(set type-eq-decl nil sets nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" 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)
(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)
(fullset const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(TRUE const-decl "bool" booleans nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil))
nil))
(lesseqp_TCC4 0
(lesseqp_TCC4-1 nil 3493989932
("" (skeep)
(("" (typepred "Ext`Lop")
(("" (expand "bounded_linear_operator?") (("" (flatten) nil nil))
nil))
nil))
nil)
((Op_Pair type-eq-decl nil riesz_hahn_banach nil)
(bounded_linear_operator? const-decl "bool"
riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(set type-eq-decl nil sets nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" 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)
(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))
(lesseqp_TCC5 0
(lesseqp_TCC5-1 nil 3493989932
("" (skeep)
(("" (typepred "Ext`space")
(("" (hide -2)
(("" (hide -2)
(("" (expand "fullset")
(("" (expand "extend")
((""
(case "Ext`space = (LAMBDA (t: [INTab[a, b] -> real]):
IF (Ext`space)(t) THEN TRUE ELSE FALSE ENDIF)")
(("1" (assert) nil nil)
("2" (decompose-equality)
(("2" (lift-if) (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Op_Pair type-eq-decl nil riesz_hahn_banach nil)
(bounded_linear_operator? const-decl "bool"
riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(set type-eq-decl nil sets nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" 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)
(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)
(extend const-decl "R" extend nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(TRUE const-decl "bool" booleans nil)
(FALSE const-decl "bool" booleans nil)
(fullset const-decl "set" sets nil))
nil))
(Hahn_Banach_partial_order 0
(Hahn_Banach_partial_order-1 nil 3493984770
("" (expand "partial_order?")
(("" (expand "preorder?")
(("" (expand "reflexive?")
(("" (expand "transitive?")
(("" (expand "antisymmetric?")
(("" (split)
(("1" (skolem 1 "OE")
(("1" (expand "<=")
(("1" (expand "subset?") (("1" (skeep) nil nil))
nil))
nil))
nil)
("2" (skolem 1 ("oe1" "oe2" "oe3"))
(("2" (flatten)
(("2" (expand "<=")
(("2" (flatten)
(("2" (split)
(("1" (hide -2)
(("1" (expand "subset?")
(("1" (skeep)
(("1"
(inst - "x")
(("1"
(inst - "x")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (inst - "ff")
(("2" (inst - "ff")
(("2"
(assert)
(("2"
(expand "subset?")
(("2"
(inst - "ff")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (skolem 1 ("oe1" "oe2"))
(("3" (flatten)
(("3" (assert)
(("3" (expand "<=")
(("3" (flatten)
(("3" (case "oe1`space = oe2`space")
(("1" (decompose-equality +)
(("1" (decompose-equality +)
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (decompose-equality 1)
(("2" (hide -2)
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2"
(inst - "x!1")
(("2"
(assert)
(("2"
(iff)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(<= const-decl "bool" riesz_hahn_banach nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach 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)
(Op_Pair type-eq-decl nil riesz_hahn_banach nil)
(bounded_linear_operator? const-decl "bool"
riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(antisymmetric? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil))
shostak))
(Hahn_Banach_partial_order_sub 0
(Hahn_Banach_partial_order_sub-1 nil 3494059940
("" (skeep)
(("" (lemma "Hahn_Banach_partial_order")
(("" (expand "partial_order?")
(("" (flatten)
(("" (split)
(("1" (hide -2)
(("1" (expand "preorder?")
(("1" (flatten)
(("1" (split)
(("1" (hide -2)
(("1" (expand "reflexive?")
(("1" (skeep)
(("1" (inst - "x")
(("1" (expand "le")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (expand "transitive?")
(("2" (skeep)
(("2" (inst - "x" "y" "z")
(("2" (expand "le")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (expand "antisymmetric?")
(("2" (skeep)
(("2" (inst - "x" "y")
(("2" (expand "le") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Hahn_Banach_partial_order formula-decl nil riesz_hahn_banach nil)
(antisymmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(le const-decl "bool" riesz_hahn_banach nil)
(Op_Extension type-eq-decl nil riesz_hahn_banach nil)
(<= const-decl "bool" riesz_hahn_banach nil)
(Op_Pair type-eq-decl nil riesz_hahn_banach nil)
(bounded_linear_operator? const-decl "bool"
riesz_bounded_functionals nil)
(Operator type-eq-decl nil riesz_linear_functionals nil)
(bounded_linear_subspace? const-decl "bool" riesz_function_sets
nil)
(set type-eq-decl nil sets nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_hahn_banach nil)
(< const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_hahn_banach 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)
(reflexive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(partial_order? const-decl "bool" orders nil))
shostak))
(Op_Extension_exists 0
(Op_Extension_exists-5 nil 3565655758
(""
(deftactic step_assert (step)
(branch step ((skip) (finalize (assert)))))
(("" (skeep)
(("" (name "OEnorm" "op_norm[a, b, ((OE`space))](OE`Lop)")
(("1" (label "OEnormname" -1)
(("1"
(name "Extspace"
"{gg:[INTab->real] | bounded_on_int?[a,b](gg) AND EXISTS (rr: [INTab->real],ffc:real): OE`space(rr) AND gg = rr + ffc*ff}")
(("1" (case "NOT bounded_linear_subspace?[a,b](Extspace)")
(("1" (hide 3)
(("1" (hide -)
(("1" (expand "bounded_linear_subspace?")
(("1" (split)
(("1" (expand "funs_sum_closed?")
(("1" (skosimp*)
(("1" (ground)
(("1" (typepred "f!1")
(("1"
(typepred "g!1")
(("1"
(expand "Extspace")
(("1"
(flatten)
(("1"
(split)
(("1"
(expand "bounded_on_int?")
(("1"
(skosimp*)
(("1"
(inst + "M!1 + M!2")
(("1"
(skosimp*)
(("1"
(inst - "x!1")
(("1"
(inst - "x!1")
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst
+
"rr!1+rr!2"
"ffc!1+ffc!2")
(("2"
(assert)
(("2"
(split +)
(("1"
(typepred "OE`space")
(("1"
(expand
"bounded_linear_subspace?")
(("1"
(flatten)
(("1"
(expand
"funs_sum_closed?")
(("1"
(inst
-
"rr!1"
"rr!2")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace -3)
(("2"
(replace -6)
(("2"
(hide-all-but 1)
(("2"
(decompose-equality)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "funs_const_closed?")
(("2" (skosimp*)
(("2" (typepred "f!1")
(("2" (expand "Extspace")
(("2"
(flatten)
(("2"
(split)
(("1"
(hide -2)
(("1"
(expand "bounded_on_int?")
(("1"
(skosimp*)
(("1"
(expand "*")
(("1"
(assert)
(("1"
(inst + "abs(c!1)*M!1")
(("1"
(skosimp*)
(("1"
(inst - "x!1")
(("1"
(rewrite
"abs_mult")
(("1"
(mult-by
-1
"abs(c!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst + "c!1*rr!1" "c!1*ffc!1")
(("2"
(split)
(("1"
(typepred "OE`space")
(("1"
(expand
"bounded_linear_subspace?")
(("1"
(flatten)
(("1"
(expand
"funs_const_closed?")
(("1"
(inst - "rr!1" "c!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(replace -3)
(("2"
(hide-all-but 1)
(("2"
(decompose-equality)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "funs_bounded?")
(("3" (skosimp*)
(("3" (typepred "f!1")
(("3" (expand "Extspace")
(("3" (flatten) nil nil)) nil))
nil))
nil))
nil)
("4" (ground)
(("4" (expand "funs_contain_constants?")
(("4" (skosimp*)
(("4" (expand "Extspace" +)
(("4"
(split)
(("1"
(expand "bounded_on_int?")
(("1"
(inst + "abs(c!1)")
(("1" (grind) nil nil))
nil))
nil)
("2"
(inst + "LAMBDA (y:INTab): c!1" "0")
(("2"
(split +)
(("1"
(typepred "OE`space")
(("1"
(expand
"bounded_linear_subspace?")
(("1"
(flatten)
(("1"
(expand
"funs_contain_constants?")
(("1"
(inst - "c!1")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(decompose-equality)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (expand "funs_contain_continuous?")
(("5" (skosimp*)
(("5" (expand "Extspace")
(("5" (split)
(("1"
(lemma
"continuous_implies_bounded[a,b]")
(("1" (inst - "f!1") nil nil))
nil)
("2"
(inst + "f!1" "0")
(("2"
(split)
(("1"
(typepred "OE`space")
(("1"
(expand
"bounded_linear_subspace?")
(("1"
(flatten)
(("1"
(expand
"funs_contain_continuous?")
(("1"
(inst - "f!1")
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(decompose-equality)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (label "bls" -1)
(("2" (label "Extspacename" -2)
(("2" (label "ffmember" 1)
(("2" (label "ExtExists" 2)
(("2"
(name "funchoose"
"LAMBDA (gg:(Extspace)): choose({rr:[INTab->real]|EXISTS (ffc:real):OE`space(rr) AND gg = rr + ffc * ff})")
(("1" (label "funchoosename" -1)
(("1"
(name "constchoose"
"(LAMBDA (gg: (Extspace)):
choose({ffc: real |
EXISTS (rr: [INTab->real]):
OE`space(rr) AND gg = rr + ffc * ff}))")
(("1" (label "constchoosename" -1)
(("1"
(case
"NOT FORALL (gg:(Extspace),rr:real): gg = funchoose(gg) + rr*ff IMPLIES rr = constchoose(gg)")
(("1"
(skeep)
(("1"
(typepred "constchoose(gg)")
(("1"
(skolem -1 "fq")
(("1"
(assert)
(("1"
(flatten)
(("1"
(case
"ff = (1/(rr-constchoose(gg)))*(fq+(-1)*funchoose(gg))")
(("1"
(typepred "OE`space")
(("1"
(expand
"bounded_linear_subspace?"
-1)
(("1"
(flatten)
(("1"
(expand
"funs_const_closed?")
(("1"
(inst-cp
-
"funchoose(gg)"
"-1")
(("1"
(expand
"funs_sum_closed?")
(("1"
(step_assert
(inst
-
"fq"
"(-1) * funchoose(gg)"))
(("1"
(step_assert
(inst
-
"fq + (-1) * funchoose(gg)"
"(1 / (rr - constchoose(gg)))"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred
"funchoose(gg)")
(("2"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-2 -3 1))
(("2"
(decompose-equality +)
(("2"
(decompose-equality
-)
(("2"
(decompose-equality
-)
(("2"
(inst - "x!1")
(("2"
(inst - "x!1")
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(expand
"*")
(("2"
(cross-mult
1)
(("2"
(grind
:exclude
("funchoose"
"constchoose"))
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(label "funchooseunique" -1)
(("2"
(case
"NOT FORALL (gg:(Extspace), fq:(OE`space)): gg = fq + constchoose(gg)*ff IMPLIES fq = funchoose(gg)")
(("1"
(skeep)
(("1"
(typepred "funchoose(gg)")
(("1"
(skosimp*)
(("1"
(case
"ffc!1 = constchoose(gg)")
(("1"
(replace -1)
(("1"
(hide-all-but
(-3 -4 1))
(("1"
(decompose-equality
+)
(("1"
(decompose-equality
-)
(("1"
(decompose-equality
-)
(("1"
(inst - "x!1")
(("1"
(inst
-
"x!1")
(("1"
(grind
:exclude
("funchoose"
"constchoose"))
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"ff = (1/(ffc!1-constchoose(gg)))*(fq+(-1)*funchoose(gg))")
(("1"
(typepred "OE`space")
(("1"
(expand
"bounded_linear_subspace?"
-1)
(("1"
(flatten)
(("1"
(expand
"funs_const_closed?")
(("1"
(inst-cp
-
"funchoose(gg)"
"-1")
(("1"
(expand
"funs_sum_closed?")
(("1"
(step_assert
(inst
-
"fq"
"-1 * funchoose(gg)"))
(("1"
(step_assert
(inst
-
"fq + -1 * funchoose(gg)"
"(1 / (ffc!1 - constchoose(gg)))"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-2 -3 1))
(("2"
(decompose-equality
+)
(("2"
(decompose-equality
-)
(("2"
(decompose-equality
-)
(("2"
(inst - "x!1")
(("2"
(inst
-
"x!1")
(("2"
(replace
-1)
(("2"
(hide -1)
(("2"
(expand
"*")
(("2"
(cross-mult
1)
(("2"
(assert)
(("2"
(grind
:exclude
("funchoose"
"constchoose"))
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(label "funchooseunique2" -1)
(("2"
(case
"NOT FORALL (gg:(Extspace)): gg = funchoose(gg) + constchoose(gg)*ff")
(("1"
(skeep)
(("1"
(typepred
"constchoose(gg)")
(("1"
(skosimp*)
(("1"
(inst
"funchooseunique2"
"gg"
"rr!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(label "ggdecomp" -1)
(("2"
(case
"NOT FORALL (gg: (Extspace), fq: (OE`space), rr:real):
gg = fq + rr * ff IMPLIES fq = funchoose(gg) AND rr = constchoose(gg)")
(("1"
(skeep)
(("1"
(case
"rr = constchoose(gg)")
(("1"
(assert)
(("1"
(inst
"funchooseunique2"
"gg"
"fq")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(inst
"ggdecomp"
"gg")
(("2"
(case
"ff = (1/(rr-constchoose(gg)))*(funchoose(gg)+(-1)*fq)")
(("1"
(typepred
"OE`space")
(("1"
(expand
"bounded_linear_subspace?"
-1)
(("1"
(flatten)
(("1"
(expand
"funs_const_closed?")
(("1"
(inst-cp
-
"fq"
"-1")
(("1"
(expand
"funs_sum_closed?")
(("1"
(step_assert
(inst
-
"funchoose(gg)"
"(-1)*fq"))
(("1"
(step_assert
(inst
-
"funchoose(gg) + (-1) * fq"
"(1 / (rr - constchoose(gg)))"))
(("1"
(assert)
nil
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.373Angebot
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
|
