Quelle integer_enumerations.prf Sprache: Lisp

(integer_enumerations
(enumerable_below_bounded 0
  (enumerable_below_bounded-1 nil 3314637789
   ("" (skolem-typepred)
    (("" (expand* "enumerable?" "non_empty_bounded_below?")
      (("" (prop) (("" (use "infinite_nonempty") nil nil)) nil)) nil))
    nil)
   ((non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
     nil)
    (x!1 skolem-const-decl "(enumerable?)" integer_enumerations nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (infinite_nonempty judgement-tcc nil infinite_sets_def nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations 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))
(enumerable_infinite 0
  (enumerable_infinite-1 nil 3314637789 ("" (judgement-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (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)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (< const-decl "bool" reals nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (restrict const-decl "R" restrict nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     restrict_order_props nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil))
   nil))
(remove_enumerable 0
  (remove_enumerable-1 nil 3314637789
   ("" (skolem-typepred)
    (("" (expand "enumerable?")
      (("" (prop)
        (("1" (rewrite "remove_preserves_bounded_below") nil nil)
         ("2" (rewrite "infinite_remove") nil nil))
        nil))
      nil))
    nil)
   ((remove_preserves_bounded_below application-judgement
     "(LAMBDA (S: set[T]): bounded_below?(S, R))" integer_enumerations
     nil)
    (infinite_remove application-judgement "infinite_set[T]"
     integer_enumerations nil)
    (infinite_remove judgement-tcc nil infinite_sets_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil)
    (remove_preserves_bounded_below judgement-tcc nil bounded_sets nil)
    (pred type-eq-decl nil defined_types nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (restrict const-decl "R" restrict nil)
    (<= const-decl "bool" reals nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations 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))
(enum_TCC1 0
  (enum_TCC1-1 nil 3314637789 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (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)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (restrict const-decl "R" restrict nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (bounded_below? const-decl "bool" bounded_orders nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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))
   nil))
(enum_TCC2 0
  (enum_TCC2-1 nil 3314637789 ("" (termination-tcc) nil nil) nil nil))
(enum_member 0
  (enum_member-1 nil 3314637789
   ("" (induct "n")
    (("1" (skolem!)
      (("1" (expand "enum")
        (("1" (invoke (typepred "%1") (! 1 1))
          (("1" (expand* "least?" "member") (("1" (flatten) nil nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "enum" +)
        (("2" (inst?)
          (("2" (expand "remove" - 1)
            (("2" (expand "member") (("2" (flatten) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((remove_enumerable application-judgement "(enumerable?)"
     integer_enumerations nil)
    (remove const-decl "set" sets nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (restrict const-decl "R" restrict nil)
    (<= const-decl "bool" reals nil)
    (member const-decl "bool" sets nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (enum def-decl "T" integer_enumerations nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil))
(enum_surjective_lem 0
  (enum_surjective_lem-1 nil 3314638136
   ("" (induct "c" :name "NAT_induction")
    (("" (skosimp*)
      (("" (invoke (case "i!1 = %1") (! -2 r r))
        (("1" (inst + "0")
          (("1" (expand "enum") (("1" (propax) nil nil)) nil)) nil)
         ("2" (use "remove_least")
          (("2" (use "infinite_nonempty")
            (("2" (assert)
              (("2" (hide -1)
                (("2"
                  (inst -
                   "i!1 - least[T](restrict[[real, real], [T, T], boolean](<=))(remove(least[T](restrict[[real, real], [T, T], boolean](<=))(S!1), S!1))")
                  (("1" (assert)
                    (("1" (invoke (inst - "%1" "i!1") (! -1 r 1))
                      (("1" (skolem!)
                        (("1" (inst + "n!1 + 1")
                          (("1" (expand "enum" +)
                            (("1" (propax) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (expand* "remove" "member") nil nil))
                      nil))
                    nil)
                   ("2" (lemma "least_le")
                    (("2"
                      (inst -
                       "restrict[[real, real], [T, T], boolean](<=)"
                       "remove[T](least[T](restrict[[real, real], [T, T], boolean](<=))(S!1), S!1)"
                       "i!1")
                      (("1" (expand "restrict")
                        (("1" (assert) nil nil)) nil)
                       ("2" (expand* "remove" "member") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((remove_least formula-decl nil bounded_integers nil)
    (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (S!1 skolem-const-decl "(enumerable?)" integer_enumerations nil)
    (i!1 skolem-const-decl "(S!1)" integer_enumerations nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (member const-decl "bool" sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (least_le formula-decl nil minmax_orders nil)
    (remove_enumerable application-judgement "(enumerable?)"
     integer_enumerations nil)
    (remove const-decl "set" sets nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (infinite_nonempty judgement-tcc nil infinite_sets_def nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     restrict_order_props nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     restrict_order_props nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     restrict_order_props nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     restrict_order_props nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     restrict_order_props nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     restrict_order_props nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     restrict_order_props nil)
    (NAT_induction formula-decl nil naturalnumbers nil)
    (enum def-decl "T" integer_enumerations nil)
    (<= const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(enum_surjective 0
  (enum_surjective-1 nil 3314638307
   ("" (skolem!)
    (("" (lemma "enum_surjective_lem")
      (("" (inst? -)
        ((""
          (inst -
           "i!1 - least(restrict[[real, real], [T, T], boolean](<=))(S!1)")
          (("" (use "least_le")
            (("" (expand "restrict" -1 1) (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((enum_surjective_lem formula-decl nil integer_enumerations nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (<= const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (i!1 skolem-const-decl "(S!1)" integer_enumerations nil)
    (S!1 skolem-const-decl "(enumerable?)" integer_enumerations nil)
    (least_le formula-decl nil minmax_orders nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(enum_def 0
  (enum_def-1 nil 3314638361
   ("" (skolem-typepred)
    (("" (decompose-equality)
      (("" (iff)
        (("" (expand "image")
          (("" (prop)
            (("1" (skolem!)
              (("1" (replace -1 :hide? t)
                (("1" (rewrite "enum_member") nil nil)) nil))
              nil)
             ("2" (use "enum_surjective")
              (("2" (skolem!)
                (("2" (inst?)
                  (("2" (expand "fullset") (("2" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (image const-decl "set[R]" function_image nil)
    (enum def-decl "T" integer_enumerations nil)
    (fullset const-decl "set" sets nil)
    (enum_surjective formula-decl nil integer_enumerations nil)
    (x!1 skolem-const-decl "T" integer_enumerations nil)
    (S!1 skolem-const-decl "(enumerable?)" integer_enumerations nil)
    (n!1 skolem-const-decl "nat" integer_enumerations nil)
    (enum_member judgement-tcc nil integer_enumerations nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations 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))
   shostak))
(enum_subset_monotone 0
  (enum_subset_monotone-1 nil 3314638436
   ("" (induct "n")
    (("1" (skosimp)
      (("1" (expand "enum")
        (("1" (lemma "least_monotone")
          (("1" (invoke (inst - "%1" _ _) (! 1 l 0 1))
            (("1" (inst?)
              (("1" (expand "restrict" -1 1) (("1" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "enum" +)
        (("2" (inst?)
          (("2" (prop)
            (("2" (rewrite "remove_least_monotone") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((remove_enumerable application-judgement "(enumerable?)"
     integer_enumerations nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (remove const-decl "set" sets nil)
    (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
     nil)
    (remove_least_monotone formula-decl nil bounded_integers nil)
    (least_monotone formula-decl nil minmax_orders nil)
    (has_least? const-decl "bool" minmax_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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (restrict const-decl "R" restrict nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (enum def-decl "T" integer_enumerations nil)
    (<= const-decl "bool" reals nil)
    (subset? const-decl "bool" sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak))
(enum_strictly_ascending 0
  (enum_strictly_ascending-1 nil 3314638518
   ("" (induct "n")
    (("1" (skolem!)
      (("1" (expand* "enum" "enum")
        (("1" (rewrite "remove_least")
          (("1" (use "infinite_nonempty") nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "enum" +)
        (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (enum_member application-judgement "(S)" integer_enumerations nil)
    (non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
     nil)
    (remove_least formula-decl nil bounded_integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (remove_enumerable application-judgement "(enumerable?)"
     integer_enumerations nil)
    (infinite_nonempty judgement-tcc nil infinite_sets_def nil)
    (<= const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (remove const-decl "set" sets nil)
    (infinite_set type-eq-decl nil infinite_sets_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (enum def-decl "T" integer_enumerations nil)
    (< const-decl "bool" reals nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   shostak))
(enum_strictly_monotone 0
  (enum_strictly_monotone-1 nil 3314637789
   ("" (expand "strictly_monotone?")
    (("" (skosimp*)
      (("" (generalize-skolem-constants)
        (("" (induct "n_1" :name "NAT_induction")
          (("" (skosimp*)
            (("" (inst - "j!1 - 1")
              (("1" (assert)
                (("1" (inst?)
                  (("1" (lemma "enum_strictly_ascending")
                    (("1" (inst - _ "j!1 - 1")
                      (("1" (inst?) (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pred type-eq-decl nil defined_types nil)
    (NAT_induction formula-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (j!1 skolem-const-decl "nat" integer_enumerations nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (enum_strictly_ascending formula-decl nil integer_enumerations nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (enum_member application-judgement "(S)" integer_enumerations nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (enum def-decl "T" integer_enumerations nil)
    (strictly_monotone? const-decl "bool" integer_enumerations nil))
   nil))
(enumerable 0
  (enumerable-1 nil 3314638662
   ("" (skolem!)
    (("" (inst + "enum(S!1)") (("" (rewrite "enum_def") nil nil)) nil))
    nil)
   ((enum_strictly_monotone application-judgement
     "(strictly_monotone?)" integer_enumerations 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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (strictly_monotone? const-decl "bool" integer_enumerations nil)
    (set type-eq-decl nil sets nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (enum def-decl "T" integer_enumerations nil)
    (enum_def formula-decl nil integer_enumerations nil))
   shostak))
(enum_bijective 0
  (enum_bijective-1 nil 3316977910
   ("" (skolem!)
    (("" (expand* "bijective?" "injective?" "surjective?")
      (("" (split)
        (("1" (skosimp)
          (("1" (use "enum_strictly_monotone")
            (("1" (expand "strictly_monotone?")
              (("1" (inst-cp - "x2!1" "x1!1")
                (("1" (inst - "x1!1" "x2!1") (("1" (ground) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (use "enum_surjective")
            (("2" (skolem!)
              (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (enum_strictly_monotone application-judgement
     "(strictly_monotone?)" integer_enumerations nil)
    (bijective? const-decl "bool" functions nil)
    (enum_surjective formula-decl nil integer_enumerations nil)
    (strictly_monotone? const-decl "bool" integer_enumerations nil)
    (enum_member application-judgement "(S)" integer_enumerations nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (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)
    (T_pred const-decl "[int -> boolean]" integer_enumerations nil)
    (T formal-subtype-decl nil integer_enumerations nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (enumerable? const-decl "bool" integer_enumerations nil)
    (enum_strictly_monotone judgement-tcc nil integer_enumerations
     nil))
   shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.