Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: real_intervals_aux.prf Sprache: Lisp

Original von: PVS^©

(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.114 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.