| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 217 kB |
|
Quelle derivative_inverse.prfSprache: Lisp |
|||||||||||||||
|
(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" (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") 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 "deriv_domain1") (("3" (expand "deriv_domain?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "not_one_element1") nil nil) ("3" (use "deriv_domain1") nil nil)) nil)) nil)) nil) ((deriv const-decl "real" derivatives_def nil) (derivable? const-decl "bool" derivatives_def nil) (derivable? const-decl "bool" derivatives nil) (continuity_def formula-decl nil continuous_functions nil) (inv_continuous formula-decl nil continuous_functions nil) (derivable_cont_fun formula-decl nil derivatives 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) (inverse_continuous formula-decl nil inverse_continuous_functions nil) (cv_in_domain formula-decl nil lim_of_functions nil) (deriv const-decl "[T -> real]" derivatives nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (derivative_equivalence3 formula-decl nil derivatives_alt nil)) nil) (inverse_derivable-5 "Alternative" 3473181482 (";;; Proof inverse_derivable-4 for formula derivative_inverse.inverse_derivable" (skolem 1 ("F" "G" "f" "Y0")) ((";;; Proof inverse_derivable-4 for formula derivative_inverse.inverse_derivable" (flatten) ((";;; Proof inverse_derivable-4 for formula derivative_inverse.inverse_derivable" (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) ("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) ("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))) ("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) ("2" (hide-all-but (-3 1)) (("2" (expand "continuous?") (("2" (propax) nil))))))))))))))))))) ("2" (expand "convergence") (("2" (expand "convergence") (("2" (hide 2) (("2" (hide -1 -2) (("2" (lemma "continuity_def3[T1]" ("f" "psi!1" "x0" "X0")) (("2" (expand "convergent?") (("2" (replace -1 1) (("2" (inst + "f(X0)") (("2" (expand "continuous?") (("2" (assert) 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) ("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))))))))))))))))))))) ("2" (lemma "derivable_cont_fun[T1]" ("f" "F")) (("2" (assert) nil))) ("3" (inst + "Y0") nil) ("4" (inst + "X0") nil) ("5" (lemma "connected_domain1") (("5" (propax) nil))))))))))))) ("3" (propax) 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))))))))))))))))))))) ("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))))))) ("2" (inst -1 "G(Y1)" "G(Y0)") (("2" (replace -3 -1) (("2" (replace -4 -1) (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))) ("2" (use "not_one_element2") nil) ("3" (use "deriv_domain2") nil))))))))) ("2" (expand "derivable?" -4) (("2" (inst -4 "X0") nil))))) ("2" (expand "deriv" -5) (("2" (replace -5 1 rl) (("2" (assert) nil))))) ("3" (lemma "deriv_domain1") (("3" (expand "deriv_domain?") (("3" (propax) nil))))))))))) ("2" (use "not_one_element1") nil) ("3" (use "deriv_domain1") nil)))))) ";;; developed with shostak decision procedures") nil nil) (inverse_derivable-4 "Alternative" 3473181409 ("" (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" (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") 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 "deriv_domain1") (("3" (expand "deriv_domain?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "not_one_element1") nil nil) ("3" (use "deriv_domain1") nil nil)) nil)) nil)) nil) ((derivative_equivalence3 formula-decl nil derivatives_alt nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (deriv const-decl "[T -> real]" derivatives nil) (cv_in_domain formula-decl nil lim_of_functions nil) (inverse_continuous formula-decl nil inverse_continuous_functions nil) (composition_cont formula-decl nil composition_continuous nil) (convergence const-decl "bool" convergence_functions nil) (convergent? const-decl "bool" lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil) (convergence const-decl "bool" lim_of_functions nil) (derivable_cont_fun formula-decl nil derivatives nil) (inv_continuous formula-decl nil continuous_functions nil) (continuity_def formula-decl nil continuous_functions nil) (derivable? const-decl "bool" derivatives nil) (derivable? const-decl "bool" derivatives_def nil) (deriv const-decl "real" derivatives_def nil)) nil) (inverse_derivable-3 "Alternative" 3374401124 ("" (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" (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") 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 "deriv_domain1") (("3" (expand "deriv_domain?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "not_one_element1") nil nil) ("3" (use "deriv_domain1") nil nil)) nil)) nil)) nil) ((derivative_equivalence3 formula-decl nil derivatives_alt nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (deriv const-decl "[T -> real]" derivatives nil) (cv_in_domain formula-decl nil lim_of_functions nil) (inverse_continuous formula-decl nil inverse_continuous_functions nil) (composition_cont formula-decl nil composition_continuous nil) (convergence const-decl "bool" convergence_functions nil) (convergent? const-decl "bool" lim_of_functions nil) (continuity_def2 formula-decl nil continuous_functions nil) (convergence const-decl "bool" lim_of_functions nil) (derivable_cont_fun formula-decl nil derivatives nil) (inv_continuous formula-decl nil continuous_functions nil) (continuity_def formula-decl nil continuous_functions nil) (derivable? const-decl "bool" derivatives nil) (derivable? const-decl "bool" derivatives_def nil) (deriv const-decl "real" derivatives_def nil)) nil) (inverse_derivable-2 "Alternative" 3262541591 ("" (skolem 1 ("F" "G" "f" "Y0")) (("" (flatten) (("" (lemma "derivative_equivalence3" ("f" "F" "D" "f(G(Y0))" "x" "G(Y0)")) (("" (name "X0" "G(Y0)") (("" (replace -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" (expand "continuous?" -1) (("1" (propax) nil 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" (expand "convergence") (("2" (expand "convergence") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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)") 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)) 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)) 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" (expand "derivable?" -3) (("3" (inst -3 "X0") (("3" (lemma "not_one_element1") (("3" (propax) nil nil)) nil)) nil)) nil) ("4" (lemma "deriv_domain1") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv const-decl "[T -> real]" derivatives nil) (cv_in_domain formula-decl nil lim_of_functions nil) (inverse_continuous formula-decl nil inverse_continuous_functions nil) (convergence const-decl "bool" lim_of_functions nil) (convergence const-decl "bool" convergence_functions nil) (composition_cont formula-decl nil composition_continuous nil) (continuity_def2 formula-decl nil continuous_functions nil) (derivable_cont_fun formula-decl nil derivatives nil) (inv_continuous formula-decl nil continuous_functions nil) (deriv const-decl "real" derivatives_def nil)) shostak) (inverse_derivable-1 nil 3262452070 ("" (skolem 1 ("F" "G" "f" "y")) (("" (flatten) (("" (expand "derivable?" 1) (("" (expand "convergent?" 1) (("" (inst + "1/(f(G(y)))") (("" (expand "convergence") (("" (expand "convergence") (("" (split 1) (("1" (expand "adh") (("1" (skosimp*) (("1" (typepred "y") (("1" (lemma "not_one_element2" ("x" "y")) (("1" (skolem! -1) (("1" (lemma "trich_lt" ("x" "y!1" "y" "y")) (("1" (split -1) (("1" (lemma "deriv_domain2" ("x" "y!1" "y" "y")) (("1" (case "y!1 < y-e!1/2") (("1" (inst + "-e!1/2") (("1" (expand "fullset") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "A") (("2" (inst - "y-e!1/2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (inst + "y!1-y") (("1" (expand "fullset") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "A" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (lemma "deriv_domain2" ("x" "y" "y" "y!1")) (("3" (case "y+e!1/2 < y!1") (("1" (inst + "e!1/2") (("1" (expand "fullset") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "A") (("2" (inst - "y+e!1/2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "fullset") (("2" (expand "abs") (("2" (inst + "y!1-y") (("1" (assert) nil nil) ("2" (expand "A") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skolem 1 ("ep")) (("2" (expand "fullset") (("2" (expand "NQ") (("2" (copy -2) (("2" (expand "bijective?" -1) (("2" (flatten -1) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (inverse_derivable_fun 0 (inverse_derivable_fun-1 nil 3262491010 ("" (skolem 1 ("F" "G" "f")) (("" (flatten) (("" (lemma "inverse_derivable" ("F" "F" "G" "G" "f" "f")) (("" (expand "derivable?" 1) (("" (skolem 1 ("x")) (("" (inst - "x") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((derivable? const-decl "bool" derivatives nil) (inverse_derivable formula-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) (T2_pred const-decl "[real -> boolean]" derivative_inverse nil) (T2 formal-subtype-decl nil derivative_inverse nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) shostak)) (deriv_inverse_fun_TCC1 0 (deriv_inverse_fun_TCC1-1 nil 3262438973 ("" (skosimp*) (("" (lemma "inverse_derivable") (("" (assert) (("" (expand "derivable?" 1) (("" (skosimp*) (("" (inst - "F!1" "G!1" "f!1" "x!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inverse_derivable formula-decl nil derivative_inverse nil) (derivable? const-decl "bool" derivatives 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) (T2_pred const-decl "[real -> boolean]" derivative_inverse nil) (T2 formal-subtype-decl nil derivative_inverse nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil)) shostak)) (deriv_inverse_fun 0 (deriv_inverse_fun-2 nil 3477737541 ("" (skolem 1 ("F" "G" "f")) (("" (flatten) (("" (assert) (("" (lemma "identity_derivable_fun[T2]") (("1" (lemma "deriv_id_fun[T2]") (("1" (expand "I") (("1" (lemma "composition_derivable_fun[T2,T1]" ("g" "F" "f" "G")) (("1" (assert) (("1" (lemma "deriv_comp_fun[T2,T1]") (("1" (inst - "G" "F") (("1" (lemma "extensionality" ("f" "deriv[T2](G)" "g" "(LAMBDA (x: T2): 1 / f(G(x)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "extensionality" ("f" "F o G" "g" "LAMBDA (x: T2): x")) (("2" (split -1) (("1" (expand "o") (("1" (replace -1) (("1" (replace -4 -2) (("1" (hide -1 -3 -4 -5) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: T2): 1)" "g" "(LAMBDA (x: T2): deriv(F)(G(x))) * deriv(G)")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (inst - "x") (("1" (expand "*" -1) (("1" (lemma "div_cancel3" ("x" "1" "n0z" "f(G(x))" "y" "deriv[T2](G)(x)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o" 1) (("2" (skolem 1 ("y")) (("2" (typepred "y") (("2" (typepred "G(y)") (("2" (lemma "comp_inverse_right_surj_alt" ("f" "F" "g" "G" "r" "y")) (("1" (propax) nil nil) ("2" (expand "bijective?") (("2" (flatten -9) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element1") (("2" (expand "not_one_element?") (("2" (propax) nil nil)) nil)) nil) ("3" (lemma "deriv_domain1") (("3" (propax) nil nil)) nil) ("4" (lemma "not_one_element2") (("4" (expand "not_one_element?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element2") (("2" (propax) nil nil)) nil) ("3" (lemma "deriv_domain2") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((T2 formal-subtype-decl nil derivative_inverse nil) (T2_pred const-decl "[real -> boolean]" derivative_inverse 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) (identity_derivable_fun formula-decl nil derivatives nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (not_one_element? const-decl "bool" deriv_domain_def nil) (bool nonempty-type-eq-decl nil booleans nil) (I const-decl "(bijective?[T, T])" identity nil) (deriv_domain1 formula-decl nil derivative_inverse nil) (not_one_element1 formula-decl nil derivative_inverse nil) (derivable? const-decl "bool" derivatives nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (extensionality_postulate formula-decl nil functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (comp_inverse_right_surj_alt formula-decl nil function_inverse_def nil) (surjective? const-decl "bool" functions nil) (inverse? const-decl "bool" function_inverse_def nil) (bijective? const-decl "bool" functions nil) (O const-decl "T3" function_props nil) (extensionality formula-decl nil functions nil) (deriv_fun type-eq-decl nil derivatives nil) (deriv const-decl "[T -> real]" derivatives nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (deriv_comp_fun formula-decl nil chain_rule nil) (T1 formal-subtype-decl nil derivative_inverse nil) (T1_pred const-decl "[real -> boolean]" derivative_inverse nil) (composition_derivable_fun formula-decl nil chain_rule nil) (deriv_id_fun formula-decl nil derivatives nil) (not_one_element2 formula-decl nil derivative_inverse nil) (deriv_domain2 formula-decl nil derivative_inverse nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (deriv_inverse_fun-1 nil 3262449269 ("" (skolem 1 ("F" "G" "f")) (("" (flatten) (("" (assert) (("" (lemma "identity_derivable_fun[T2]") (("1" (lemma "deriv_id_fun[T2]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "composition_derivable_fun[T2,T1]" ("g" "F" "f" "G")) (("1" (assert) (("1" (lemma "deriv_comp_fun[T2,T1]") (("1" (inst - "G" "F") (("1" (lemma "extensionality" ("f" "deriv[T2](G)" "g" "(LAMBDA (x: T2): 1 / f(G(x)))")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skolem 1 ("x")) (("2" (lemma "extensionality" ("f" "F o G" "g" "LAMBDA (x: T2): x")) (("2" (split -1) (("1" (expand "o") (("1" (replace -1) (("1" (replace -4 -2) (("1" (hide -1 -3 -4 -5) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: T2): 1)" "g" "(LAMBDA (x: T2): deriv(F)(G(x))) * deriv(G)")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (inst - "x") (("1" (expand "*" -1) (("1" (lemma "div_cancel3" ("x" "1" "n0z" "f(G(x))" "y" "deriv[T2](G)(x)")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "o" 1) (("2" (skolem 1 ("y")) (("2" (typepred "y") (("2" (typepred "G(y)") (("2" (lemma "comp_inverse_right_surj_alt" ("f" "F" "g" "G" "r" "y")) (("1" (propax) nil nil) ("2" (expand "bijective?") (("2" (flatten -9) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "inverse_derivable_fun" ("F" "F" "G" "G")) (("2" (assert) (("2" (lemma "inverse_derivable_fun" ("F" "F" "G" "G" "f" "f")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "inverse_derivable_fun" ("F" "F" "G" "G")) (("2" (assert) (("2" (lemma "inverse_derivable_fun" ("F" "F" "G" "G" "f" "f")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element1") (("2" (propax) nil nil)) nil) ("3" (lemma "deriv_domain1") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element2") (("2" (propax) nil nil)) nil) ("3" (lemma "deriv_domain2") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((identity_derivable_fun formula-decl nil derivatives nil) (deriv_domain? const-decl "bool" deriv_domain_def nil) (composition_derivable_fun formula-decl nil chain_rule nil) (deriv_comp_fun formula-decl nil chain_rule nil) (deriv const-decl "[T -> real]" derivatives nil) (deriv_fun type-eq-decl nil derivatives nil) (derivable? const-decl "bool" derivatives nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_id_fun formula-decl nil derivatives nil)) shostak)) (deriv_inverse 0 (deriv_inverse-1 nil 3298214172 ("" (skosimp*) (("" (lemma "inverse_derivable_fun") (("" (inst - "F!1" "G!1" "f!1") (("" (lemma "deriv_inverse_fun") (("" (inst - "F!1" "G!1" "f!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((inverse_derivable_fun formula-decl nil derivative_inverse nil) (deriv_inverse_fun formula-decl nil derivative_inverse nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (T2 formal-subtype-decl nil derivative_inverse nil) (T2_pred const-decl "[real -> boolean]" derivative_inverse nil) (T1 formal-subtype-decl nil derivative_inverse nil) (T1_pred const-decl "[real -> boolean]" derivative_inverse 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)) shostak)))
¤ Dauer der Verarbeitung: 0.188 Sekunden (vorverarbeitet am 2026-05-03) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26