(metric_spaces_def
 (metric_restriction 0
  (metric_restriction-1 nil 3293720022 3293720104
   ("" (skosimp*)
    (("" (expand "metric?")
      (("" (expand "metric_zero?")
        (("" (expand "metric_symmetric?")
          (("" (expand "metric_triangle?")
            (("" (flatten)
              (("" (expand "metric_space?")
                (("" (split)
                  (("1" (expand "space_zero?")
                    (("1" (skosimp*)
                      (("1" (inst -1 "x!1" "y!1") nil nil)) nil))
                    nil)
                   ("2" (expand "space_symmetric?")
                    (("2" (skosimp*)
                      (("2" (inst -2 "x!1" "y!1") nil nil)) nil))
                    nil)
                   ("3" (expand "space_triangle?")
                    (("3" (skosimp*)
                      (("3" (inst - "x!1" "y!1" "z!1") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((metric? const-decl "bool" metric_spaces_def nil)
    (metric_symmetric? const-decl "bool" metric_spaces_def nil)
    (T formal-nonempty-type-decl nil metric_spaces_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (space_symmetric? const-decl "bool" metric_spaces_def nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (metric_triangle? const-decl "bool" metric_spaces_def nil)
    (metric_zero? const-decl "bool" metric_spaces_def nil))
   82989 2170 t shostak)))