Quelle  composition_continuous.prf   Sprache: unbekannt

(composition_continuous
 (composition_cont 0
  (composition_cont-1 nil 3473169490
   ("" (skosimp*)
    (("" (expand "continuous?")
      (("" (skosimp*)
        (("" (inst -2 "epsilon!1")
          (("" (expand "o ")
            (("" (skosimp*)
              (("" (inst - "delta!1")
                (("" (skolem!)
                  (("" (inst 1 "delta!2")
                    (("" (skosimp)
                      (("" (inst - "x!1")
                        (("" (assert)
                          (("" (inst - "f!1(x!1)")
                            (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_minus_real_is_real application-judgement "real" reals nil)
    (continuous? const-decl "bool" continuous_functions 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T2_pred const-decl "[real -> boolean]" composition_continuous nil)
    (T2 formal-subtype-decl nil composition_continuous nil)
    (T1_pred const-decl "[real -> boolean]" composition_continuous nil)
    (T1 formal-subtype-decl nil composition_continuous nil)
    (O const-decl "T3" function_props nil))
   nil))
 (composition_cont_set 0
  (composition_cont_set-1 nil 3473169490
   ("" (skosimp*)
    (("" (rewrite "continuous_on_def")
      (("" (rewrite "continuous_on_def")
        (("" (rewrite "continuous_on_def")
          (("" (skosimp*)
            (("" (grind :exclude ("convergence") :if-match nil)
              (("" (inst?)
                (("" (assert)
                  (("" (inst?)
                    (("1" (grind :exclude ("abs" "adh") :if-match nil)
                      (("1" (inst? -6)
                        (("1" (skolem!)
                          (("1" (inst -4 "delta!1")
                            (("1" (skolem!)
                              (("1"
                                (inst 1 "delta!2")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (inst -4 "x!1")
                                    (("1"
                                      (inst -6 "f!1(x!1)")
                                      (("1"
                                        (assert)
                                        (("1" (inst?) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert)
                      (("2" (inst?)
                        (("2" (hide-all-but 1)
                          (("2" (typepred "y!1")
                            (("2" (expand "restrict")
                              (("2" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
 (composition_cont_fun 0
  (composition_cont_fun-1 nil 3473169490
   ("" (grind :defs nil :rewrites ("continuous_def2[T1]"))
    (("" (rewrite "composition_cont_set")
      (("1" (rewrite "continuity_subset2[T2]")
        (("1" (delete -1 -2 2 3) (("1" (grind) nil)))))
       ("2" (rewrite "subset_reflexive") nil))))
    nil)
   ((subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (composition_cont_set formula-decl nil composition_continuous nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets nil)
    (subset? const-decl "bool" sets nil)
    (T2_pred const-decl "[real -> boolean]" composition_continuous nil)
    (T2 formal-subtype-decl nil composition_continuous nil)
    (continuity_subset2 formula-decl nil continuous_functions nil)
    (restrict const-decl "R" restrict nil)
    (Im const-decl "setof[real]" real_fun_props "reals/")
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (continuous_def2 formula-decl nil continuous_functions 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]" composition_continuous nil)
    (T1 formal-subtype-decl nil composition_continuous nil))
   nil)))