Impressum metric_continuity.prf

(metric_continuity
 (metric_continuous_at_def 0
  (metric_continuous_at_def-1 nil 3359022978
   ("" (skosimp)
    (("" (expand "metric_continuous_at?")
      (("" (expand "continuous_at?")
        (("" (expand "neighbourhood?")
          (("" (expand "interior_point?")
            (("" (split)
              (("1" (skosimp*)
                (("1" (expand "member")
                  (("1" (inst - "ball(f!1(x0!1), epsilon!1)")
                    (("1" (split -1)
                      (("1" (skosimp)
                        (("1" (typepred "U!1")
                          (("1" (lemma "metric_open_def" ("S" "U!1"))
                            (("1" (assert)
                              (("1"
                                (expand "metric_open?")
                                (("1"
                                  (inst - "x0!1")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (skosimp)
                                      (("1"
                                        (inst + "r!1")
                                        (("1"
                                          (skosimp)
                                          (("1"
                                            (expand "subset?")
                                            (("1"
                                              (inst - "x!1")
                                              (("1"
                                                (inst - "x!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (expand
                                                     "inverse_image")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide 2)
                        (("2"
                          (lemma "metric_open_ball"
                           ("x" "f!1(x0!1)" "r" "epsilon!1"))
                          (("2" (rewrite "metric_open_def")
                            (("2" (inst + "ball(f!1(x0!1), epsilon!1)")
                              (("2"
                                (lemma
                                 "ball_centre"
                                 ("x" "f!1(x0!1)" "r" "epsilon!1"))
                                (("2"
                                  (assert)
                                  (("2"
                                    (rewrite "subset_reflexive")
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (typepred "U!2")
                  (("2" (lemma "metric_open_def[T2,d2]" ("S" "U!2"))
                    (("2" (assert)
                      (("2" (expand "metric_open?")
                        (("2" (inst - "f!1(x0!1)")
                          (("2" (assert)
                            (("2" (skosimp)
                              (("2"
                                (inst - "r!1")
                                (("2"
                                  (skosimp)
                                  (("2"
                                    (inst + "ball(x0!1, delta!1)")
                                    (("1"
                                      (lemma
                                       "ball_centre"
                                       ("x" "x0!1" "r" "delta!1"))
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "subset?")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (inst -4 "x!1")
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (expand
                                                     "inverse_image")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (inst
                                                         -2
                                                         "f!1(x!1)")
                                                        (("1"
                                                          (inst
                                                           -
                                                           "f!1(x!1)")
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (rewrite
                                         "metric_open_def"
                                         1
                                         :dir
                                         rl)
                                        (("2"
                                          (rewrite "metric_open_ball")
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((metric_continuous_at? const-decl "bool" metric_continuity nil)
    (neighbourhood? const-decl "bool" topology "topology/")
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (d1 formal-const-decl "metric[T1]" metric_continuity nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     nil)
    (open? const-decl "bool" topology "topology/")
    (open nonempty-type-eq-decl nil topology "topology/")
    (ball_is_metric_open application-judgement "metric_open"
     metric_continuity nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (ball_is_metric_open application-judgement "metric_open"
     metric_continuity nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (subset? const-decl "bool" sets nil)
    (metric_open? const-decl "bool" metric_space_def nil)
    (metric_open_def formula-decl nil metric_space nil)
    (metric_open_ball formula-decl nil metric_space nil)
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (ball_centre formula-decl nil metric_space nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (ball const-decl "set[T]" metric_space_def nil)
    (d2 formal-const-decl "metric[T2]" metric_continuity nil)
    (metric nonempty-type-eq-decl nil metric_def nil)
    (metric? const-decl "bool" metric_def nil)
    (nnreal type-eq-decl nil real_types 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)
    (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)
    (number nonempty-type-decl nil numbers nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (interior_point? const-decl "bool" topology "topology/")
    (continuous_at? const-decl "bool" continuity_def "topology/"))
   shostak))
 (metric_continuous_def 0
  (metric_continuous_def-1 nil 3324700803
   ("" (skosimp)
    (("" (expand "continuous?")
      (("" (expand "metric_continuous?")
        (("" (split)
          (("1" (skosimp*)
            (("1" (inst - "x!1")
              (("1"
                (lemma "metric_continuous_at_def"
                 ("f" "f!1" "x0" "x!1"))
                (("1" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (skosimp*)
            (("2" (inst - "x!1")
              (("2"
                (lemma "metric_continuous_at_def"
                 ("f" "f!1" "x0" "x!1"))
                (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((continuous? const-decl "bool" continuity_def "topology/")
    (T1 formal-type-decl nil metric_continuity nil)
    (metric_continuous_at_def formula-decl nil metric_continuity nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (metric_continuous? const-decl "bool" metric_continuity nil))
   shostak))
 (metric_continuity_limit 0
  (metric_continuity_limit-1 nil 3359166753
   ("" (skosimp)
    (("" (expand "convergence?")
      (("" (skosimp*)
        (("" (rewrite "metric_continuous_at_def" -2 :dir rl)
          (("" (expand "continuous_at?")
            (("" (inst -2 "U!1")
              (("" (split -2)
                (("1" (expand "neighbourhood?")
                  (("1" (expand "interior_point?")
                    (("1" (skosimp)
                      (("1" (typepred "U!2")
                        (("1" (inst -4 "U!2")
                          (("1" (assert)
                            (("1" (skosimp)
                              (("1"
                                (inst + "n!1")
                                (("1"
                                  (skosimp)
                                  (("1"
                                    (inst -4 "i!1")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "o")
                                        (("1"
                                          (expand "subset?")
                                          (("1"
                                            (inst - "u!1(i!1)")
                                            (("1"
                                              (expand "member")
                                              (("1"
                                                (expand
                                                 "inverse_image")
                                                (("1"
                                                  (expand "member")
                                                  (("1"
                                                    (propax)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (expand "neighbourhood?")
                    (("2" (expand "interior_point?")
                      (("2" (typepred "U!1")
                        (("2" (inst + "U!1")
                          (("2" (expand "member")
                            (("2" (rewrite "subset_reflexive") nil
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergence? const-decl "bool" topological_convergence
     "topology/")
    (metric_continuous_at_def formula-decl nil metric_continuity nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (number nonempty-type-decl nil numbers 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)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (metric? const-decl "bool" metric_def nil)
    (metric nonempty-type-eq-decl nil metric_def nil)
    (d2 formal-const-decl "metric[T2]" metric_continuity nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     nil)
    (open? const-decl "bool" topology "topology/")
    (open nonempty-type-eq-decl nil topology "topology/")
    (subset_reflexive formula-decl nil sets_lemmas nil)
    (neighbourhood? const-decl "bool" topology "topology/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (subset? const-decl "bool" sets nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (sequence type-eq-decl nil sequences nil)
    (O const-decl "T3" function_props nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (d1 formal-const-decl "metric[T1]" metric_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (interior_point? const-decl "bool" topology "topology/")
    (continuous_at? const-decl "bool" continuity_def "topology/"))
   shostak))
 (metric_continuous_is_continuous 0
  (metric_continuous_is_continuous-1 nil 3383401763
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (rewrite "metric_continuous_def") nil nil)) nil))
    nil)
   ((metric_continuous type-eq-decl nil metric_continuity nil)
    (metric_continuous? const-decl "bool" metric_continuity nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (metric_continuous_def formula-decl nil metric_continuity nil))
   nil))
 (continuous_is_metric_continuous 0
  (continuous_is_metric_continuous-1 nil 3383401763
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (rewrite "metric_continuous_def") nil nil)) nil))
    nil)
   ((continuous type-eq-decl nil continuity_def "topology/")
    (continuous? const-decl "bool" continuity_def "topology/")
    (d2 formal-const-decl "metric[T2]" metric_continuity nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     nil)
    (d1 formal-const-decl "metric[T1]" metric_continuity nil)
    (metric nonempty-type-eq-decl nil metric_def nil)
    (metric? const-decl "bool" metric_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (metric_continuous_def formula-decl nil metric_continuity nil))
   nil))
 (uniform_continuous 0
  (uniform_continuous-1 nil 3337412454
   ("" (skosimp)
    (("" (rewrite "metric_continuous_def")
      (("" (expand "metric_continuous?")
        (("" (expand "uniform_continuous?")
          (("" (expand "metric_continuous_at?")
            (("" (expand "ball")
              (("" (expand "member")
                (("" (skosimp*)
                  (("" (inst - "epsilon!1")
                    (("" (skosimp)
                      (("" (inst + "delta!1")
                        (("" (skosimp)
                          (("" (inst - "x!2" "x!1")
                            (("" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((metric_continuous_def formula-decl nil metric_continuity nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (uniform_continuous? const-decl "bool" metric_continuity nil)
    (ball const-decl "set[T]" metric_space_def nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (bool nonempty-type-eq-decl nil booleans 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)
    (member const-decl "bool" sets nil)
    (metric_continuous_at? const-decl "bool" metric_continuity nil)
    (metric_continuous? const-decl "bool" metric_continuity nil))
   shostak))
 (uniform_continuous_is_continuous 0
  (uniform_continuous_is_continuous-1 nil 3383401763
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (lemma "uniform_continuous" ("f" "x!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((uniform_continuous type-eq-decl nil metric_continuity nil)
    (uniform_continuous? const-decl "bool" metric_continuity nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (uniform_continuous formula-decl nil metric_continuity nil))
   nil))
 (compact_uniform_continuous 0
  (compact_uniform_continuous-1 nil 3359167367
   ("" (skosimp)
    (("" (split)
      (("1" (flatten)
        (("1" (expand "uniform_continuous?")
          (("1" (skosimp*)
            (("1" (rewrite "metric_continuous_def")
              (("1"
                (name "DELTA"
                      "LAMBDA x: {delta| forall (y:T1): d1(x,y)<2*delta => d2(f!1(x),f!1(y))<epsilon!1/2}")
                (("1" (case "forall x: nonempty?[posreal](DELTA(x))")
                  (("1"
                    (name "Delta"
                          "LAMBDA x: choose[posreal](DELTA(x))")
                    (("1" (hide -3)
                      (("1" (case "forall x: Delta(x)>0")
                        (("1" (expand "compact_subset?")
                          (("1"
                            (inst -5
                             "image((LAMBDA x: ball(x,Delta(x))),fullset[T1])")
                            (("1" (split -5)
                              (("1"
                                (skosimp)
                                (("1"
                                  (expand "finite_cover?")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (name "N" "card(V!1)")
                                      (("1"
                                        (name
                                         "Centres"
                                         "{x| V!1(ball(x,Delta(x)))}")
                                        (("1"
                                          (name
                                           "F"
                                           "lambda x: ball(x,Delta(x))")
                                          (("1"
                                            (replace -1)
                                            (("1"
                                              (case "nonempty?(V!1)")
                                              (("1"
                                                (lemma
                                                 "nonempty_card[set[T1]]"
                                                 ("S" "V!1"))
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (replace -5)
                                                    (("1"
                                                      (case
                                                       "surjective?[(Centres),(V!1)](F)")
                                                      (("1"
                                                        (lemma
                                                         "surjective_inverse_exists[(Centres),(V!1)]"
                                                         ("f" "F"))
                                                        (("1"
                                                          (skosimp)
                                                          (("1"
                                                            (expand
                                                             "restrict")
                                                            (("1"
                                                              (expand
                                                               "inverse?")
                                                              (("1"
                                                                (case
                                                                 "injective?[(V!1),(Centres)](g!1)")
                                                                (("1"
                                                                  (name
                                                                   "X"
                                                                   "image(g!1, fullset[(V!1)])")
                                                                  (("1"
                                                                    (case
                                                                     "bijective?[(V!1),(X)](g!1)")
                                                                    (("1"
                                                                      (case
                                                                       "is_finite(X)")
                                                                      (("1"
                                                                        (case
                                                                         "card(X) = N")
                                                                        (("1"
                                                                          (lemma
                                                                           "comp_inverse_right_alt[(V!1), (X)]"
                                                                           ("f"
                                                                            "g!1"
                                                                            "g"
                                                                            "F"))
                                                                          (("1"
                                                                            (expand
                                                                             "restrict")
                                                                            (("1"
                                                                              (name
                                                                               "SS"
                                                                               "image[(X),posreal](Delta,X)")
                                                                              (("1"
                                                                                (lemma
                                                                                 "finite_image[(X),posreal]"
                                                                                 ("f"
                                                                                  "Delta"
                                                                                  "S"
                                                                                  "X"))
                                                                                (("1"
                                                                                  (replace
                                                                                   -2)
                                                                                  (("1"
                                                                                    (hide
                                                                                     -2)
                                                                                    (("1"
                                                                                      (case
                                                                                       "nonempty?(SS)")
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "min_lem"
                                                                                         ("SS"
                                                                                          "SS"
                                                                                          "a"
                                                                                          "min(SS)"))
                                                                                        (("1"
                                                                                          (assert)
                                                                                          (("1"
                                                                                            (case
                                                                                             "forall x: exists (y:(X)): F(y)(x)")
                                                                                            (("1"
                                                                                              (inst
                                                                                               +
                                                                                               "min(SS)")
                                                                                              (("1"
                                                                                                (skosimp)
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "F"
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (expand
                                                                                                     "ball"
                                                                                                     (-1
                                                                                                      -25
                                                                                                      1))
                                                                                                    (("1"
                                                                                                      (inst
                                                                                                       -
                                                                                                       "x0!1")
                                                                                                      (("1"
                                                                                                        (skosimp)
                                                                                                        (("1"
                                                                                                          (typepred
                                                                                                           "y!1")
                                                                                                          (("1"
                                                                                                            (inst
                                                                                                             -
                                                                                                             "Delta(y!1)")
                                                                                                            (("1"
                                                                                                              (lemma
                                                                                                               "metric_triangle"
                                                                                                               ("x"
                                                                                                                "y!1"
                                                                                                                "y"
                                                                                                                "x0!1"
                                                                                                                "z"
                                                                                                                "x!1"))
                                                                                                              (("1"
                                                                                                                (case
                                                                                                                 "d1(y!1, x!1) < 2*Delta(y!1)")
                                                                                                                (("1"
                                                                                                                  (hide
                                                                                                                   -2)
                                                                                                                  (("1"
                                                                                                                    (inst
                                                                                                                     -26
                                                                                                                     "y!1")
                                                                                                                    (("1"
                                                                                                                      (lemma
                                                                                                                       "choose_member[posreal]"
                                                                                                                       ("a"
                                                                                                                        "DELTA(y!1)"))
                                                                                                                      (("1"
                                                                                                                        (split
                                                                                                                         -1)
                                                                                                                        (("1"
                                                                                                                          (expand
                                                                                                                           "member")
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "DELTA"
                                                                                                                             -1
                                                                                                                             1)
                                                                                                                            (("1"
                                                                                                                              (inst
                                                                                                                               -
                                                                                                                               "x!1")
                                                                                                                              (("1"
                                                                                                                                (split
                                                                                                                                 -1)
                                                                                                                                (("1"
                                                                                                                                  (lemma
                                                                                                                                   "choose_member[posreal]"
                                                                                                                                   ("a"
                                                                                                                                    "DELTA(y!1)"))
                                                                                                                                  (("1"
                                                                                                                                    (split
                                                                                                                                     -1)
                                                                                                                                    (("1"
                                                                                                                                      (expand
                                                                                                                                       "member")
                                                                                                                                      (("1"
                                                                                                                                        (expand
                                                                                                                                         "DELTA"
                                                                                                                                         -1
                                                                                                                                         1)
                                                                                                                                        (("1"
                                                                                                                                          (inst
                                                                                                                                           -
                                                                                                                                           "x0!1")
                                                                                                                                          (("1"
                                                                                                                                            (split
                                                                                                                                             -1)
                                                                                                                                            (("1"
                                                                                                                                              (lemma
                                                                                                                                               "metric_triangle"
                                                                                                                                               ("x"
                                                                                                                                                "f!1(x0!1)"
                                                                                                                                                "y"
                                                                                                                                                "f!1(y!1)"
                                                                                                                                                "z"
                                                                                                                                                "f!1(x!1)"))
                                                                                                                                              (("1"
                                                                                                                                                (rewrite
                                                                                                                                                 "metric_symmetric"
                                                                                                                                                 -2)
                                                                                                                                                (("1"
                                                                                                                                                  (assert)
                                                                                                                                                  nil
                                                                                                                                                  nil))
                                                                                                                                                nil))
                                                                                                                                              nil)
                                                                                                                                             ("2"
                                                                                                                                              (expand
                                                                                                                                               "Delta"
                                                                                                                                               -5)
                                                                                                                                              (("2"
                                                                                                                                                (assert)
                                                                                                                                                nil
                                                                                                                                                nil))
                                                                                                                                              nil))
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil)
                                                                                                                                     ("2"
                                                                                                                                      (expand
                                                                                                                                       "nonempty?")
                                                                                                                                      (("2"
                                                                                                                                        (propax)
                                                                                                                                        nil
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil)
                                                                                                                                 ("2"
                                                                                                                                  (expand
                                                                                                                                   "Delta")
                                                                                                                                  (("2"
                                                                                                                                    (propax)
                                                                                                                                    nil
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil)
                                                                                                                         ("2"
                                                                                                                          (expand
                                                                                                                           "nonempty?")
                                                                                                                          (("2"
                                                                                                                            (propax)
                                                                                                                            nil
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil)
                                                                                                                 ("2"
                                                                                                                  (assert)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (expand
                                                                                                               "SS")
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "restrict")
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "image")
                                                                                                                  (("2"
                                                                                                                    (inst
                                                                                                                     +
                                                                                                                     "y!1")
                                                                                                                    nil
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil)
                                                                                               ("2"
                                                                                                (expand
                                                                                                 "nonempty?")
                                                                                                (("2"
                                                                                                  (propax)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (hide
                                                                                               -23
                                                                                               2)
                                                                                              (("2"
                                                                                                (skosimp)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "cover?")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "Union")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "subset?")
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "member")
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           -19
                                                                                                           "x!1")
                                                                                                          (("2"
                                                                                                            (split
                                                                                                             -19)
                                                                                                            (("1"
                                                                                                              (skosimp)
                                                                                                              (("1"
                                                                                                                (typepred
                                                                                                                 "a!1")
                                                                                                                (("1"
                                                                                                                  (inst
                                                                                                                   -19
                                                                                                                   "a!1")
                                                                                                                  (("1"
                                                                                                                    (assert)
                                                                                                                    (("1"
                                                                                                                      (expand
                                                                                                                       "fullset")
                                                                                                                      (("1"
                                                                                                                        (expand
                                                                                                                         "image")
                                                                                                                        (("1"
                                                                                                                          (skosimp)
                                                                                                                          (("1"
                                                                                                                            (typepred
                                                                                                                             "g!1(a!1)")
                                                                                                                            (("1"
                                                                                                                              (inst
                                                                                                                               -13
                                                                                                                               "a!1")
                                                                                                                              (("1"
                                                                                                                                (split
                                                                                                                                 -13)
                                                                                                                                (("1"
                                                                                                                                  (inst
                                                                                                                                   +
                                                                                                                                   "g!1(a!1)")
                                                                                                                                  (("1"
                                                                                                                                    (assert)
                                                                                                                                    nil
                                                                                                                                    nil)
                                                                                                                                   ("2"
                                                                                                                                    (assert)
                                                                                                                                    (("2"
                                                                                                                                      (expand
                                                                                                                                       "X")
                                                                                                                                      (("2"
                                                                                                                                        (expand
                                                                                                                                         "fullset")
                                                                                                                                        (("2"
                                                                                                                                          (expand
                                                                                                                                           "image")
                                                                                                                                          (("2"
                                                                                                                                            (inst
                                                                                                                                             +
                                                                                                                                             "a!1")
                                                                                                                                            nil
                                                                                                                                            nil))
                                                                                                                                          nil))
                                                                                                                                        nil))
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil)
                                                                                                                                 ("2"
                                                                                                                                  (hide
                                                                                                                                   2)
                                                                                                                                  (("2"
                                                                                                                                    (expand
                                                                                                                                     "surjective?")
                                                                                                                                    (("2"
                                                                                                                                      (inst
                                                                                                                                       -13
                                                                                                                                       "a!1")
                                                                                                                                      nil
                                                                                                                                      nil))
                                                                                                                                    nil))
                                                                                                                                  nil))
                                                                                                                                nil))
                                                                                                                              nil))
                                                                                                                            nil))
                                                                                                                          nil))
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil)
                                                                                                             ("2"
                                                                                                              (hide-all-but
                                                                                                               1)
                                                                                                              (("2"
                                                                                                                (lemma
                                                                                                                 "ball_centre"
                                                                                                                 ("x"
                                                                                                                  "x!1"
                                                                                                                  "r"
                                                                                                                  "1"))
                                                                                                                (("2"
                                                                                                                  (expand
                                                                                                                   "member")
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "fullset")
                                                                                                                    (("2"
                                                                                                                      (propax)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (expand
                                                                                           "nonempty?")
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil)
                                                                                       ("2"
                                                                                        (expand
                                                                                         "nonempty?"
                                                                                         1)
                                                                                        (("2"
                                                                                          (expand
                                                                                           "SS")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "restrict")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "image")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "nonempty?")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "empty?")
                                                                                                  (("2"
                                                                                                    (skosimp)
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "member")
                                                                                                      (("2"
                                                                                                        (inst
                                                                                                         -
                                                                                                         "Delta(g!1(x!1))")
                                                                                                        (("2"
                                                                                                          (inst
                                                                                                           +
                                                                                                           "g!1(x!1)")
                                                                                                          (("2"
                                                                                                            (assert)
                                                                                                            (("2"
                                                                                                              (expand
                                                                                                               "X")
                                                                                                              (("2"
                                                                                                                (expand
                                                                                                                 "image")
                                                                                                                (("2"
                                                                                                                  (inst
                                                                                                                   +
                                                                                                                   "x!1")
                                                                                                                  (("2"
                                                                                                                    (expand
                                                                                                                     "fullset")
                                                                                                                    (("2"
                                                                                                                      (propax)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (hide-all-but
                                                                                   (-4
                                                                                    1))
                                                                                  (("2"
                                                                                    (expand
                                                                                     "restrict")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "is_finite")
                                                                                      (("2"
                                                                                        (propax)
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("2"
                                                                            (hide
                                                                             2)
                                                                            (("2"
                                                                              (expand
                                                                               "inverse?")
                                                                              (("2"
                                                                                (skosimp)
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (typepred
                                                                                     "r!1")
                                                                                    (("2"
                                                                                      (typepred
                                                                                       "d!1")
                                                                                      (("2"
                                                                                        (inst
                                                                                         -10
                                                                                         "d!1")
                                                                                        (("2"
                                                                                          (split
                                                                                           -10)
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (replace
                                                                                               -5)
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "restrict")
                                                                                                (("1"
                                                                                                  (replace
                                                                                                   -1)
                                                                                                  (("1"
                                                                                                    (propax)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (hide
                                                                                             2)
                                                                                            (("2"
                                                                                              (expand
                                                                                               "surjective?")
                                                                                              (("2"
                                                                                                (inst
                                                                                                 -10
                                                                                                 "d!1")
                                                                                                nil
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil)
                                                                           ("3"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (hide-all-but
                                                                           (-1
                                                                            -2
                                                                            -11
                                                                            1
                                                                            -13))
                                                                          (("2"
                                                                            (lemma
                                                                             "card_bij_inv[T1]"
                                                                             ("S"
                                                                              "X"
                                                                              "N"
                                                                              "N"))
                                                                            (("1"
                                                                              (hide
                                                                               -1)
                                                                              (("1"
                                                                                (lemma
                                                                                 "card_bij_inv[set[T1]]"
                                                                                 ("S"
                                                                                  "V!1"
                                                                                  "N"
                                                                                  "N"))
                                                                                (("1"
                                                                                  (assert)
                                                                                  (("1"
                                                                                    (skosimp)
                                                                                    (("1"
                                                                                      (expand
                                                                                       "bijective?")
                                                                                      (("1"
                                                                                        (flatten)
                                                                                        (("1"
                                                                                          (expand
                                                                                           "injective?")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            (("1"
                                                                                              (rewrite
                                                                                               "card_bij_inv"
                                                                                               +)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 +
                                                                                                 "lambda (x:below[N]): g!1(f!2(x))")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "bijective?")
                                                                                                  (("1"
                                                                                                    (split)
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "injective?")
                                                                                                      (("1"
                                                                                                        (skosimp)
                                                                                                        (("1"
                                                                                                          (inst
                                                                                                           -
                                                                                                           "x1!1"
                                                                                                           "x2!1")
                                                                                                          (("1"
                                                                                                            (assert)
                                                                                                            (("1"
                                                                                                              (inst
                                                                                                               -
                                                                                                               "f!2(x1!1)"
                                                                                                               "f!2(x2!1)")
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                nil
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil)
                                                                                                     ("2"
                                                                                                      (hide-all-but
                                                                                                       (-2
                                                                                                        -5
                                                                                                        1))
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "surjective?")
                                                                                                        (("2"
                                                                                                          (skosimp)
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             -2
                                                                                                             "y!1")
                                                                                                            (("2"
                                                                                                              (skosimp)
                                                                                                              (("2"
                                                                                                                (typepred
                                                                                                                 "x!1")
                                                                                                                (("2"
                                                                                                                  (inst
                                                                                                                   -
                                                                                                                   "x!1")
                                                                                                                  (("2"
                                                                                                                    (skosimp)
                                                                                                                    (("2"
                                                                                                                      (inst
                                                                                                                       +
                                                                                                                       "x!2")
                                                                                                                      (("2"
                                                                                                                        (assert)
                                                                                                                        nil
                                                                                                                        nil))
                                                                                                                      nil))
                                                                                                                    nil))
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (skosimp)
                                                                                                  (("2"
                                                                                                    (typepred
                                                                                                     "g!1(f!2(x!1))")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "X"
                                                                                                       1)
                                                                                                      (("2"
                                                                                                        (expand
                                                                                                         "fullset")
                                                                                                        (("2"
                                                                                                          (expand
                                                                                                           "image")
                                                                                                          (("2"
                                                                                                            (inst
                                                                                                             +
                                                                                                             "f!2(x!1)")
                                                                                                            nil
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil)
                                                                             ("2"
                                                                              (hide-all-but
                                                                               (-1
                                                                                1))
                                                                              (("2"
                                                                                (expand
                                                                                 "is_finite")
                                                                                (("2"
                                                                                  (skolem
                                                                                   -
                                                                                   ("NN"
                                                                                    "FF"))
                                                                                  (("2"
                                                                                    (inst
                                                                                     +
                                                                                     "NN"
                                                                                     "lambda (x:(extend[T1, ((Centres)), bool, FALSE](X))): FF(x)")
                                                                                    (("1"
                                                                                      (expand
                                                                                       "injective?")
                                                                                      (("1"
                                                                                        (skosimp)
                                                                                        (("1"
                                                                                          (inst
                                                                                           -
                                                                                           "x1!1"
                                                                                           "x2!1")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (skosimp)
                                                                                      (("2"
                                                                                        (typepred
                                                                                         "x!1")
                                                                                        (("2"
                                                                                          (expand
                                                                                           "extend")
                                                                                          (("2"
                                                                                            (prop)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("3"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (hide-all-but
                                                                         (-1
                                                                          -12
                                                                          1))
                                                                        (("2"
                                                                          (lemma
                                                                           "is_finite_surj[set[T1]]"
                                                                           ("s"
                                                                            "V!1"))
                                                                          (("2"
                                                                            (assert)
                                                                            (("2"
                                                                              (skosimp)
                                                                              (("2"
                                                                                (expand
                                                                                 "bijective?")
                                                                                (("2"
                                                                                  (flatten)
                                                                                  (("2"
                                                                                    (lemma
                                                                                     "is_finite_surj[(Centres)]"
                                                                                     ("s"
                                                                                      "X"))
                                                                                    (("2"
                                                                                      (replace
                                                                                       -1
                                                                                       1
                                                                                       rl)
                                                                                      (("2"
                                                                                        (hide
                                                                                         -1
                                                                                         -3
                                                                                         -5)
                                                                                        (("2"
                                                                                          (expand
                                                                                           "surjective?")
                                                                                          (("2"
                                                                                            (inst
                                                                                             +
                                                                                             "N!1"
                                                                                             "lambda (x:below[N!1]): g!1(f!2(x))")
                                                                                            (("1"
                                                                                              (skosimp)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 -2
                                                                                                 "y!1")
                                                                                                (("1"
                                                                                                  (skosimp)
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     -
                                                                                                     "x!1")
                                                                                                    (("1"
                                                                                                      (skosimp)
                                                                                                      (("1"
                                                                                                        (inst
                                                                                                         +
                                                                                                         "x!2")
                                                                                                        (("1"
                                                                                                          (assert)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (skosimp)
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "X")
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "fullset")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "image")
                                                                                                    (("2"
                                                                                                      (inst
                                                                                                       +
                                                                                                       "f!2(x!1)")
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (hide-all-but
                                                                       (-1
                                                                        -2
                                                                        1))
                                                                      (("2"
                                                                        (lemma
                                                                         "bijective_image[(V!1),(Centres)]"
                                                                         ("inj"
                                                                          "g!1"))
                                                                        (("1"
                                                                          (expand
                                                                           "bijective?")
                                                                          (("1"
                                                                            (flatten)
                                                                            (("1"
                                                                              (split)
                                                                              (("1"
                                                                                (expand
                                                                                 "injective?")
                                                                                (("1"
                                                                                  (propax)
                                                                                  nil
                                                                                  nil))
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "surjective?")
                                                                                (("2"
                                                                                  (skosimp)
                                                                                  (("2"
                                                                                    (typepred
                                                                                     "y!1")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "X")
                                                                                      (("2"
                                                                                        (inst
                                                                                         -
                                                                                         "y!1")
                                                                                        nil
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (propax)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("3"
                                                                      (hide-all-but
                                                                       (-1
                                                                        1))
                                                                      (("3"
                                                                        (expand
                                                                         "fullset")
                                                                        (("3"
                                                                          (expand
                                                                           "image")
                                                                          (("3"
                                                                            (replace
                                                                             -1
                                                                             1
                                                                             rl)
                                                                            (("3"
                                                                              (skosimp)
                                                                              (("3"
                                                                                (inst
                                                                                 +
                                                                                 "x1!1")
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   -14
                                                                   2
                                                                   -3
                                                                   -4
                                                                   -7
                                                                   -9)
                                                                  (("2"
                                                                    (expand
                                                                     "injective?")
                                                                    (("2"
                                                                      (skosimp)
                                                                      (("2"
                                                                        (typepred
                                                                         "x1!1")
                                                                        (("2"
                                                                          (typepred
                                                                           "x2!1")
                                                                          (("2"
                                                                            (inst-cp
                                                                             -
                                                                             "x1!1")
                                                                            (("2"
                                                                              (inst
                                                                               -
                                                                               "x2!1")
                                                                              (("2"
                                                                                (split
                                                                                 -4)
                                                                                (("1"
                                                                                  (split
                                                                                   -5)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "F")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil)
                                                                                   ("2"
                                                                                    (expand
                                                                                     "subset?")
                                                                                    (("2"
                                                                                      (inst
                                                                                       -8
                                                                                       "x1!1")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "fullset")
                                                                                        (("2"
                                                                                          (expand
                                                                                           "image")
                                                                                          (("2"
                                                                                            (expand
                                                                                             "member")
                                                                                            (("2"
                                                                                              (skosimp)
                                                                                              (("2"
                                                                                                (inst
                                                                                                 +
                                                                                                 "x!1")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (expand
                                                                                   "subset?")
                                                                                  (("2"
                                                                                    (expand
                                                                                     "fullset")
                                                                                    (("2"
                                                                                      (expand
                                                                                       "image")
                                                                                      (("2"
                                                                                        (expand
                                                                                         "member")
                                                                                        (("2"
                                                                                          (inst
                                                                                           -8
                                                                                           "x2!1")
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (skosimp)
                                                                                              (("2"
                                                                                                (inst
                                                                                                 +
                                                                                                 "x!1")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil)
                                                                                                 ("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (hide 2)
                                                        (("2"
                                                          (expand
                                                           "restrict")
                                                          (("2"
                                                            (expand
                                                             "surjective?")
                                                            (("2"
                                                              (skosimp)
                                                              (("2"
                                                                (typepred
                                                                 "y!1")
                                                                (("2"
                                                                  (expand
                                                                   "subset?")
                                                                  (("2"
                                                                    (inst
                                                                     -
                                                                     "y!1")
                                                                    (("2"
                                                                      (expand
                                                                       "member")
                                                                      (("2"
                                                                        (expand
                                                                         "fullset")
                                                                        (("2"
                                                                          (expand
                                                                           "image")
                                                                          (("2"
                                                                            (skosimp)
                                                                            (("2"
                                                                              (inst
                                                                               +
                                                                               "x!1")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil)
                                                                               ("2"
                                                                                (expand
                                                                                 "Centres")
                                                                                (("2"
                                                                                  (expand
                                                                                   "F")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (expand "nonempty?")
                                                (("2"
                                                  (lemma
                                                   "empty_card[set[T1]]"
                                                   ("S" "V!1"))
                                                  (("2"
                                                    (lemma
                                                     "emptyset_is_empty?"
                                                     ("a" "V!1"))
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (replace -1)
                                                        (("2"
                                                          (hide
                                                           -3
                                                           -6
                                                           -7
                                                           -8)
                                                          (("2"
                                                            (expand
                                                             "cover?")
                                                            (("2"
                                                              (expand
                                                               "subset?")
                                                              (("2"
                                                                (expand
                                                                 "emptyset"
                                                                 -5)
                                                                (("2"
                                                                  (expand
                                                                   "member")
                                                                  (("2"
                                                                    (case
                                                                     "nonempty?(fullset[T1])")
                                                                    (("1"
                                                                      (expand
                                                                       "nonempty?")
                                                                      (("1"
                                                                        (expand
                                                                         "fullset")
                                                                        (("1"
                                                                          (expand
                                                                           "empty?")
                                                                          (("1"
                                                                            (skosimp)
                                                                            (("1"
                                                                              (inst
                                                                               -6
                                                                               "x!1")
                                                                              (("1"
                                                                                (expand
                                                                                 "Union"
                                                                                 -6)
                                                                                (("1"
                                                                                  (skosimp)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil)
                                                                     ("2"
                                                                      (expand
                                                                       "nonempty?")
                                                                      (("2"
                                                                        (expand
                                                                         "fullset")
                                                                        (("2"
                                                                          (expand
                                                                           "empty?")
                                                                          (("2"
                                                                            (expand
                                                                             "member")
                                                                            (("2"
                                                                              (inst
                                                                               +
                                                                               "1")
                                                                              (("2"
                                                                                (skosimp)
                                                                                (("2"
                                                                                  (inst
                                                                                   -
                                                                                   "x0!1")
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide 2)
                                (("2"
                                  (expand "open_cover?")
                                  (("2"
                                    (split)
                                    (("1"
                                      (expand "subset?")
                                      (("1"
                                        (expand "image")
                                        (("1"
                                          (expand "member")
                                          (("1"
                                            (skosimp)
                                            (("1"
                                              (skosimp)
                                              (("1"
                                                (expand
                                                 "metric_induced_topology")
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (expand
                                                     "metric_open?")
                                                    (("1"
                                                      (skosimp)
                                                      (("1"
                                                        (case-replace
                                                         "ball(x!2, Delta(x!2))(x!3)")
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (expand
                                                             "ball")
                                                            (("1"
                                                              (inst
                                                               +
                                                               "Delta(x!2)-d1(x!2,x!3)")
                                                              (("1"
                                                                (expand
                                                                 "subset?")
                                                                (("1"
                                                                  (expand
                                                                   "member")
                                                                  (("1"
                                                                    (skosimp)
                                                                    (("1"
                                                                      (typepred
                                                                       "d1")
                                                                      (("1"
                                                                        (expand
                                                                         "metric?")
                                                                        (("1"
                                                                          (flatten)
                                                                          (("1"
                                                                            (expand
                                                                             "metric_triangle?")
                                                                            (("1"
                                                                              (inst
                                                                               -
                                                                               "x!2"
                                                                               "x!3"
                                                                               "x!4")
                                                                              (("1"
                                                                                (assert)
                                                                                nil
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil)
                                                               ("2"
                                                                (assert)
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (assert)
                                                          (("2"
                                                            (skosimp)
                                                            (("2"
                                                              (expand
                                                               "subset?")
                                                              (("2"
                                                                (inst
                                                                 -
                                                                 "x!3")
                                                                (("2"
                                                                  (rewrite
                                                                   "ball_centre")
                                                                  (("2"
                                                                    (expand
                                                                     "member")
                                                                    (("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "cover?")
                                      (("2"
                                        (expand "subset?")
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (skosimp*)
                                            (("2"
                                              (expand "fullset")
                                              (("2"
                                                (expand "image")
                                                (("2"
                                                  (expand "Union")
                                                  (("2"
                                                    (inst
                                                     +
                                                     "ball(x!1,Delta(x!1))")
                                                    (("1"
                                                      (lemma
                                                       "ball_centre"
                                                       ("x"
                                                        "x!1"
                                                        "r"
                                                        "Delta(x!1)"))
                                                      (("1"
                                                        (expand
                                                         "member")
                                                        (("1"
                                                          (propax)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (inst + "x!1")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skosimp)
                          (("2" (expand "Delta")
                            (("2" (inst - "x!1")
                              (("2"
                                (expand "nonempty?")
                                (("2"
                                  (lemma
                                   "choose_member[posreal]"
                                   ("a" "DELTA(x!1)"))
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (propax) nil nil))
                    nil)
                   ("2" (expand "nonempty?")
                    (("2" (skosimp)
                      (("2" (expand "empty?")
                        (("2" (expand "DELTA")
                          (("2" (hide -2)
                            (("2" (expand "member")
                              (("2"
                                (expand "metric_continuous?")
                                (("2"
                                  (expand "metric_continuous_at?")
                                  (("2"
                                    (inst -2 "x!1")
                                    (("2"
                                      (inst -2 "epsilon!1/2")
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (expand "ball")
                                          (("2"
                                            (skosimp)
                                            (("2"
                                              (inst - "delta!1/2")
                                              (("2"
                                                (hide -2 2)
                                                (("2"
                                                  (skosimp)
                                                  (("2"
                                                    (inst - "y!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))
          nil))
        nil)
       ("2" (flatten) (("2" (rewrite "uniform_continuous") nil nil))
        nil))
      nil))
    nil)
   ((uniform_continuous? const-decl "bool" metric_continuity nil)
    (metric_continuous_def formula-decl nil metric_continuity nil)
    (T1 formal-type-decl nil metric_continuity nil)
    (T2 formal-type-decl nil metric_continuity nil)
    (set type-eq-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (compact_subset? const-decl "bool" topology_prelim "topology/")
    (finite_cover? const-decl "bool" topology_prelim "topology/")
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (metric_open? const-decl "bool" metric_space_def nil)
    (metric_open nonempty-type-eq-decl nil metric_space nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (fullset_is_clopen name-judgement
     "clopen[T, (metric_induced_topology)]" metric_continuity nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (surjective? const-decl "bool" functions nil)
    (restrict const-decl "R" restrict nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (x!1 skolem-const-decl "({x | TRUE})" metric_continuity nil)
    (x!1 skolem-const-decl "({x | TRUE})" metric_continuity nil)
    (y!1 skolem-const-decl "(X)" metric_continuity nil)
    (bijective_image formula-decl nil function_image_aux nil)
    (f!2 skolem-const-decl "[below[N] -> (V!1)]" metric_continuity nil)
    (below type-eq-decl nil nat_types nil)
    (N skolem-const-decl "{n: nat | n = Card[setof[T1]](V!1)}"
     metric_continuity nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (card_bij_inv formula-decl nil finite_sets nil)
    (comp_inverse_right_alt formula-decl nil function_inverse_def nil)
    (cover? const-decl "bool" topology_prelim "topology/")
    (subset? const-decl "bool" sets nil)
    (ball_centre formula-decl nil metric_space nil)
    (V!1 skolem-const-decl "setofsets[T1]" metric_continuity nil)
    (g!1 skolem-const-decl "[(V!1) -> (Centres)]" metric_continuity
     nil)
    (a!1 skolem-const-decl "(V!1)" metric_continuity nil)
    (Union const-decl "set" sets nil)
    (SS skolem-const-decl "set[posreal]" metric_continuity nil)
    (F skolem-const-decl "[T1 -> metric_open[T1, d1]]"
     metric_continuity nil)
    (TRUE const-decl "bool" booleans nil)
    (metric_triangle formula-decl nil metric_space nil)
    (choose_member formula-decl nil sets_lemmas nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (metric_symmetric formula-decl nil metric_space nil)
    (y!1 skolem-const-decl "(X)" metric_continuity nil)
    (X skolem-const-decl "set[(Centres)]" metric_continuity nil)
    (Centres skolem-const-decl "[T1 -> bool]" metric_continuity nil)
    (Delta skolem-const-decl "[x: T1 -> (DELTA(x))]" metric_continuity
     nil)
    (DELTA skolem-const-decl "[T1 -> [posreal -> boolean]]"
     metric_continuity nil)
    (<= const-decl "bool" reals nil)
    (min const-decl
         "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
         finite_sets_minmax "finite_sets/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (min_lem formula-decl nil finite_sets_minmax "finite_sets/")
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     restrict_order_props nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     restrict_order_props nil)
    (x!1 skolem-const-decl "setof[T1]" metric_continuity nil)
    (finite_image judgement-tcc nil function_image_aux nil)
    (is_finite_surj formula-decl nil finite_sets nil)
    (f!2 skolem-const-decl "[below[N!1] -> (V!1)]" metric_continuity
     nil)
    (N!1 skolem-const-decl "nat" metric_continuity nil)
    (bijective? const-decl "bool" functions nil)
    (injective? const-decl "bool" functions nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (x!1 skolem-const-decl "({x | TRUE})" metric_continuity nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (empty_card formula-decl nil finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[finite_set[T]]"
     countable_setofsets "sets_aux/")
    (finite_emptyset name-judgement "finite_set[set[T]]"
     countable_setofsets "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" countable_setofsets
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (emptyset const-decl "set" sets nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (open_cover? const-decl "bool" topology_prelim "topology/")
    (x!1 skolem-const-decl "T1" metric_continuity nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (x!2 skolem-const-decl "(fullset[T1])" metric_continuity nil)
    (x!3 skolem-const-decl "T1" metric_continuity nil)
    (metric_triangle? const-decl "bool" metric_def nil)
    (metric_induced_topology const-decl "setofsets[T]" metric_space_def
     nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (image const-decl "set[R]" function_image nil)
    (ball const-decl "set[T]" metric_space_def nil)
    (fullset const-decl "set" sets nil)
    (ball_is_metric_open application-judgement "metric_open"
     metric_continuity nil)
    (choose const-decl "(p)" sets nil)
    (metric_continuous_at? const-decl "bool" metric_continuity nil)
    (metric_continuous? const-decl "bool" metric_continuity nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (metric? const-decl "bool" metric_def nil)
    (metric nonempty-type-eq-decl nil metric_def nil)
    (d1 formal-const-decl "metric[T1]" metric_continuity nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (d2 formal-const-decl "metric[T2]" metric_continuity nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (uniform_continuous formula-decl nil metric_continuity nil))
   shostak)))