Quelle  bounded_nats.prf   Sprache: unbekannt

(bounded_nats
 (every_nonempty_set_has_least 0
  (every_nonempty_set_has_least-1 nil 3314637118
   ("" (skolem-typepred)
    (("" (use "non_empty_bounded_below_has_least")
      ((""
        (expand* "non_empty_bounded_below?" "nonempty?" "empty?"
         "member")
        (("" (skolem!)
          (("" (lemma "non_empty_finite_bounded_below")
            (("" (inst - "{t: T |  x!1(t) AND t <= x!2}")
              (("1" (expand "non_empty_bounded_below?")
                (("1" (flatten)
                  (("1"
                    (expand* "bounded_below?" "lower_bound?"
                     "restrict")
                    (("1" (skolem!)
                      (("1" (inst + "t!1")
                        (("1" (skolem!)
                          (("1" (inst-cp - "x!2")
                            (("1" (inst - "r!1")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (split)
                (("1" (expand "is_finite")
                  (("1"
                    (inst + "1 + x!2"
                     "LAMBDA (n: ({t: T | x!1(t) AND t <= x!2})): n")
                    (("1" (expand "injective?")
                      (("1" (skosimp) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (expand* "empty?" "member")
                  (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((non_empty_bounded_below_has_least judgement-tcc nil
     bounded_integers nil)
    (x!1 skolem-const-decl "(nonempty?[T])" bounded_nats nil)
    (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
     nil)
    (x!2 skolem-const-decl "T" bounded_nats nil)
    (<= const-decl "bool" reals nil)
    (is_finite const-decl "bool" finite_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (r!1 skolem-const-decl "(x!1)" bounded_nats nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (restrict const-decl "R" restrict nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (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)
    (injective? const-decl "bool" functions nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (non_empty_finite_bounded_below judgement-tcc nil
     non_empty_bounded_sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil bounded_nats nil)
    (T_pred const-decl "[nat -> boolean]" bounded_nats nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil)))