|
(inverse_continuous_functions
(inverse_incr 0
(inverse_incr-1 nil 3324805607
("" (skosimp)
(("" (assert)
(("" (expand "bijective?")
(("" (expand "continuous?")
(("" (skosimp)
(("" (delete -1)
(("" (expand "continuous?")
(("" (expand "surjective?")
(("" (inst-cp -1 "x0!1")
(("" (skolem!)
(("" (case-replace "inverse(g!1)(x0!1) = x!1")
(("1" (delete -1)
(("1" (skolem!)
(("1"
(case "EXISTS (d : posreal) : FORALL (u : T1) : x0!1 - g!1(u) < d IMPLIES x!1 - u < epsilon!1")
(("1"
(case
"EXISTS (d : posreal) : FORALL (u : T1) : g!1(u) - x0!1 < d IMPLIES u - x!1 < epsilon!1")
(("1"
(skosimp*)
(("1"
(inst 1 "min(d!1, d!2)")
(("1"
(skosimp)
(("1"
(inst -3 "x!2")
(("1"
(skolem!)
(("1"
(case-replace
"inverse(g!1)(x!2) = x!3")
(("1"
(delete -1)
(("1"
(inst -1 "x!3")
(("1"
(inst -2 "x!3")
(("1"
(delete -5)
(("1"
(grind
:exclude
"min")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"bijective_inverse")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(delete -1 -2 2)
(("2"
(case
"EXISTS (v : T1) : x!1 + epsilon!1 = v")
(("1"
(skolem!)
(("1"
(expand "strict_increasing?")
(("1"
(inst-cp -3 "x!1" "v!1")
(("1"
(assert)
(("1"
(assert)
(("1"
(inst
1
"g!1(v!1) - x0!1")
(("1"
(skosimp)
(("1"
(inst
-4
"v!1"
"u!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 2 "1")
(("2"
(skosimp)
(("2"
(lemma "connected_domain")
(("2"
(inst
-1
"x!1"
"u!1"
"x!1 + epsilon!1")
(("2"
(assert)
(("2"
(inst
+
"epsilon!1 + x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(delete -1 2)
(("2"
(case
"EXISTS (v : T1) : x!1 - epsilon!1 = v")
(("1"
(skolem!)
(("1"
(expand "strict_increasing?")
(("1"
(inst-cp -3 "v!1" "x!1")
(("1"
(assert)
(("1"
(assert)
(("1"
(inst
1
"x0!1 - g!1(v!1)")
(("1"
(skosimp)
(("1"
(inst -4 "u!1" "v!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 2 "1")
(("2"
(skosimp)
(("2"
(lemma "connected_domain")
(("2"
(inst
-1
"u!1"
"x!1"
"x!1 - epsilon!1")
(("2"
(assert)
(("2"
(inst
+
"-epsilon!1 + x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "bijective_inverse")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous? const-decl "bool" continuous_functions nil)
(surjective? const-decl "bool" functions nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(connected_domain formula-decl nil inverse_continuous_functions
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(bijective_inverse formula-decl nil function_inverse nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(bool nonempty-type-eq-decl nil booleans nil)
(inverse const-decl "D" function_inverse nil)
(T1 formal-nonempty-subtype-decl nil inverse_continuous_functions
nil)
(T1_pred const-decl "[real -> boolean]"
inverse_continuous_functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T2 formal-nonempty-subtype-decl nil inverse_continuous_functions
nil)
(T2_pred const-decl "[real -> boolean]"
inverse_continuous_functions 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)
(continuous? const-decl "bool" continuous_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(bijective? const-decl "bool" functions nil))
nil))
(inverse_decr 0
(inverse_decr-1 nil 3324805607
("" (skosimp)
(("" (assert)
(("" (expand "bijective?")
(("" (expand "continuous?")
(("" (skosimp)
(("" (delete -1)
(("" (expand "continuous?")
(("" (expand "surjective?")
(("" (inst-cp -1 "x0!1")
(("" (skolem!)
(("" (skolem!)
(("" (case-replace "inverse(g!1)(x0!1) = x!1")
(("1" (delete -1)
(("1"
(case "EXISTS (d : posreal) : FORALL (u : T1) : x0!1 - g!1(u) < d IMPLIES u - x!1 < epsilon!1")
(("1"
(case
"EXISTS (d : posreal) : FORALL (u : T1) : g!1(u) - x0!1 < d IMPLIES x!1 - u < epsilon!1")
(("1"
(skosimp*)
(("1"
(inst 1 "min(d!1, d!2)")
(("1"
(skosimp)
(("1"
(inst -3 "x!2")
(("1"
(skolem!)
(("1"
(case-replace
"inverse(g!1)(x!2) = x!3")
(("1"
(delete -1)
(("1"
(inst -1 "x!3")
(("1"
(inst -2 "x!3")
(("1"
(grind
:exclude
("min"
"strict_decreasing?"))
nil
nil))
nil))
nil))
nil)
("2"
(rewrite
"bijective_inverse")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(delete -1 -2 2)
(("2"
(case
"EXISTS (v : T1) : x!1 - epsilon!1 = v")
(("1"
(skolem!)
(("1"
(expand "strict_decreasing?")
(("1"
(inst-cp -3 "v!1" "x!1")
(("1"
(assert)
(("1"
(assert)
(("1"
(inst
1
"g!1(v!1) - x0!1")
(("1"
(skosimp)
(("1"
(inst
-4
"u!1"
"v!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 2 "1")
(("2"
(skosimp)
(("2"
(lemma "connected_domain")
(("2"
(inst
-1
"u!1"
"x!1"
"x!1 - epsilon!1")
(("2"
(assert)
(("2"
(inst
+
"-epsilon!1 + x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(delete -1 2)
(("2"
(case
"EXISTS (v : T1) : x!1 + epsilon!1 = v")
(("1"
(skolem!)
(("1"
(expand "strict_decreasing?")
(("1"
(inst-cp -3 "x!1" "v!1")
(("1"
(assert)
(("1"
(assert)
(("1"
(inst
1
"x0!1 - g!1(v!1)")
(("1"
(skosimp)
(("1"
(inst -4 "v!1" "u!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 2 "1")
(("2"
(skosimp)
(("2"
(lemma "connected_domain")
(("2"
(inst
-1
"x!1"
"u!1"
"x!1 + epsilon!1")
(("2"
(assert)
(("2"
(inst
+
"epsilon!1 + x!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "bijective_inverse")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous? const-decl "bool" continuous_functions nil)
(surjective? const-decl "bool" functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T1_pred const-decl "[real -> boolean]"
inverse_continuous_functions nil)
(T1 formal-nonempty-subtype-decl nil inverse_continuous_functions
nil)
(inverse const-decl "D" function_inverse nil)
(bool nonempty-type-eq-decl nil booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(connected_domain formula-decl nil inverse_continuous_functions
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(strict_decreasing? const-decl "bool" real_fun_preds "reals/")
(bijective_inverse formula-decl nil function_inverse nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(T2 formal-nonempty-subtype-decl nil inverse_continuous_functions
nil)
(T2_pred const-decl "[real -> boolean]"
inverse_continuous_functions 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)
(continuous? const-decl "bool" continuous_functions nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(bijective? const-decl "bool" functions nil))
nil))
(inverse_continuous 0
(inverse_continuous-1 nil 3324805607
("" (skosimp)
(("" (assert)
(("" (expand "bijective?")
(("" (flatten)
(("" (use "inj_monotone[T1]")
(("1" (ground)
(("1" (rewrite "inverse_incr") nil)
("2" (rewrite "inverse_decr") nil)
("3" (expand "injective?") (("3" (propax) nil)))))
("2" (lemma "connected_domain")
(("2" (skosimp)
(("2" (inst -1 "x!1" "y!1" "z!1")
(("2" (assert) nil))))))))))))))))
nil)
((connected_domain formula-decl nil inverse_continuous_functions
nil)
(inverse_incr formula-decl nil inverse_continuous_functions nil)
(inverse_decr formula-decl nil inverse_continuous_functions nil)
(injective? const-decl "bool" functions nil)
(continuous? const-decl "bool" continuous_functions nil)
(T2_pred const-decl "[real -> boolean]"
inverse_continuous_functions nil)
(T2 formal-nonempty-subtype-decl nil inverse_continuous_functions
nil)
(T1 formal-nonempty-subtype-decl nil inverse_continuous_functions
nil)
(T1_pred const-decl "[real -> boolean]"
inverse_continuous_functions 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)
(inj_monotone formula-decl nil continuous_functions_props nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil))
nil)))
¤ Dauer der Verarbeitung: 0.40 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.
|
