|
(derivative_inverse
(deriv_domain1 0
(deriv_domain1-2 nil 3472399224
("" (lemma "connected_deriv_domain[T1]")
(("" (lemma "connected_domain1")
(("" (lemma not_one_element1) (("" (assert) nil nil)) nil)) nil))
nil)
((connected_domain1 formula-decl nil derivative_inverse nil)
(not_one_element1 formula-decl nil derivative_inverse nil)
(connected_deriv_domain formula-decl nil deriv_domain_def 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)
(T1_pred const-decl "[real -> boolean]" derivative_inverse nil)
(T1 formal-subtype-decl nil derivative_inverse nil))
nil)
(deriv_domain1-1 nil 3471606970
("" (skosimp*)
(("" (lemma "connected_domain1")
(("" (lemma "connected_deriv_domain[T1]")
(("1" (replace -2) (("1" (inst?) nil nil)) nil)
("2" (lemma "not_one_element1") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
nil shostak))
(deriv_domain2 0
(deriv_domain2-4 nil 3472399302
("" (lemma "connected_deriv_domain[T2]")
(("" (lemma "connected_domain2")
(("" (lemma "not_one_element2") (("" (assert) nil nil)) nil))
nil))
nil)
((connected_domain2 formula-decl nil derivative_inverse nil)
(not_one_element2 formula-decl nil derivative_inverse nil)
(connected_deriv_domain formula-decl nil deriv_domain_def 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)
(T2_pred const-decl "[real -> boolean]" derivative_inverse nil)
(T2 formal-subtype-decl nil derivative_inverse nil))
nil)
(deriv_domain2-3 nil 3472399245
("" (lemma "connected_domain2")
(("" (lemma "connected_deriv_domain[T2]")
(("" (replace -2)
(("" (lemma "not_one_element2")
(("" (replace -1)
(("" (hide -1)
(("" (expand "deriv_domain?") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_domain? const-decl "bool" deriv_domain_def nil)
(connected_deriv_domain formula-decl nil deriv_domain_def nil))
nil)
(deriv_domain2-2 nil 3471607027
("" (skosimp*)
(("" (lemma "connected_domain2")
(("" (lemma "connected_deriv_domain[T2]")
(("1" (replace -2) (("1" (inst?) nil nil)) nil)
("2" (lemma "not_one_element2") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
nil nil)
(deriv_domain2-1 nil 3471607020
(";;; Proof deriv_domain1-1 for formula derivative_inverse.deriv_domain1"
(skosimp*)
((";;; Proof deriv_domain1-1 for formula derivative_inverse.deriv_domain1"
(lemma "connected_domain2")
((";;; Proof deriv_domain1-1 for formula derivative_inverse.deriv_domain1"
(lemma "connected_deriv_domain[T2]")
(("1" (replace -2) (("1" (inst?) nil)))
("2" (lemma "not_one_element1") (("2" (propax) nil))))))))
";;; developed with shostak decision procedures")
nil nil))
(inverse_derivable_TCC1 0
(inverse_derivable_TCC1-1 nil 3262438616
("" (lemma "deriv_domain1") (("" (propax) nil nil)) nil)
((deriv_domain1 formula-decl nil derivative_inverse nil)) shostak))
(inverse_derivable_TCC2 0
(inverse_derivable_TCC2-1 nil 3262438682
("" (lemma "not_one_element1") (("" (propax) nil nil)) nil)
((not_one_element1 formula-decl nil derivative_inverse nil))
shostak))
(inverse_derivable_TCC3 0
(inverse_derivable_TCC3-1 nil 3262438701
("" (skosimp*)
(("" (lemma "deriv_domain2")
(("" (expand "deriv_domain?") (("" (inst?) nil nil)) nil)) nil))
nil)
((deriv_domain2 formula-decl nil derivative_inverse nil)) shostak))
(inverse_derivable_TCC4 0
(inverse_derivable_TCC4-1 nil 3262438892
("" (skolem 1 ("F" "G" "f"))
(("" (flatten)
(("" (lemma "not_one_element2")
(("" (expand "not_one_element?") (("" (propax) nil nil)) nil))
nil))
nil))
nil)
((not_one_element2 formula-decl nil derivative_inverse nil))
shostak))
(inverse_derivable 0
(inverse_derivable-7 "Alternative" 3477737338
("" (skolem 1 ("F" "G" "f" "Y0"))
(("" (flatten)
((""
(lemma "derivative_equivalence3"
("f" "F" "D" "f(G(Y0))" "x" "G(Y0)"))
(("1" (name "X0" "G(Y0)")
(("1" (replace -1)
(("1" (case "deriv(F, X0) = f(X0)")
(("1" (case "derivable?(F, X0)")
(("1" (assert)
(("1" (skolem! -4)
(("1" (flatten -4)
(("1"
(lemma "derivative_equivalence3"
("f" "G" "x" "Y0" "D" "1/f(G(Y0))"))
(("1" (flatten -1)
(("1" (hide -1)
(("1" (split -1)
(("1" (flatten -1) nil nil)
("2"
(hide 2)
(("2"
(case
"FORALL (y: T2): psi!1(G(y)) /= 0")
(("1"
(inst
+
"LAMBDA (y:T2): 1/psi!1(G(y))")
(("1"
(split 1)
(("1"
(lemma
"cv_in_domain"
("f"
"psi!1"
"x"
"X0"
"l"
"f(X0)"))
(("1"
(assert)
(("1"
(replace -5 1)
(("1"
(replace -1 1)
(("1"
(replace -5 1 rl)
(("1"
(case
"continuous?(LAMBDA (y: T2): 1 / psi!1(G(y)), Y0)")
(("1"
(rewrite
continuity_def)
nil
nil)
("2"
(hide 2)
(("2"
(lemma
"inv_continuous[T2]"
("g"
"LAMBDA (y: T2): psi!1(G(y))"
"x0"
"Y0"))
(("2"
(split -1)
(("1"
(expand
"/"
-1)
(("1"
(propax)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"inverse_continuous[T1,T2]"
("g" "F"))
(("1"
(replace
-10)
(("1"
(case
"inverse(F)=LAMBDA (y:T2): G(y)")
(("1"
(replace
-1)
(("1"
(case
"continuous?[T1](psi!1,X0)")
(("1"
(expand
"continuous?"
-3)
(("1"
(inst
-
"Y0")
(("1"
(lemma
"composition_cont[T2,T1]"
("f"
"G"
"g"
"psi!1"
"x0"
"Y0"))
(("1"
(expand
"o"
-1)
(("1"
(replace
-9
-1)
(("1"
(replace
-2)
(("1"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(hide-all-but
(-3
1))
(("2"
(expand
"continuous?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"convergence")
(("2"
(expand
"convergence")
(("2"
(hide
2)
(("2"
(hide
-1
-2)
(("2"
(lemma
"continuity_def2[T1]"
("f"
"psi!1"
"x0"
"X0"))
(("2"
(expand
"convergent?")
(("2"
(replace
-1
1)
(("2"
(inst
+
"f(X0)")
(("2"
(expand
"continuous?")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(hide-all-but
(-10
-12
1))
(("2"
(lemma
"extensionality"
("f"
"inverse(F)"
"g"
"(LAMBDA (y: T2): G(y))"))
(("2"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(lemma
"bijective_inverse"
("f"
"F"
"y"
"x!1"
"x"
"G(x!1)"))
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"x!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"derivable_cont_fun[T1]"
("f"
"F"))
(("2"
(assert)
nil
nil))
nil)
("3"
(inst
+
"Y0")
nil
nil)
("4"
(inst
+
"X0")
nil
nil)
("5"
(lemma
"connected_domain1")
(("5"
(expand
"connected?")
(("5"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skolem 1 ("Y1"))
(("2"
(inst -6 "G(Y1)")
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"Y1"))
(("2"
(replace -1)
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"Y0"))
(("2"
(replace -6 -8 rl)
(("2"
(replace -1 -8)
(("2"
(lemma
"div_cancel4"
("y"
"G(Y1) - G(Y0)"
"x"
"Y1 - Y0"
"n0z"
"psi!1(G(Y1))"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skolem 1 ("Y1"))
(("2"
(inst -5 "G(Y1)")
(("2"
(lemma
"comp_inverse_right_alt"
("f" "F" "g" "G" "r" "Y1"))
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"Y0"))
(("2"
(replace -2 -7)
(("2"
(replace -5 -7 rl)
(("2"
(replace -1)
(("2"
(copy -9)
(("2"
(expand
"bijective?"
-1)
(("2"
(flatten -1)
(("2"
(expand
"injective?")
(("2"
(case
"Y1 = Y0")
(("1"
(lemma
"cv_in_domain"
("f"
"psi!1"
"x"
"X0"
"l"
"f(X0)"))
(("1"
(replace
-9
*
rl)
(("1"
(replace
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(inst
-1
"G(Y1)"
"G(Y0)")
(("2"
(replace
-3
-1)
(("2"
(replace
-4
-1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (use "not_one_element2")
(("2" (expand "not_one_element?")
(("2" (propax) nil nil)) nil))
nil)
("3" (use "deriv_domain2") nil nil))
nil))
nil))
nil))
nil)
("2" (expand "derivable?" -4)
(("2" (inst -4 "X0") nil nil)) nil))
nil)
("2" (expand "deriv" -5)
(("2" (replace -5 1 rl) (("2" (assert) nil nil)) nil))
nil)
("3" (lemma "not_one_element1") (("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (use "not_one_element1")
(("2" (expand "not_one_element?") (("2" (propax) nil nil))
nil))
nil)
("3" (use "deriv_domain1") nil nil))
nil))
nil))
nil)
((deriv_domain1 formula-decl nil derivative_inverse nil)
(not_one_element1 formula-decl nil derivative_inverse nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(deriv const-decl "real" derivatives_def nil)
(derivable? const-decl "bool" derivatives_def nil)
(derivable? const-decl "bool" derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(deriv_domain2 formula-decl nil derivative_inverse nil)
(not_one_element2 formula-decl nil derivative_inverse nil)
(continuous? const-decl "bool" continuous_functions nil)
(continuity_def formula-decl nil continuous_functions nil)
(inv_continuous formula-decl nil continuous_functions nil)
(connected_domain1 formula-decl nil derivative_inverse nil)
(connected? const-decl "bool" deriv_domain_def nil)
(derivable_cont_fun formula-decl nil derivatives nil)
(extensionality formula-decl nil functions nil)
(bijective_inverse formula-decl nil function_inverse nil)
(bijective? const-decl "bool" functions nil)
(inverse? const-decl "bool" function_inverse_def nil)
(comp_inverse_right_alt formula-decl nil function_inverse_def nil)
(convergence const-decl "bool" lim_of_functions nil)
(continuity_def2 formula-decl nil continuous_functions nil)
(convergent? const-decl "bool" lim_of_functions nil)
(convergence const-decl "bool" convergence_functions nil)
(composition_cont formula-decl nil composition_continuous nil)
(O const-decl "T3" function_props nil)
(inverse const-decl "D" function_inverse nil)
(TRUE const-decl "bool" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(continuous? const-decl "bool" continuous_functions nil)
(inverse_continuous formula-decl nil inverse_continuous_functions
nil)
(/ const-decl "[T -> real]" real_fun_ops "reals/")
(cv_in_domain formula-decl nil lim_of_functions nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(div_cancel4 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(G skolem-const-decl "[T2 -> T1]" derivative_inverse nil)
(psi!1 skolem-const-decl "[T1 -> real]" derivative_inverse nil)
(injective? const-decl "bool" functions nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(deriv const-decl "[T -> real]" derivatives nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(not_one_element? const-decl "bool" deriv_domain_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def nil)
(derivative_equivalence3 formula-decl nil derivatives_alt nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(T2_pred const-decl "[real -> boolean]" derivative_inverse nil)
(T2 formal-subtype-decl nil derivative_inverse 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)
(T1_pred const-decl "[real -> boolean]" derivative_inverse nil)
(T1 formal-subtype-decl nil derivative_inverse nil))
nil)
(inverse_derivable-6 "Alternative" 3473181730
("" (skolem 1 ("F" "G" "f" "Y0"))
(("" (flatten)
((""
(lemma "derivative_equivalence3"
("f" "F" "D" "f(G(Y0))" "x" "G(Y0)"))
(("1" (name "X0" "G(Y0)")
(("1" (replace -1)
(("1" (case "deriv(F, X0) = f(X0)")
(("1" (case "derivable?(F, X0)")
(("1" (assert)
(("1" (skolem! -4)
(("1" (flatten -4)
(("1"
(lemma "derivative_equivalence3"
("f" "G" "x" "Y0" "D" "1/f(G(Y0))"))
(("1" (flatten -1)
(("1" (hide -1)
(("1" (split -1)
(("1" (flatten -1) nil nil)
("2"
(hide 2)
(("2"
(case
"FORALL (y: T2): psi!1(G(y)) /= 0")
(("1"
(inst
+
"LAMBDA (y:T2): 1/psi!1(G(y))")
(("1"
(split 1)
(("1"
(lemma
"cv_in_domain"
("f"
"psi!1"
"x"
"X0"
"l"
"f(X0)"))
(("1"
(assert)
(("1"
(replace -5 1)
(("1"
(replace -1 1)
(("1"
(replace -5 1 rl)
(("1"
(case
"continuous?(LAMBDA (y: T2): 1 / psi!1(G(y)), Y0)")
(("1"
(rewrite
continuity_def)
nil
nil)
("2"
(hide 2)
(("2"
(lemma
"inv_continuous[T2]"
("g"
"LAMBDA (y: T2): psi!1(G(y))"
"x0"
"Y0"))
(("2"
(split -1)
(("1"
(expand
"/"
-1)
(("1"
(propax)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"inverse_continuous[T1,T2]"
("g" "F"))
(("1"
(replace
-10)
(("1"
(case
"inverse(F)=LAMBDA (y:T2): G(y)")
(("1"
(replace
-1)
(("1"
(case
"continuous?[T1](psi!1,X0)")
(("1"
(expand
"continuous?"
-3)
(("1"
(inst
-
"Y0")
(("1"
(lemma
"composition_cont[T2,T1]"
("f"
"G"
"g"
"psi!1"
"x0"
"Y0"))
(("1"
(expand
"o"
-1)
(("1"
(replace
-9
-1)
(("1"
(replace
-2)
(("1"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(hide-all-but
(-3
1))
(("2"
(expand
"continuous?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"convergence")
(("2"
(expand
"convergence")
(("2"
(hide
2)
(("2"
(hide
-1
-2)
(("2"
(lemma
"continuity_def2[T1]"
("f"
"psi!1"
"x0"
"X0"))
(("2"
(expand
"convergent?")
(("2"
(replace
-1
1)
(("2"
(inst
+
"f(X0)")
(("2"
(expand
"continuous?")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(hide-all-but
(-10
-12
1))
(("2"
(lemma
"extensionality"
("f"
"inverse(F)"
"g"
"(LAMBDA (y: T2): G(y))"))
(("2"
(split
-1)
(("1"
(propax)
nil
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(lemma
"bijective_inverse"
("f"
"F"
"y"
"x!1"
"x"
"G(x!1)"))
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"x!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"derivable_cont_fun[T1]"
("f"
"F"))
(("2"
(assert)
nil
nil))
nil)
("3"
(inst
+
"Y0")
nil
nil)
("4"
(inst
+
"X0")
nil
nil)
("5"
(lemma
"connected_domain1")
(("5"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skolem 1 ("Y1"))
(("2"
(inst -6 "G(Y1)")
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"Y1"))
(("2"
(replace -1)
(("2"
(lemma
"comp_inverse_right_alt"
("f"
"F"
"g"
"G"
"r"
"Y0"))
(("2"
(replace -6 -8 rl)
(("2"
(replace -1 -8)
(("2"
(lemma
"div_cancel4"
("y"
"G(Y1) - G(Y0)"
"x"
"Y1 - Y0"
"n0z"
"psi!1(G(Y1))"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.107 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.
|
