Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: inverse_continuous_functions.prf Sprache: Lisp

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.33 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.