Quellcode-Bibliothek composition_continuous.prf

(composition_continuous
 (composition_continuous 0
  (composition_continuous-1 nil 3401127653
   ("" (skosimp)
    (("" (expand "metric_continuous?")
      (("" (skosimp)
        (("" (expand "metric_continuous_at?")
          (("" (expand "ball")
            (("" (expand "member")
              (("" (skosimp)
                (("" (inst - "x!1")
                  (("" (inst -2 "g!1(x!1)")
                    (("" (inst -2 "epsilon!1")
                      (("" (skosimp)
                        (("" (inst - "delta!1")
                          (("" (skosimp)
                            (("" (inst + "delta!2")
                              ((""
                                (skosimp)
                                ((""
                                  (inst - "x!2")
                                  ((""
                                    (inst - "g!1(x!2)")
                                    ((""
                                      (expand "o ")
                                      (("" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((metric_continuous? const-decl "bool" metric_continuity nil)
    (metric_continuous_at? const-decl "bool" metric_continuity nil)
    (member const-decl "bool" sets nil)
    (T1 formal-type-decl nil composition_continuous 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)
    (O const-decl "T3" function_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T2 formal-type-decl nil composition_continuous nil)
    (ball const-decl "set[T]" metric_space_def nil))
   shostak)))