Quelle  reals_complete_more.prf  Sprache: unbekannt

(reals_complete_more
 (real_complete2 0
  (real_complete2-1 nil 3506273121
   ("" (skosimp*)
    (("" (lemma "real_complete")
      (("" (inst -1 "S!1")
        (("1" (assert)
          (("1" (split -1)
            (("1" (skosimp*)
              (("1" (inst 1 "y!2")
                (("1" (hide -2)
                  (("1" (expand "extend")
                    (("1" (expand "least_upper_bound")
                      (("1" (expand "least_upper_bound?")
                        (("1" (prop)
                          (("1" (hide -2)
                            (("1" (expand "upper_bound")
                              (("1"
                                (expand "upper_bound?")
                                (("1"
                                  (skosimp*)
                                  (("1" (inst?) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -1)
                            (("2" (skosimp*)
                              (("2"
                                (inst -2 "y!3")
                                (("2"
                                  (assert)
                                  (("2"
                                    (hide 1 2)
                                    (("2"
                                      (expand "upper_bound")
                                      (("2"
                                        (expand "upper_bound?")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (typepred "s!1")
                                            (("2"
                                              (assert)
                                              (("2" (inst?) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (inst 1 "y!1")
              (("2" (hide 2)
                (("2" (expand "upper_bound?")
                  (("2" (expand "upper_bound")
                    (("2" (skosimp*)
                      (("2" (inst?)
                        (("2" (typepred "s!1")
                          (("2" (expand "extend")
                            (("2" (assert) (("2" (ground) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (typepred "S!1")
          (("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((real_complete formula-decl nil bounded_real_defs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (s!1 skolem-const-decl "(extend[real, T, bool, FALSE](S!1))"
     reals_complete_more nil)
    (S!1 skolem-const-decl "(nonempty?[T])" reals_complete_more nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (least_upper_bound const-decl "bool" bound_defs nil)
    (upper_bound const-decl "bool" bound_defs nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (upper_bound? const-decl "bool" bounded_real_defs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (least_upper_bound? const-decl "bool" bounded_real_defs nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (T formal-subtype-decl nil reals_complete_more nil)
    (T_pred const-decl "[real -> boolean]" reals_complete_more nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets 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)
    (nonempty_extend application-judgement "(nonempty?[T])"
     extend_set_props nil))
   nil))
 (real_lower_complete2 0
  (real_lower_complete2-1 nil 3506273121
   ("" (skosimp*)
    (("" (lemma "real_lower_complete")
      (("" (inst -1 "S!1")
        (("1" (split -1)
          (("1" (skosimp*)
            (("1" (inst 1 "x!1")
              (("1" (hide -2)
                (("1" (expand "greatest_lower_bound")
                  (("1" (expand "greatest_lower_bound?")
                    (("1" (prop)
                      (("1" (hide -2)
                        (("1" (expand "lower_bound")
                          (("1" (expand "lower_bound?")
                            (("1" (skosimp*)
                              (("1"
                                (inst?)
                                (("1"
                                  (expand "extend")
                                  (("1" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -1)
                        (("2" (skosimp*)
                          (("2" (inst -2 "y!2")
                            (("2" (assert)
                              (("2"
                                (hide 1 2)
                                (("2"
                                  (expand "lower_bound")
                                  (("2"
                                    (expand "lower_bound?")
                                    (("2"
                                      (skosimp*)
                                      (("2"
                                        (inst?)
                                        (("2"
                                          (typepred "s!1")
                                          (("2" (grind) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide 2)
            (("2" (inst?)
              (("2" (expand "lower_bound?")
                (("2" (expand "lower_bound")
                  (("2" (skosimp*)
                    (("2" (inst?)
                      (("2" (typepred "s!1") (("2" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (typepred "S!1")
            (("2" (hide -2) (("2" (grind) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_lower_complete formula-decl nil bounded_real_defs nil)
    (greatest_lower_bound const-decl "bool" bound_defs nil)
    (lower_bound const-decl "bool" bound_defs nil)
    (z!1 skolem-const-decl "{x: T | S!1(x)}" reals_complete_more nil)
    (S!1 skolem-const-decl "(nonempty?[T])" reals_complete_more nil)
    (lower_bound? const-decl "bool" bounded_real_defs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (s!1 skolem-const-decl "(extend[real, T, bool, FALSE](S!1))"
     reals_complete_more nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (greatest_lower_bound? const-decl "bool" bounded_real_defs nil)
    (s!1 skolem-const-decl "(extend[real, T, bool, FALSE](S!1))"
     reals_complete_more nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (T formal-subtype-decl nil reals_complete_more nil)
    (T_pred const-decl "[real -> boolean]" reals_complete_more nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets 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)
    (nonempty_extend application-judgement "(nonempty?[T])"
     extend_set_props nil))
   nil)))