| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 2 MB |
|
Quellcode-Bibliothek riesz_hahn_banach.prfSprache: Lisp |
|||||||||||||||
|
(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 (("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 g (("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 = funcho (("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)) nil) ("2" (typepred "funchoose(gg)") (("2" (step_assert (skosimp*)) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1 2)) (("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) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "decompunique" -1) (("2" (case "NOT FORALL (fq:[INTab->real]): OE`space(fq) IMPLIES funchoose(fq) = fq AND constchoose(fq (("1" (skeep) (("1" (inst - "fq" "fq" "0") (("1" (assert) (("1" (split -) (("1" (ground) nil nil) ("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Extspace") (("2" (split +) (("1" (hide-all-but (-1 1)) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (expand "funs_bounded?") (("1" (flatten) (("1" (inst - "fq") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (inst + "fq" "0") (("2" (assert) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "OEdecomp" -1) (("2" (case "EXISTS (beta:real): FORALL (yy,hh:(OE`space)): -OEnorm*fun_norm[a,b](hh+ff)-OE`Lop( (("1" (label "betadef" -1) (("1" (skosimp*) (("1" (name "Extop" "(LAMBDA (gg:(Extspace)): OE`Lop(funchoose(gg)) + constchoose(gg)*beta!1)") (("1" (label "Extopname" -1) (("1" (case "NOT FORALL (f: ((Extspace))): abs(Extop(f)) <= OEnorm * fun_norm[a,b](f)") (("1" (hide "ExtExists") (("1" (skosimp*) (("1" (expand "Extop" +) (("1" (case "constchoose(f!1) = 0") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (case "f!1 = funchoose(f!1)") (("1" (typepred "OEnorm") (("1" (inst - "funchoose(f!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -2) (("2" (hide-all-but (-1 1)) (("2" (decompose-equality +) (("2" (decompose-equality -) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "spcfun" "(1/constchoose(f!1))*funchoose(f!1)") (("1" (label "spcfunname" -1) (("1" (case "constchoose(f!1)*spcfun = funchoose(f!1)") (("1" (label "fcmult" -1) (("1" (copy "betadef") (("1" (case "NOT bounded_on_int?[a, b] ((+[INTab])(funchoose(f!1), *[INTab](constchoose(f!1), ff)))") (("1" (hide-all-but 1) (("1" (typepred "ff") (("1" (expand "+") (("1" (expand "*") (("1" (typepred "funchoose(f!1)") (("1" (skosimp*) (("1" (hide -2) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_bounded?") (("1" (inst - "funchoose(f!1)") (("1" (expand "bounded_on_int?") (("1" (skosimp*) (("1" (inst + "M!1 + abs(constchoose(f!1))*M!2") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (copy -7) (("1" (copy -4) (("1" (mult-by -2 "abs(constchoose(f!1))") (("1" (hide-all-but (-1 -2 1)) (("1" (lemma "triangle") (("1" (inst?) (("1" (rewrite "abs_mult") (("1" (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) ("2" (label "boi" -1) (("2" (hide "boi") (("2" (expand "abs" +) (("2" (lift-if) (("2" (ground) (("1" (inst - "spcfun" "spcfun") (("1" (assert) (("1" (flatten) (("1" (case "constchoose(f!1) < 0") (("1" (mult-by -4 "-constchoose(f!1)") (("1" (assert) (("1" (case "fun_norm[a, b](spcfun + ff) * -constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constch (("1" (case "OE`Lop(spcfun) * -constchoose(f!1) = -OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (reveal "boi") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (mult-by -2 "constchoose(f!1)") (("2" (assert) (("2" (case "fun_norm[a, b](spcfun + ff) * constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constcho (("1" (case "OE`Lop(spcfun) * constchoose(f!1) = OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2 3)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (reveal "boi") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?" -1) (("2" (flatten) (("2" (expand "funs_const_closed?") (("2" (inst - "funchoose(f!1)" "(1 / constchoose(f!1))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (inst - "spcfun" "spcfun") (("1" (assert) (("1" (flatten) (("1" (case "constchoose(f!1) >= 0") (("1" (mult-by -3 "constchoose(f!1)") (("1" (assert) (("1" (case "fun_norm[a, b](spcfun + ff) * constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constcho (("1" (case "OE`Lop(spcfun) * constchoose(f!1) = OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (reveal "boi") (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (mult-by -1 "-constchoose(f!1)") (("2" (assert) (("2" (case "fun_norm[a, b](spcfun + ff) * -constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constch (("1" (case "OE`Lop(spcfun) * constchoose(f!1) = OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2 3)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (reveal "boi") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?" -1) (("2" (flatten) (("2" (expand "funs_const_closed?") (("2" (inst - "funchoose(f!1)" "(1 / constchoose(f!1))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace "spcfunname" + :dir rl) (("2" (hide-all-but (1 2)) (("2" (decompose-equality +) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (label "oplem" -1) (("2" (case "bounded_linear_operator?[a,b,(Extspace)](Extop)") (("1" (label "blop" -1) (("1" (name "Extn" "(# space:=Extspace, Lop := Extop #)") (("1" (label "Extnname" -1) (("1" (inst "ExtExists" "Extn") (("1" (assert) (("1" (expand "Extn" +) (("1" (expand "Extspace" +) (("1" (inst + "LAMBDA (x:INTab): 0" "1") (("1" (split) (("1" (hide-all-but "ExtExists") (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_contain_constants?") (("1" (inst - "0") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but "ExtExists") (("2" (decompose-equality) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (expand "Extn" +) (("1" (propax) nil nil)) nil) ("2" (expand "Extn" +) (("2" (propax) nil nil)) nil) ("3" (hide-all-but ("blop" 1)) (("3" (expand "Extn") (("3" (case "Extn`space = Extspace") (("1" (expand "bounded_linear_operator?") (("1" (flatten) (("1" (split) (("1" (expand "bounded_op?") (("1" (skosimp*) (("1" (inst + "M!1") (("1" (skosimp*) (("1" (inst - "f!1") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "linear_op?") (("2" (flatten) (("2" (split) (("1" (expand "additive_op?") (("1" (skosimp*) (("1" (inst - "f!1" "g!1") nil nil)) nil)) nil) ("2" (expand "const_inv_op?") (("2" (skosimp*) (("2" (inst - "f!1" "c!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Extn" 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("4" (expand "<=" 1) (("4" (split) (("1" (expand "subset?") (("1" (skeep) (("1" (assert) (("1" (expand "Extn" +) (("1" (expand "Extspace" +) (("1" (split +) (("1" (hide-all-but (-1 1)) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_bounded?") (("1" (inst - "x") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_on_int?") (("2" (ground) (("2" (inst + "x" "0") (("2" (assert) (("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" (skosimp*) (("2" (expand "Extn" +) (("2" (expand "Extop" +) (("2" (case "constchoose(ff!1) = 0") (("1" (replace -1) (("1" (assert) (("1" (inst "ggdecomp" "ff!1") (("1" (assert) (("1" (replace -1) (("1" (case "ff!1 = funchoose(ff!1)") (("1" (assert) nil nil) ("2" (hide-all-but ("ggdecomp" 1)) (("2" (decompose-equality) (("2" (decompose-equality -) (("2" (inst - "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst "OEdecomp" "ff!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (name "Extnnorm" "op_norm[a, b, ((Extn`space))](Extn`Lop)") (("1" (label "Extnnormname" -1) (("1" (replace "Extnnormname") (("1" (replace "OEnormname") (("1" (case "OEnorm < Extnnorm") (("1" (typepred "Extnnorm") (("1" (copy -3) (("1" (inst - "OEnorm") (("1" (assert) (("1" (skosimp*) (("1" (expand "Extn" -1) (("1" (inst "oplem" "f!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "OEnorm") (("2" (inst -3 "Extnnorm") (("2" (assert) (("2" (skosimp*) (("2" (typepred "Extnnorm") (("2" (inst - "f!1") (("1" (case "Extn`Lop(f!1) = OE`Lop(f!1)") (("1" (assert) nil nil) ("2" (expand "Extn" +) (("2" (expand "Extop" +) (("2" (case "constchoose(f!1) = 0") (("1" (case "f!1 = funchoose(f!1)") (("1" (replace -2) (("1" (assert) nil nil)) nil) ("2" (inst "ggdecomp" "f!1") (("2" (replace -1) (("2" (hide-all-but ("ggdecomp" 1)) (("2" (decompose-equality +) (("2" (decompose-equality -) (("2" (inst - "x!1") (("2" (grind :exclude "funchoose") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst "OEdecomp" "f!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Extn" +) (("2" (expand "Extspace" +) (("2" (assert) (("2" (split +) (("1" (hide-all-but 1) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (expand "bounded_on_int?") (("1" (flatten) (("1" (expand "funs_bounded?") (("1" (inst - "f!1") (("1" (expand "bounded_on_int?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "f!1" "0") (("2" (assert) (("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)) nil)) nil) ("2" (hide-all-but ("bls" 1)) (("2" (expand "fullset") (("2" (expand "extend") (("2" (expand "Extn") (("2" (case "Extspace = (LAMBDA (t: [INTab->real]): IF Extspace(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) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (expand "Extn") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but ("ffmember" 1 "oplem")) (("2" (expand "bounded_linear_operator?") (("2" (split) (("1" (expand "bounded_op?") (("1" (inst + "OEnorm") nil nil)) nil) ("2" (hide "oplem") (("2" (expand "linear_op?") (("2" (split) (("1" (expand "additive_op?") (("1" (skosimp*) (("1" (expand "Extop") (("1" (case "funchoose(f!1+g!1) = funchoose(f!1)+funchoose(g!1) AND constchoose(f!1+g!1) = constch (("1" (flatten) (("1" (replace -1) (("1" (replace -2) (("1" (hide -) (("1" (typepred "OE`Lop") (("1" (expand "bounded_linear_operator?") (("1" (flatten) (("1" (expand "linear_op?") (("1" (flatten) (("1" (expand "additive_op?") (("1" (inst - "funchoose(f!1)" "funchoose(g!1)") (("1" (replace -2) (("1" (hide -) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "decompunique") (("2" (inst - "f!1+g!1" "funchoose(f!1) + funchoose(g!1)" "constchoose(f!1) + constchoose(g!1)") (("1" (split -) (("1" (ground) nil nil) ("2" (hide 2) (("2" (reveal "ggdecomp") (("2" (inst-cp - "f!1") (("2" (inst - "g!1") (("2" (decompose-equality +) (("2" (decompose-equality -) (("2" (decompose-equality -) (("2" (inst - "x!1") (("2" (inst - "x!1") (("2" (grind :exclude ("funchoose" "constchoose")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_sum_closed?") (("2" (inst - "funchoose(f!1)" "funchoose(g!1)") (("1" (typepred "funchoose(g!1)") (("1" (skosimp*) nil nil)) nil) ("2" (typepred "funchoose(f!1)") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (reveal "bls") (("3" (hide-all-but ("bls" 1)) (("3" (expand "bounded_linear_subspace?") (("3" (flatten) (("3" (expand "funs_sum_closed?") (("3" (inst - "f!1" "g!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide "ffmember") (("2" (expand "const_inv_op?") (("2" (skosimp*) (("2" (expand "Extop") (("2" (case "funchoose(c!1*f!1) = c!1*funchoose(f!1) AND constchoose(c!1*f!1) = c!1*constchoose(f! (("1" (flatten) (("1" (typepred "OE`Lop") (("1" (expand "bounded_linear_operator?") (("1" (expand "linear_op?") (("1" (expand "const_inv_op?") (("1" (flatten) (("1" (inst - "funchoose(f!1)" "c!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal "decompunique") (("2" (inst - "c!1*f!1" "c!1 * funchoose(f!1)" "c!1 * constchoose(f!1)") (("1" (split -) (("1" (ground) nil nil) ("2" (hide 2) (("2" (reveal "ggdecomp") (("2" (inst - "f!1") (("2" (decompose-equality +) (("2" (decompose-equality -) (("2" (inst - "x!1") (("2" (mult-by -1 "c!1") (("2" (grind :exclude ("funchoose" "constchoose")) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (expand "funs_const_closed?") (("2" (flatten) (("2" (inst - "funchoose(f!1)" "c!1") (("2" (typepred "funchoose(f!1)") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (reveal "bls") (("3" (expand "bounded_linear_subspace?") (("3" (expand "funs_const_closed?") (("3" (flatten) (("3" (inst - "f!1" "c!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but ("bls" 1)) (("3" (expand "extend") (("3" (expand "fullset") (("3" (case "Extspace = (LAMBDA (t: [INTab->real]): IF (Extspace)(t) THEN TRUE ELSE FALSE ENDIF)") (("1" (assert) nil nil) ("2" (hide 2) (("2" (hide "bls") (("2" (decompose-equality +) (("2" (lift-if) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "f!1") (("3" (expand "Extspace") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "bounded_on_int?") (("2" (ground) (("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "funchoose(gg!1)") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "NOT FORALL (yy, hh: (OE`space)): -OEnorm * fun_norm[a, b](hh + ff) - OE`Lop(hh) <= OEnorm * fun_ (("1" (hide 2) (("1" (skeep) (("1" (typepred "OEnorm") (("1" (inst - "yy-hh") (("1" (case "OE`Lop(yy)-OE`Lop(hh) <= OEnorm*fun_norm[a,b](yy-hh)") (("1" (case "fun_norm[a,b](yy-hh) <= fun_norm[a,b](yy+ff) + fun_norm[a,b](hh+ff)") (("1" (mult-by -1 "OEnorm") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "fun_norm_triangle[a,b]") (("2" (inst - "yy+ff" "(-1)*hh+(-1)*ff") (("1" (case "yy + ff + ((-1) * hh + (-1) * ff) = yy-hh") (("1" (replace -1) (("1" (hide -1) (("1" (case "fun_norm[a,b]((-1) * hh + (-1) * ff) = fun_norm[a, b](hh + ff)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "hh+ff" "-1") (("2" (case "(-1) * hh + (-1) * ff = (-1)*(hh+ff)") (("1" (assert) (("1" (expand "abs") (("1" (assert) 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) ("2" (decompose-equality +) (("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "+") (("2" (expand "*") (("2" (expand "bounded_on_int?") (("2" (typepred "ff") (("2" (typepred "hh") (("2" (case "bounded_on_int?[a,b](hh)") (("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" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (expand "funs_bounded?") (("2" (flatten) (("2" (inst - "hh") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (flatten) (("2" (expand "const_inv_op?") (("2" (inst - "hh" "-1") (("2" (expand "additive_op?") (("2" (step_assert (inst - "yy" "-1*hh")) (("2" (case "yy+-1*hh = yy-hh") (("1" (replace -1) (("1" (replace -3) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) 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" (hide-all-but 1) (("2" (typepred "yy") (("2" (typepred "hh") (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_const_closed?") (("2" (inst - "hh" "-1") (("2" (expand "funs_sum_closed?") (("2" (inst - "yy" "-1*hh") (("1" (case "yy+-1*hh = yy-hh") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (name "Aset" "{Pr:real|EXISTS (hh:(OE`space)): Pr = -OEnorm * fun_norm[a, b](hh + ff) - OE`Lop(hh)}") (("1" (name "betas" "lub(Aset)") (("1" (inst + "betas") (("1" (skosimp*) (("1" (split +) (("1" (typepred "betas") (("1" (expand "least_upper_bound?") (("1" (flatten) (("1" (expand "upper_bound?" -1) (("1" (inst - "-OEnorm * fun_norm[a, b](hh!1 + ff) - OE`Lop(hh!1)") (("1" (expand "Aset" +) (("1" (inst + "hh!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "betas") (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (expand "upper_bound?" +) (("2" (skosimp*) (("2" (typepred "s!1") (("2" (expand "Aset" -1) (("2" (skosimp*) (("2" (inst - "yy!1" "hh!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (split) (("1" (name "zerfun" "LAMBDA (x:INTab): 0") (("1" (inst - "-OEnorm * fun_norm[a, b](zerfun + ff) - OE`Lop(zerfun)") (("1" (expand "Aset" +) (("1" (inst + "zerfun") (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_contain_constants?") (("1" (inst - "0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_contain_constants?") (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "zerfun + ff = ff") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (expand "zerfun") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (name "zerfun" "LAMBDA (x:INTab): 0") (("2" (expand "bounded_above?") (("2" (inst + "OEnorm * fun_norm[a, b](zerfun + ff) - OE`Lop(zerfun)") (("1" (expand "upper_bound?") (("1" (skosimp*) (("1" (typepred "s!1") (("1" (expand "Aset" -1) (("1" (skosimp*) (("1" (inst - "zerfun" "hh!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_contain_constants?") (("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "zerfun+ff = ff") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "zerfun") (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (case "bounded_on_int?[a,b](hh)") (("1" (typepred "ff") (("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)) nil) ("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_bounded?") (("2" (inst - "hh") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skeep) (("3" (case "bounded_on_int?[a,b](yy)") (("1" (typepred "ff") (("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)) nil) ("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_bounded?") (("2" (inst - "yy") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skeep) (("3" (hide -) (("3" (case "bounded_on_int?[a,b](yy)") (("1" (typepred "ff") (("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)) nil) ("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_bounded?") (("2" (inst - "yy") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skeep) (("4" (case "bounded_on_int?[a,b](hh)") (("1" (typepred "ff") (("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)) nil) ("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?") (("2" (flatten) (("2" (expand "funs_bounded?") (("2" (inst - "hh") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (typepred "funchoose(fq!1)") (("3" (skosimp*) (("3" (expand "Extspace") (("3" (assert) (("3" (split) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_bounded?") (("1" (inst - "funchoose(fq!1)") (("1" (expand "bounded_on_int?") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "funchoose(fq!1)" "ffc!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (skosimp*) (("4" (expand "Extspace") (("4" (split) (("1" (expand "bounded_on_int?") (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_bounded?") (("1" (inst - "fq!1") (("1" (assert) (("1" (expand "bounded_on_int?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "fq!1" "0") (("2" (assert) (("2" (decompose-equality +) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (typepred "gg") (("2" (expand "Extspace" -1) (("2" (flatten) (("2" (skosimp*) (("2" (inst - "ffc!1") (("2" (expand "member") (("2" (inst + "rr!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (typepred "gg") (("2" (expand "Extspace" -1) (("2" (flatten) (("2" (skosimp*) (("2" (inst - "rr!1") (("2" (expand "member" 1) (("2" (inst + "ffc!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide 2) (("2" (typepred "OE`space") (("2" (expand "extend") (("2" (expand "fullset") (("2" (case "OE`space = (LAMBDA (t: [INTab->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) ("3" (hide 2) (("3" (typepred "OE`Lop") (("3" (expand "bounded_linear_operator?") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (Extspace skolem-const-decl "[[INTab[a, b] -> real] -> boolean]" riesz_hahn_banach nil) (minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (member const-decl "bool" sets nil) (funs_sum_closed? const-decl "bool" riesz_function_sets nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (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) (OE skolem-const-decl "Op_Pair" riesz_hahn_banach nil) (rr!1 skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach 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_Function type-eq-decl nil riesz_interval_funs nil) (continuous_on_int? const-decl "bool" riesz_interval_funs nil) (f!1 skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach nil) (continuous_implies_bounded formula-decl nil riesz_interval_funs nil) (funs_contain_continuous? const-decl "bool" riesz_function_sets nil) (fq!1 skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (yy skolem-const-decl "(OE`space)" riesz_hahn_banach nil) (hh skolem-const-decl "(OE`space)" riesz_hahn_banach nil) (fun_norm_triangle formula-decl nil riesz_interval_funs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (empty? const-decl "bool" sets nil) (zerfun skolem-const-decl "[INTab[a, b] -> naturalnumber]" riesz_hahn_banach nil) (naturalnumber 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) (zerfun skolem-const-decl "[INTab[a, b] -> naturalnumber]" riesz_hahn_banach nil) (upper_bound? const-decl "bool" bounded_real_defs nil) (hh!1 skolem-const-decl "(OE`space)" riesz_hahn_banach nil) (OEnorm skolem-const-decl "{M: nnreal | (FORALL (f: ((OE`space))): abs(OE`Lop(f)) <= M * fun_norm(f)) AND (FORALL (M1: real): M1 < M IMPLIES (EXISTS (f: ((OE`space))): abs(OE`Lop(f)) > M1 * fun_norm(f)))}" riesz_hahn_banach nil) (Aset skolem-const-decl "[real -> boolean]" riesz_hahn_banach nil) (lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs nil) (least_upper_bound? const-decl "bool" bounded_real_defs nil) (bounded_above? const-decl "bool" bounded_real_defs nil) (f!1 skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (triangle formula-decl nil real_props nil) (spcfun skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach nil) (constchoose skolem-const-decl "[gg: (Extspace) -> ({ffc: real | EXISTS (rr: [INTab -> real]): OE`space(rr) AND gg = rr + ffc * ff})]" riesz_hahn_banach nil) (const_inv_op? const-decl "bool" riesz_linear_functionals nil) (linear_op? const-decl "bool" riesz_linear_functionals nil) (fun_norm_scal formula-decl nil riesz_interval_funs nil) (Extop skolem-const-decl "[(Extspace) -> real]" riesz_hahn_banach nil) (Extn skolem-const-decl "[# Lop: [(Extspace) -> real], space: [[INTab[a, b] -> real] -> boolean] #]" riesz_hahn_banach nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" riesz_hahn_banach nil) (Op_Extension type-eq-decl nil riesz_hahn_banach nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (f!1 skolem-const-decl "((OE`space))" riesz_hahn_banach nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (subset? const-decl "bool" sets nil) (additive_op? const-decl "bool" riesz_linear_functionals nil) (g!1 skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (f!1 skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (c!1 skolem-const-decl "real" riesz_hahn_banach nil) (f!1 skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (fq skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach nil) (fq skolem-const-decl "(OE`space)" riesz_hahn_banach nil) (gg skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (rr!1 skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach nil) (fq skolem-const-decl "(OE`space)" riesz_hahn_banach nil) (gg skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (div_cancel4 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div2 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (ff skolem-const-decl "Bounded_Function[a, b]" riesz_hahn_banach nil) (funchoose skolem-const-decl "[gg: (Extspace) -> ({rr: [INTab -> real] | EXISTS (ffc: real): OE`space(rr) AND gg = rr + ffc * ff})]" riesz_hahn_banach nil) (gg skolem-const-decl "(Extspace)" riesz_hahn_banach nil) (fq skolem-const-decl "[INTab[a, b] -> real]" riesz_hahn_banach nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (Bounded_Function type-eq-decl nil riesz_interval_funs nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (fullset const-decl "set" 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) (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) (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) (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) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil) (Op_Extension_exists-4 nil 3565654845 ("" (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 (("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))))))))))))) ("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))))))))) ("2" (replace -3) (("2" (replace -6) (("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (grind) 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))))))))))))))))))))) ("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))))))))) ("2" (replace -3) (("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (grind) nil))))))))))))))))))))))))) ("3" (expand "funs_bounded?") (("3" (skosimp*) (("3" (typepred "f!1") (("3" (expand "Extspace") (("3" (flatten) 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))))) ("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))))))))) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (grind) 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))) ("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))))))))))) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (grind) 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 g (("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))))))) ("2" (assert) (("2" (typepred "funchoose(gg)") (("2" (skosimp*) 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))))))))))))))))))))))))))))))))) ("2" (label "funchooseunique" -1) (("2" (case "NOT FORALL (gg:(Extspace), fq:(OE`space)): gg = fq + constchoose(gg)*ff IMPLIES fq = funcho (("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))))))))))))))) ("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))))))))))))))))) ("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))))))))))))))))))))))) ("3" (assert) 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))))))))) ("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))))) ("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" (inst - "funchoose(gg)" "(-1)*fq") (("1" (inst - "funchoose(gg) + (-1) * fq" "(1 / (rr - constchoose(gg)))") (("1" (assert) nil))) ("2" (typepred "funchoose(gg)") (("2" (skosimp*) (("2" (assert) nil))))) ("3" (assert) nil))))))))))))))) ("2" (hide-all-but (-1 -2 1 2)) (("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))))))))))))))))))))) ("3" (assert) nil))))))))))) ("2" (label "decompunique" -1) (("2" (case "NOT FORALL (fq:[INTab->real]): OE`space(fq) IMPLIES funchoose(fq) = fq AND constchoose(fq (("1" (skeep) (("1" (inst - "fq" "fq" "0") (("1" (assert) (("1" (split -) (("1" (ground) nil) ("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind) nil))))))))) ("2" (hide 2) (("2" (expand "Extspace") (("2" (split +) (("1" (hide-all-but (-1 1)) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (expand "funs_bounded?") (("1" (flatten) (("1" (inst - "fq") nil))))))))))) ("2" (hide-all-but (-1 1)) (("2" (inst + "fq" "0") (("2" (assert) (("2" (decompose-equality +) (("2" (grind) nil))))))))))))))))))) ("2" (label "OEdecomp" -1) (("2" (case "EXISTS (beta:real): FORALL (yy,hh:(OE`space)): -OEnorm*fun_norm[a,b](hh+ff)-OE`Lop( (("1" (label "betadef" -1) (("1" (skosimp*) (("1" (name "Extop" "(LAMBDA (gg:(Extspace)): OE`Lop(funchoose(gg)) + constchoose(gg)*beta!1)") (("1" (label "Extopname" -1) (("1" (case "NOT FORALL (f: ((Extspace))): abs(Extop(f)) <= OEnorm * fun_norm[a,b](f)") (("1" (hide "ExtExists") (("1" (skosimp*) (("1" (expand "Extop" +) (("1" (case "constchoose(f!1) = 0") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (case "f!1 = funchoose(f!1)") (("1" (typepred "OEnorm") (("1" (inst - "funchoose(f!1)") (("1" (assert) nil))))) ("2" (replace -2) (("2" (hide-all-but (-1 1)) (("2" (decompose-equality +) (("2" (decompose-equality -) (("2" (grind) nil))))))))))))))) ("2" (name "spcfun" "(1/constchoose(f!1))*funchoose(f!1)") (("1" (label "spcfunname" -1) (("1" (case "constchoose(f!1)*spcfun = funchoose(f!1)") (("1" (label "fcmult" -1) (("1" (copy "betadef") (("1" (case "NOT bounded_on_int?[a, b] ((+[INTab])(funchoose(f!1), *[INTab](constchoose(f!1), ff)))") (("1" (hide-all-but 1) (("1" (typepred "ff") (("1" (expand "+") (("1" (expand "*") (("1" (typepred "funchoose(f!1)") (("1" (skosimp*) (("1" (hide -2) (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_bounded?") (("1" (inst - "funchoose(f!1)") (("1" (expand "bounded_on_int?") (("1" (skosimp*) (("1" (inst + "M!1 + abs(constchoose(f!1))*M!2") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (copy -7) (("1" (copy -4) (("1" (mult-by -2 "abs(constchoose(f!1))") (("1" (hide-all-but (-1 -2 1)) (("1" (lemma "triangle") (("1" (inst?) (("1" (rewrite "abs_mult") (("1" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (label "boi" -1) (("2" (hide "boi") (("2" (expand "abs" +) (("2" (lift-if) (("2" (ground) (("1" (inst - "spcfun" "spcfun") (("1" (assert) (("1" (flatten) (("1" (case "constchoose(f!1) < 0") (("1" (mult-by -4 "-constchoose(f!1)") (("1" (assert) (("1" (case "fun_norm[a, b](spcfun + ff) * -constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constch (("1" (case "OE`Lop(spcfun) * -constchoose(f!1) = -OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil))))) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil))))))))))))))))))) ("3" (reveal "boi") (("3" (propax) nil))))))))) ("2" (mult-by -2 "constchoose(f!1)") (("2" (assert) (("2" (case "fun_norm[a, b](spcfun + ff) * constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constcho (("1" (case "OE`Lop(spcfun) * constchoose(f!1) = OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil))))) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2 3)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil))))))))))))))))))) ("3" (reveal "boi") (("3" (propax) nil))))))))))))))) ("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?" -1) (("2" (flatten) (("2" (expand "funs_const_closed?") (("2" (inst - "funchoose(f!1)" "(1 / constchoose(f!1))") (("2" (assert) nil))))))))))))) ("2" (hide 1) (("2" (inst - "spcfun" "spcfun") (("1" (assert) (("1" (flatten) (("1" (case "constchoose(f!1) >= 0") (("1" (mult-by -3 "constchoose(f!1)") (("1" (assert) (("1" (case "fun_norm[a, b](spcfun + ff) * constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constcho (("1" (case "OE`Lop(spcfun) * constchoose(f!1) = OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil))))) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil))))))))))))))))))) ("3" (reveal "boi") (("3" (propax) nil))))))))) ("2" (mult-by -1 "-constchoose(f!1)") (("2" (assert) (("2" (case "fun_norm[a, b](spcfun + ff) * -constchoose(f!1) = fun_norm[a,b](funchoose(f!1) + constch (("1" (case "OE`Lop(spcfun) * constchoose(f!1) = OE`Lop(funchoose(f!1))") (("1" (copy "ggdecomp") (("1" (inst - "f!1") (("1" (assert) nil))))) ("2" (hide-all-but ("fcmult" 1)) (("2" (typepred "OE`Lop") (("2" (expand "bounded_linear_operator?") (("2" (expand "linear_op?") (("2" (expand "const_inv_op?") (("2" (flatten) (("2" (inst - "spcfun" "constchoose(f!1)") (("2" (assert) nil))))))))))))))))) ("2" (hide 2) (("2" (hide-all-but ("fcmult" 1 -2 3)) (("2" (lemma "fun_norm_scal[a,b]") (("2" (inst - "spcfun + ff" "constchoose(f!1)") (("2" (expand "abs" -1) (("2" (case "constchoose(f!1) * (spcfun + ff) = funchoose(f!1) + constchoose(f!1) * ff") (("1" (assert) nil) ("2" (replace "fcmult" :dir rl) (("2" (hide-all-but 1) (("2" (decompose-equality +) (("2" (grind :exclude ("constchoose" "funchoose" "spcfun")) nil))))))))))))))))))) ("3" (reveal "boi") (("3" (propax) nil))))))))))))))) ("2" (typepred "OE`space") (("2" (expand "bounded_linear_subspace?" -1) (("2" (flatten) (("2" (expand "funs_const_closed?") (("2" (inst - "funchoose(f!1)" "(1 / constchoose(f!1))") (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (replace "spcfunname" + :dir rl) (("2" (hide-all-but (1 2)) (("2" (decompose-equality +) (("2" (expand "*") (("2" (assert) nil))))))))))))) ("2" (assert) nil))))))))))) ("2" (label "oplem" -1) (("2" (case "bounded_linear_operator?[a,b,(Extspace)](Extop)") (("1" (label "blop" -1) (("1" (name "Extn" "(# space:=Extspace, Lop := Extop #)") (("1" (label "Extnname" -1) (("1" (inst "ExtExists" "Extn") (("1" (assert) (("1" (expand "Extn" +) (("1" (expand "Extspace" +) (("1" (inst + "LAMBDA (x:INTab): 0" "1") (("1" (split) (("1" (hide-all-but "ExtExists") (("1" (typepred "OE`space") (("1" (expand "bounded_linear_subspace?") (("1" (flatten) (("1" (expand "funs_contain_constants?") (("1" (inst - "0") nil))))))))))) ("2" (hide-all-but "ExtExists") (("2" (decompose-equality) (("2" (grind) nil))))))))))))))) ("2" (split) (("1" (expand "Extn" +) (("1" (propax) nil))) ("2" (expand "Extn" +) (("2" (propax) nil))) ("3" (hide-all-but ("blop" 1)) (("3" (expand "Extn") (("3" (case "Extn`space = Extspace") (("1" (expand "bounded_linear_operator?") (("1" (flatten) (("1" (split) (("1" (expand "bounded_op?") (("1" (skosimp*) (("1" (inst + "M!1") (("1" (skosimp*) (("1" (inst - "f!1") nil))))))))) ("2" (expand "linear_op?") (("2" (flatten) (("2" (split) (("1" (expand "additive_op?") (("1" (skosimp*) (("1" (inst - "f!1" "g!1") nil))))) ("2" (expand "const_inv_op?") (("2" (skosimp*) (("2" (inst --> -------------------- --> maximum size reached --> --------------------
¤ 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.0.744Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26