|
(sup_norm
(bounded_TCC1 0
(bounded_TCC1-1 nil 3392430087
("" (expand "bounded?")
(("" (inst + "0") (("" (grind) nil nil)) nil)) 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)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(bounded? const-decl "bool" sup_norm nil))
nil))
(bounded_add 0
(bounded_add-1 nil 3392432560
("" (skosimp)
(("" (typepred "f1!1")
(("" (typepred "f2!1")
(("" (expand "+")
(("" (expand "bounded?")
(("" (skosimp*)
(("" (inst + "c!1+c!2")
(("" (skosimp)
(("" (inst - "x!1")
(("" (inst - "x!1") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm 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)
(T formal-type-decl nil sup_norm nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(minus_real_is_real application-judgement "real" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
nil))
(bounded_scal 0
(bounded_scal-1 nil 3392432560
("" (skosimp)
(("" (expand "*")
(("" (typepred "f!1")
(("" (expand "bounded?")
(("" (skosimp)
(("" (inst + " abs(y!1)*c!1")
(("" (skosimp)
(("" (inst - "x!1")
(("" (rewrite "abs_mult")
(("" (typepred "abs(y!1)")
(("" (hide -2 -3)
(("" (expand ">=")
(("" (expand "<=" -1)
(("" (split -1)
(("1"
(lemma
"both_sides_times_pos_le1"
("pz"
"abs(y!1)"
"x"
"abs(f!1(x!1))"
"y"
"c!1"))
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("2"
(replace -1 * rl)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(abs_mult formula-decl nil real_props nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil sup_norm 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)
(bounded? const-decl "bool" sup_norm nil)
(bounded nonempty-type-eq-decl nil sup_norm nil))
nil))
(bounded_opp 0
(bounded_opp-1 nil 3392432840
("" (skosimp)
(("" (lemma "bounded_scal" ("y" "-1" "f" "f!1"))
(("" (expand "*") (("" (expand "-") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm 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)
(T formal-type-decl nil sup_norm nil)
(bounded_scal judgement-tcc nil sup_norm nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(bounded_diff 0
(bounded_diff-1 nil 3392432560
("" (skosimp)
(("" (typepred "f2!1")
(("" (lemma "bounded_opp" ("f" "f2!1"))
(("" (lemma "bounded_add" ("f1" "f1!1" "f2" "-f2!1"))
(("" (expand "+")
(("" (expand "-") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm 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)
(T formal-type-decl nil sup_norm nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bounded_opp application-judgement "bounded" sup_norm nil)
(bounded_add judgement-tcc nil sup_norm nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(bounded_opp judgement-tcc nil sup_norm nil))
nil))
(sup_norm_TCC1 0
(sup_norm_TCC1-1 nil 3392429651
("" (skosimp*)
(("" (split)
(("1" (expand "extend")
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (inst - "abs(f!1(x!1))")
(("1" (assert)
(("1" (prop)
(("1" (inst + "x!1") nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "f!1")
(("2" (expand "bounded?")
(("2" (skosimp)
(("2" (expand "extend")
(("2" (expand "above_bounded")
(("2" (inst + "c!1")
(("2" (expand "upper_bound")
(("2" (skosimp)
(("2" (typepred "z!1")
(("2" (assert)
(("2" (skosimp)
(("2" (inst - "x!2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm nil)
(T formal-type-decl nil sup_norm nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals 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)
(empty? const-decl "bool" sets nil)
(extend const-decl "R" extend nil)
(nnreal type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(FALSE const-decl "bool" booleans nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(NOT const-decl "[bool -> bool]" booleans nil))
nil))
(sup_norm_TCC2 0
(sup_norm_TCC2-1 nil 3392429651
("" (skosimp*)
(("" (expand "extend")
((""
(typepred "sup[real]
(LAMBDA (t: real):
IF t >= 0 THEN EXISTS x: abs(f!1(x)) = t ELSE FALSE ENDIF)")
(("1"
(name-replace "SUP" "sup[real]
(LAMBDA (t: real):
IF t >= 0 THEN EXISTS x: abs(f!1(x)) = t ELSE FALSE ENDIF)")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (expand "upper_bound")
(("1" (inst - "abs(f!1(x!1))")
(("1" (assert) nil nil)
("2" (prop)
(("1" (inst + "x!1") nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "sup_norm_TCC1" ("f" "f!1"))
(("2" (split -1)
(("1" (expand "extend") (("1" (propax) nil nil)) nil)
("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(sup_norm_TCC1 subtype-tcc nil sup_norm nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(f!1 skolem-const-decl "bounded" sup_norm nil)
(x!1 skolem-const-decl "T" sup_norm nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(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)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(setof type-eq-decl nil defined_types nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(>= const-decl "bool" reals nil)
(T formal-type-decl nil sup_norm nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(bounded? const-decl "bool" sup_norm nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(FALSE const-decl "bool" booleans nil))
nil))
(sup_norm_eq_0 0
(sup_norm_eq_0-1 nil 3392433034
("" (skosimp)
((""
(lemma "extensionality_postulate"
("f" "f!1" "g" "const_fun[T, real](0)"))
(("" (replace -1 1 rl)
(("" (hide -1)
(("" (expand "const_fun")
(("" (expand "sup_norm")
(("" (case-replace "EXISTS x: TRUE")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(f!1(x_1)) = c}))")
(("1"
(name-replace "SUP"
"sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(f!1(x_1)) = c}))")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (expand "extend")
(("1" (expand "upper_bound")
(("1" (split 1)
(("1"
(flatten)
(("1"
(replace -1)
(("1"
(skosimp)
(("1"
(typepred "abs(f!1(x!1))")
(("1"
(hide -2 -3)
(("1"
(inst -3 "abs(f!1(x!1))")
(("1"
(hide-all-but (-1 -3 1))
(("1" (grind) nil nil))
nil)
("2"
(assert)
(("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(skosimp)
(("2"
(inst-cp - "x!1")
(("2"
(inst -3 "0")
(("1"
(inst -4 "0")
(("1"
(split -4)
(("1" (assert) nil nil)
("2" (propax) nil nil)
("3"
(skosimp)
(("3"
(typepred "z!1")
(("3"
(assert)
(("3"
(skosimp)
(("3"
(inst - "x!2")
(("3"
(replace -3)
(("3"
(expand "abs")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "x!1")
(("2"
(replace -2)
(("2"
(expand "abs")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2" (assert)
(("2" (skosimp) (("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(T formal-type-decl nil sup_norm nil)
(const_fun const-decl "[S -> T]" const_fun_def "structures/")
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm nil)
(bool nonempty-type-eq-decl nil booleans nil)
(extensionality_postulate formula-decl nil functions nil)
(sup_norm const-decl "nnreal" sup_norm nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(f!1 skolem-const-decl "bounded" sup_norm nil)
(x!1 skolem-const-decl "T" sup_norm nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(TRUE const-decl "bool" booleans nil))
shostak))
(sup_norm_neg 0
(sup_norm_neg-1 nil 3392433144
("" (skosimp)
(("" (expand "sup_norm")
(("" (case-replace "EXISTS x: TRUE")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(f!1(x_1)) = c}))")
(("1"
(name-replace "SUP" "sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(f!1(x_1)) = c}))")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c_1: nnreal | EXISTS (x_2: T): abs((-f!1)(x_2)) = c_1}))")
(("1"
(name-replace "SUPN"
"sup(extend[real, nnreal, bool, FALSE]
({c_1: nnreal | EXISTS (x_2: T): abs((-f!1)(x_2)) = c_1}))")
(("1" (expand "extend")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (inst -2 "SUP")
(("1" (split -2)
(("1" (inst -4 "SUPN")
(("1" (split -4)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3"
(hide -1 2)
(("3"
(expand "upper_bound")
(("3"
(skosimp)
(("3"
(typepred "z!1")
(("3"
(assert)
(("3"
(skosimp)
(("3"
(inst -3 "z!1")
(("3"
(inst + "x!1")
(("3"
(hide-all-but (-1 1))
(("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (expand "upper_bound")
(("3" (skosimp)
(("3"
(typepred "z!1")
(("3"
(assert)
(("3"
(skosimp)
(("3"
(inst -4 "z!1")
(("3"
(inst + "x!1")
(("3"
(hide-all-but (-1 1))
(("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2) (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((sup_norm const-decl "nnreal" sup_norm nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(pred type-eq-decl nil defined_types 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)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(bounded_opp application-judgement "bounded" sup_norm nil)
(z!1 skolem-const-decl
"{t | IF t >= 0 THEN EXISTS (x_1: T): abs(f!1(x_1)) = t ELSE FALSE ENDIF}"
sup_norm nil)
(f!1 skolem-const-decl "bounded" sup_norm nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(z!1 skolem-const-decl
"{t | IF t >= 0 THEN EXISTS (x_2: T): abs((-f!1)(x_2)) = t ELSE FALSE ENDIF}"
sup_norm nil)
(TRUE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sup_norm nil))
shostak))
(sup_norm_sum 0
(sup_norm_sum-1 nil 3392434044
("" (skosimp)
(("" (expand "sup_norm")
(("" (case-replace "EXISTS x: TRUE")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(f2!1(x_1)) = c}))")
(("1"
(name-replace "SUP2" "sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(f2!1(x_1)) = c}))")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c_1: nnreal | EXISTS (x_2: T): abs(f1!1(x_2)) = c_1}))")
(("1"
(name-replace "SUP1"
"sup(extend[real, nnreal, bool, FALSE]
({c_1: nnreal | EXISTS (x_2: T): abs(f1!1(x_2)) = c_1}))")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c_2: nnreal |
EXISTS (x_1: T): abs((f1!1 + f2!1)(x_1)) = c_2}))")
(("1"
(name-replace "SUP"
"sup(extend[real, nnreal, bool, FALSE]
({c_2: nnreal |
EXISTS (x_1: T): abs((f1!1 + f2!1)(x_1)) = c_2}))")
(("1" (expand "extend")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (hide -4 -6)
(("1" (inst -2 "SUP1 + SUP2")
(("1"
(split -2)
(("1" (propax) nil nil)
("2" (assert) nil nil)
("3"
(hide 2)
(("3"
(expand "upper_bound")
(("3"
(skosimp)
(("3"
(typepred "z!1")
(("3"
(assert)
(("3"
(skosimp)
(("3"
(expand "+" -1)
(("3"
(hide -3)
(("3"
(inst
-
"abs(f1!1(x!1))")
(("1"
(inst
-
"abs(f2!1(x!1))")
(("1"
(grind)
nil
nil)
("2"
(typepred
"abs(f2!1(x!1))")
(("2"
(assert)
(("2"
(inst
+
"x!1")
nil
nil))
nil))
nil))
nil)
("2"
(typepred
"abs(f1!1(x!1))")
(("2"
(assert)
(("2"
(inst + "x!1")
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" (replace 1 2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((sup_norm const-decl "nnreal" sup_norm nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(pred type-eq-decl nil defined_types 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)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(f1!1 skolem-const-decl "bounded" sup_norm nil)
(x!1 skolem-const-decl "T" sup_norm nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(f2!1 skolem-const-decl "bounded" sup_norm nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(TRUE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil sup_norm nil))
shostak))
(sup_norm_prop 0
(sup_norm_prop-1 nil 3394593866
("" (skosimp*)
(("" (typepred "sup_norm(f!1)")
(("" (expand "sup_norm")
(("" (case-replace "EXISTS x: TRUE")
(("1" (expand "extend")
(("1" (skolem - ("XX"))
(("1"
(typepred "sup(LAMBDA (t: real):
IF t >= 0 THEN EXISTS (x_1: T): abs(f!1(x_1)) = t
ELSE FALSE
ENDIF)")
(("1"
(name-replace "SUP" "sup(LAMBDA (t: real):
IF t >= 0 THEN EXISTS (x_1: T): abs(f!1(x_1)) = t
ELSE FALSE
ENDIF)")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1" (expand "upper_bound")
(("1" (split)
(("1" (skosimp)
(("1" (inst - "abs(f!1(x!1))")
(("1"
(assert)
(("1" (inst + "x!1") nil nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst -3 "c!1")
(("2"
(split -3)
(("1" (propax) nil nil)
("2" (assert) nil nil)
("3"
(skosimp)
(("3"
(typepred "z!1")
(("3"
(assert)
(("3"
(skosimp)
(("3"
(inst - "x!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (split)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (inst - "abs(f!1(XX))")
(("1" (expand "member")
(("1" (assert)
(("1"
(typepred "abs(f!1(XX))")
(("1"
(assert)
(("1" (inst + "XX") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "f!1")
(("2" (expand "bounded?")
(("2" (skosimp)
(("2" (expand "above_bounded")
(("2" (inst + "c!1")
(("2"
(expand "upper_bound")
(("2"
(skosimp)
(("2"
(typepred "z!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1)
(("2" (split)
(("1" (skosimp) (("1" (inst + "x!1") nil nil)) nil)
("2" (skosimp*) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sup_norm const-decl "nnreal" sup_norm nil)
(nnreal type-eq-decl nil real_types nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm nil)
(T formal-type-decl nil sup_norm nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(TRUE const-decl "bool" booleans nil)
(minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(f!1 skolem-const-decl "bounded" sup_norm nil)
(x!1 skolem-const-decl "T" sup_norm nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(pred type-eq-decl nil defined_types nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(setof type-eq-decl nil defined_types nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil))
shostak))
(sup_norm_convergent_TCC1 0
(sup_norm_convergent_TCC1-1 nil 3392434594
("" (expand "sup_norm_convergent?")
(("" (inst + "LAMBDA x: 0")
(("1" (expand "sup_norm_converges_to?")
(("1" (skosimp)
(("1" (inst + "0")
(("1" (skosimp)
(("1" (expand "-")
(("1" (expand "sup_norm")
(("1" (case-replace "EXISTS x: TRUE")
(("1"
(typepred "sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(0) = c}))")
(("1"
(name-replace "SUP"
"sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs(0) = c}))")
(("1" (expand "extend")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1"
(expand "upper_bound")
(("1"
(inst -2 "0")
(("1"
(split -2)
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3"
(skosimp)
(("3"
(typepred "z!1")
(("3"
(assert)
(("3"
(skosimp)
(("3"
(hide 2 -3)
(("3" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace 1 2) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "bounded?")
(("2" (inst + "0") (("2" (grind) nil nil)) nil)) nil))
nil))
nil)
((bounded? const-decl "bool" sup_norm 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)
(T formal-type-decl nil sup_norm nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(sup_norm const-decl "nnreal" sup_norm nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(setof type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(TRUE const-decl "bool" booleans nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sup_norm_converges_to? const-decl "bool" sup_norm nil)
(sup_norm_convergent? const-decl "bool" sup_norm nil))
nil))
(sup_norm_convergent_is_pointwise_convergent 0
(sup_norm_convergent_is_pointwise_convergent-1 nil 3392435448
("" (skolem + ("v"))
(("" (typepred "v")
(("" (expand "pointwise_convergent?")
(("" (expand "sup_norm_convergent?")
(("" (skosimp)
(("" (inst + "f!1")
(("" (expand "pointwise_convergence?")
(("" (skosimp)
(("" (expand "sup_norm_converges_to?")
(("" (rewrite "metric_convergence_def" *)
(("" (expand "metric_converges_to")
(("" (skosimp)
(("" (inst - "r!1")
(("" (skosimp)
((""
(inst + "n!1")
((""
(skosimp)
((""
(inst - "i!1")
((""
(assert)
((""
(expand "ball")
((""
(expand "sup_norm")
((""
(case-replace
"EXISTS x: TRUE")
(("1"
(typepred
"sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs((v(i!1) - f!1)(x_1)) = c}))")
(("1"
(name-replace
"SUP"
"sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs((v(i!1) - f!1)(x_1)) = c}))")
(("1"
(expand
"least_upper_bound")
(("1"
(expand "extend")
(("1"
(expand
"upper_bound")
(("1"
(flatten)
(("1"
(inst
-
"abs(f!1(x!1) - v(i!1)(x!1))")
(("1"
(assert)
nil
nil)
("2"
(prop)
(("1"
(inst
+
"x!1")
(("1"
(hide-all-but
1)
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sup_norm_convergent nonempty-type-eq-decl nil sup_norm nil)
(sup_norm_convergent? const-decl "bool" sup_norm nil)
(sequence type-eq-decl nil sequences nil)
(bounded nonempty-type-eq-decl nil sup_norm nil)
(bounded? const-decl "bool" sup_norm nil)
(T formal-type-decl nil sup_norm nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_convergence_def formula-decl nil metric_space
"metric_space/")
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(ball_is_metric_open application-judgement
"metric_open[real, (LAMBDA (x, y: real): abs(x - y))]"
convergence_aux "metric_space/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(sup_norm const-decl "nnreal" sup_norm nil)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound const-decl "bool" bound_defs "reals/")
(<= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(setof type-eq-decl nil defined_types nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(nnreal type-eq-decl nil real_types nil)
(FALSE const-decl "bool" booleans nil)
(extend const-decl "R" extend nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(upper_bound const-decl "bool" bound_defs "reals/")
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(f!1 skolem-const-decl "bounded" sup_norm nil)
(x!1 skolem-const-decl "T" sup_norm nil)
(v skolem-const-decl "sup_norm_convergent" sup_norm nil)
(i!1 skolem-const-decl "nat" sup_norm nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bounded_diff application-judgement "bounded" sup_norm nil)
(TRUE const-decl "bool" booleans nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(real_minus_real_is_real application-judgement "real" reals nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(metric_converges_to const-decl "bool" metric_space_def
"metric_space/")
(sup_norm_converges_to? const-decl "bool" sup_norm nil)
(pointwise_convergence? const-decl "bool" pointwise_convergence
nil)
(pointwise_convergent? const-decl "bool" pointwise_convergence
nil))
nil))
(sup_norm_converges_to_pointwise_convergence 0
(sup_norm_converges_to_pointwise_convergence-1 nil 3392527887
("" (skosimp)
(("" (expand "pointwise_convergence?")
(("" (skosimp)
(("" (expand "sup_norm_converges_to?")
(("" (rewrite "metric_convergence_def" *)
(("" (expand "metric_converges_to")
(("" (skosimp)
(("" (inst - "r!1")
(("" (skosimp)
(("" (inst + "n!1")
(("" (skosimp)
(("" (inst - "i!1")
(("" (assert)
(("" (expand "ball")
((""
(expand "sup_norm")
((""
(case-replace "EXISTS x: TRUE")
(("1"
(typepred
"sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs((u!1(i!1) - f!1)(x_1)) = c}))")
(("1"
(name-replace
"SUP"
"sup(extend[real, nnreal, bool, FALSE]
({c | EXISTS (x_1: T): abs((u!1(i!1) - f!1)(x_1)) = c}))")
(("1"
(expand "extend")
(("1"
(expand "least_upper_bound")
(("1"
(flatten)
(("1"
(expand "upper_bound")
(("1"
(inst
-
"abs(f!1(x!1) - u!1(i!1)(x!1))")
(("1" (assert) nil nil)
("2"
(typepred
"abs(f!1(x!1) - u!1(i!1)(x!1))")
(("2"
(assert)
(("2"
(inst + "x!1")
(("2"
(expand "-")
(("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pointwise_convergence? const-decl "bool" pointwise_convergence
nil)
(sup_norm_converges_to? const-decl "bool" sup_norm nil)
(metric_converges_to const-decl "bool" metric_space_def
"metric_space/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(TRUE const-decl "bool" booleans nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(minus_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)
(i!1 skolem-const-decl "nat" sup_norm nil)
(u!1 skolem-const-decl "sequence[bounded]" sup_norm nil)
(x!1 skolem-const-decl "T" sup_norm nil)
(f!1 skolem-const-decl "bounded" sup_norm nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.114 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
