Quelle ordered_int.prf Sprache: Lisp

(ordered_int
(upto_has_greatest 0
  (upto_has_greatest-1 nil 3316216593
   ("" (skolem!)
    ((""
      (expand* "restrict" "has_greatest?" "greatest?" "upto"
       "reflexive_closure" "union" "member" "upper_bound?")
      (("" (inst + "i!1") (("" (reduce) nil nil)) nil)) nil))
    nil)
   ((has_greatest? const-decl "bool" minmax_orders nil)
    (upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
     nil)
    (union const-decl "set" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (greatest? const-decl "bool" minmax_orders nil)
    (restrict const-decl "R" restrict nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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))
(below_has_greatest 0
  (below_has_greatest-1 nil 3316216593
   ("" (skolem!)
    ((""
      (expand* "restrict" "has_greatest?" "greatest?" "below"
       "irreflexive_kernel" "difference" "member" "upper_bound?")
      (("" (inst + "i!1 - 1") (("" (reduce) nil nil)) nil)) nil))
    nil)
   ((has_greatest? const-decl "bool" minmax_orders nil)
    (below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
     nil)
    (difference const-decl "set" sets nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (greatest? const-decl "bool" minmax_orders nil)
    (restrict const-decl "R" restrict nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(above_has_least 0
  (above_has_least-1 nil 3316216593
   ("" (skolem!)
    ((""
      (expand* "restrict" "has_least?" "least?" "above"
       "irreflexive_kernel" "difference" "member" "lower_bound?")
      (("" (inst + "i!1 + 1") (("" (reduce) nil nil)) nil)) nil))
    nil)
   ((has_least? const-decl "bool" minmax_orders nil)
    (above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
     nil)
    (difference const-decl "set" sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (least? const-decl "bool" minmax_orders nil)
    (restrict const-decl "R" restrict nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil))
(upfrom_has_least 0
  (upfrom_has_least-1 nil 3316216593
   ("" (skolem!)
    ((""
      (expand* "restrict" "has_least?" "least?" "upfrom"
       "reflexive_closure" "union" "member" "lower_bound?")
      (("" (inst + "i!1") (("" (reduce) nil nil)) nil)) nil))
    nil)
   ((has_least? const-decl "bool" minmax_orders nil)
    (upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
     nil)
    (union const-decl "set" sets nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (least? const-decl "bool" minmax_orders nil)
    (restrict const-decl "R" restrict nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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))
(prefix_empty 0
  (prefix_empty-1 nil 3316217027
   ("" (skosimp :preds? t)
    (("" (expand* "prefix?" "member" "restrict")
      (("" (assert)
        (("" (lemma "non_empty_finite_has_least")
          (("" (inst - "pre!1" "<=")
            ((""
              (expand* "restrict" "has_least?" "least?" "lower_bound?")
              (("" (skosimp)
                (("" (inst - "t!1 - 1" "t!1")
                  (("" (assert)
                    (("" (inst - "t!1 - 1") (("" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (non_empty_finite_has_least formula-decl nil minmax_orders nil)
    (has_least? const-decl "bool" minmax_orders nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (least? const-decl "bool" minmax_orders nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (pre!1 skolem-const-decl "(LAMBDA (S: set[int]):
   prefix?(S, restrict[[real, real], [int, int], boolean](<=)))"
     ordered_int nil)
    (t!1 skolem-const-decl "int" ordered_int nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (total_order? const-decl "bool" orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     ordered_int nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     ordered_int nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     ordered_int nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     ordered_int nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     ordered_int nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     ordered_int nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     ordered_int 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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (prefix? const-decl "bool" ordered_subset nil)
    (restrict const-decl "R" restrict nil)
    (<= const-decl "bool" reals nil))
   shostak))
(prefix_below 0
  (prefix_below-1 nil 3316217271
   ("" (skosimp :preds? t)
    ((""
      (case "has_greatest?[int](pre!1, restrict[[real, real], [int, int], boolean](<=))")
      (("1"
        (inst +
         "greatest[int](restrict[[real, real], [int, int], boolean](<=))(pre!1) + 1")
        (("1" (apply-extensionality 3 :hide? t)
          (("1"
            (expand* "prefix?" "below" "irreflexive_kernel"
             "difference" "member")
            (("1"
              (typepred
               "greatest[int](restrict[[real, real], [int, int], boolean](<=))(pre!1)")
              (("1" (expand "greatest?")
                (("1" (flatten)
                  (("1"
                    (inst - "x!1"
                     "greatest[int](restrict[[real, real], [int, int], boolean](<=))(pre!1)")
                    (("1" (expand* "restrict" "upper_bound?")
                      (("1" (inst - "x!1")
                        (("1" (assert) nil nil) ("2" (smash) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2"
        (expand* "has_greatest?" "greatest?" "upper_bound?" "full?"
         "empty?" "member" "restrict")
        (("2" (skosimp*)
          (("2"
            (case "x!1 < x!2 AND has_greatest?({i: int | pre!1(i) AND x!1 <=i AND i <= x!2}, restrict[[real, real], [int, int], boolean](<=))")
            (("1" (flatten)
              (("1"
                (inst +
                 "greatest(restrict[[real, real], [int, int], boolean](<=))({i: int | pre!1(i) AND x!1 <= i AND i <= x!2})")
                (("1" (assert)
                  (("1"
                    (typepred
                     "greatest(restrict[[real, real], [int, int], boolean](<=))({i: int | pre!1(i) AND x!1 <= i AND i <= x!2})")
                    (("1" (expand* "greatest?" "upper_bound?")
                      (("1" (flatten)
                        (("1" (expand "restrict" -4 :occurrence 1)
                          (("1" (assert)
                            (("1" (skolem!)
                              (("1"
                                (inst - "r!1")
                                (("1"
                                  (expand* "prefix?" "member")
                                  (("1"
                                    (inst - "x!2" "r!1")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand* "prefix?" "member")
              (("2" (inst - "x!2" "x!1")
                (("2" (assert)
                  (("2" (assert)
                    (("2" (lemma "non_empty_finite_has_greatest")
                      (("2"
                        (inst -
                         "{i: int | pre!1(i) AND x!1 <= i AND i <= x!2}"
                         "restrict[[real, real], [int, int], boolean](<=)")
                        (("2" (split)
                          (("1" (expand "is_finite")
                            (("1"
                              (inst + "x!2 - x!1 + 1"
                               "LAMBDA (x: ({i: int | pre!1(i) AND x!1 <= i AND i <= x!2})): x - x!1")
                              (("1"
                                (expand "injective?")
                                (("1" (skosimp) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand* "empty?" "member")
                            (("2" (inst - "x!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((has_greatest? const-decl "bool" minmax_orders nil)
    (order? const-decl "bool" relations_extra nil)
    (below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
     nil)
    (x!1 skolem-const-decl "int" ordered_int nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (difference const-decl "set" sets nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (greatest? const-decl "bool" minmax_orders nil)
    (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
     nil)
    (pre!1 skolem-const-decl "(LAMBDA (S: set[int]):
   prefix?(S, restrict[[real, real], [int, int], boolean](<=)))"
     ordered_int nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     ordered_int nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     ordered_int nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     ordered_int nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     ordered_int nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     ordered_int nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     ordered_int nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     ordered_int nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (non_empty_finite_has_greatest formula-decl nil minmax_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (below type-eq-decl nil nat_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (total_order? const-decl "bool" orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (r!1 skolem-const-decl "(pre!1)" ordered_int nil)
    (x!2 skolem-const-decl "int" ordered_int nil)
    (x!1 skolem-const-decl "int" ordered_int nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (full? const-decl "bool" sets 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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (prefix? const-decl "bool" ordered_subset nil)
    (restrict const-decl "R" restrict nil)
    (<= const-decl "bool" reals nil))
   shostak))
(prefix_upto 0
  (prefix_upto-1 nil 3316218283
   ("" (skosimp)
    (("" (use "prefix_below")
      (("" (assert)
        (("" (skolem!)
          (("" (inst + "i!1 - 1")
            (("" (hide 1 2) (("" (grind-with-ext) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((prefix_below formula-decl nil ordered_int nil)
    (<= const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (prefix? const-decl "bool" ordered_subset nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets 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)
    (upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
     nil)
    (below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
     nil)
    (order? const-decl "bool" relations_extra nil)
    (union const-decl "set" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (difference const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (linear_order_to_strict_total_order application-judgement
     "(strict_total_order?)" ordered_int nil)
    (linear_order_to_total_order application-judgement "(total_order?)"
     ordered_int nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     ordered_int nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     ordered_int nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     ordered_int nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     ordered_int nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     ordered_int nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     ordered_int nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     ordered_int nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
(suffix_empty 0
  (suffix_empty-1 nil 3316218333
   ("" (skosimp :preds? t)
    (("" (expand* "suffix?" "member" "restrict")
      (("" (assert)
        (("" (lemma "non_empty_finite_has_greatest")
          (("" (inst - "suf!1" "<=")
            ((""
              (expand* "restrict" "has_greatest?" "greatest?"
               "upper_bound?")
              (("" (skosimp)
                (("" (inst - "t!1 + 1" "t!1")
                  (("" (assert)
                    (("" (inst - "1 + t!1") (("" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (non_empty_finite_has_greatest formula-decl nil minmax_orders nil)
    (has_greatest? const-decl "bool" minmax_orders nil)
    (upper_bound? const-decl "bool" bounded_orders nil)
    (greatest? const-decl "bool" minmax_orders nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (suf!1 skolem-const-decl "(LAMBDA (S: set[int]):
   suffix?(S, restrict[[real, real], [int, int], boolean](<=)))"
     ordered_int nil)
    (t!1 skolem-const-decl "int" ordered_int nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (total_order? const-decl "bool" orders nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     ordered_int nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     ordered_int nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     ordered_int nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     ordered_int nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     ordered_int nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     ordered_int nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     ordered_int 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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (suffix? const-decl "bool" ordered_subset nil)
    (restrict const-decl "R" restrict nil)
    (<= const-decl "bool" reals nil))
   shostak))
(suffix_upfrom 0
  (suffix_upfrom-1 nil 3316218425
   ("" (skosimp :preds? t)
    ((""
      (case "has_least?[int](suf!1, restrict[[real, real], [int, int], boolean](<=))")
      (("1"
        (inst +
         "least[int](restrict[[real, real], [int, int], boolean](<=))(suf!1)")
        (("1" (apply-extensionality 3 :hide? t)
          (("1"
            (expand* "suffix?" "upfrom" "reflexive_closure" "union"
             "member")
            (("1"
              (typepred
               "least[int](restrict[[real, real], [int, int], boolean](<=))(suf!1)")
              (("1" (expand "least?")
                (("1" (flatten)
                  (("1"
                    (inst - "x!1"
                     "least[int](restrict[[real, real], [int, int], boolean](<=))(suf!1)")
                    (("1" (expand* "restrict" "lower_bound?")
                      (("1" (inst - "x!1")
                        (("1" (assert) nil nil) ("2" (smash) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2"
        (expand* "has_least?" "least?" "lower_bound?" "full?" "empty?"
         "member" "restrict")
        (("2" (skosimp*)
          (("2"
            (case "x!2 < x!1 AND has_least?({i: int | suf!1(i) AND x!2 <=i AND i <= x!1}, restrict[[real, real], [int, int], boolean](<=))")
            (("1" (flatten)
              (("1"
                (inst +
                 "least[int](restrict[[real, real], [int, int], boolean](<=))({i: int | suf!1(i) AND x!2 <= i AND i <= x!1})")
                (("1" (assert)
                  (("1"
                    (typepred
                     "least[int](restrict[[real, real], [int, int], boolean](<=))({i: int | suf!1(i) AND x!2 <= i AND i <= x!1})")
                    (("1" (expand* "least?" "lower_bound?")
                      (("1" (flatten)
                        (("1" (expand "restrict" -4 :occurrence 1)
                          (("1" (assert)
                            (("1" (skolem!)
                              (("1"
                                (inst - "r!1")
                                (("1"
                                  (expand* "suffix?" "member")
                                  (("1"
                                    (inst - "x!2" "r!1")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand* "suffix?" "member")
              (("2" (inst - "x!2" "x!1")
                (("2" (assert)
                  (("2" (assert)
                    (("2" (lemma "non_empty_finite_has_least")
                      (("2"
                        (inst -
                         "{i: int | suf!1(i) AND x!2 <= i AND i <= x!1}"
                         "restrict[[real, real], [int, int], boolean](<=)")
                        (("2" (split)
                          (("1" (expand "is_finite")
                            (("1"
                              (inst + "x!1 - x!2 + 1"
                               "LAMBDA (x: ({i: int | suf!1(i) AND x!2 <= i AND i <= x!1})): x - x!2")
                              (("1"
                                (expand "injective?")
                                (("1" (skosimp) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand* "empty?" "member")
                            (("2" (inst - "x!1")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((has_least? const-decl "bool" minmax_orders nil)
    (order? const-decl "bool" relations_extra nil)
    (upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
     nil)
    (x!1 skolem-const-decl "int" ordered_int nil)
    (lower_bound? const-decl "bool" bounded_orders nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (least? const-decl "bool" minmax_orders nil)
    (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
    (suf!1 skolem-const-decl "(LAMBDA (S: set[int]):
   suffix?(S, restrict[[real, real], [int, int], boolean](<=)))"
     ordered_int nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     ordered_int nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     ordered_int nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     ordered_int nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     ordered_int nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     ordered_int nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     ordered_int nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     ordered_int nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (non_empty_finite_has_least formula-decl nil minmax_orders nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (below type-eq-decl nil nat_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (total_order? const-decl "bool" orders nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (r!1 skolem-const-decl "(suf!1)" ordered_int nil)
    (x!1 skolem-const-decl "int" ordered_int nil)
    (x!2 skolem-const-decl "int" ordered_int nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (full? const-decl "bool" sets 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)
    (set type-eq-decl nil sets nil)
    (pred type-eq-decl nil defined_types nil)
    (suffix? const-decl "bool" ordered_subset nil)
    (restrict const-decl "R" restrict nil)
    (<= const-decl "bool" reals nil))
   shostak))
(suffix_above 0
  (suffix_above-1 nil 3316218852
   ("" (skosimp)
    (("" (use "suffix_upfrom")
      (("" (assert)
        (("" (skolem!)
          (("" (inst + "i!1 - 1")
            (("" (hide 1 2) (("" (grind-with-ext) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((suffix_upfrom formula-decl nil ordered_int nil)
    (<= const-decl "bool" reals nil)
    (restrict const-decl "R" restrict nil)
    (suffix? const-decl "bool" ordered_subset nil)
    (pred type-eq-decl nil defined_types nil)
    (set type-eq-decl nil sets 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)
    (above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
     nil)
    (upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
     nil)
    (order? const-decl "bool" relations_extra nil)
    (difference const-decl "set" sets nil)
    (irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (reflexive_closure const-decl "(reflexive?)" closure_ops nil)
    (linear_order_to_total_order application-judgement "(total_order?)"
     ordered_int nil)
    (linear_order_to_strict_total_order application-judgement
     "(strict_total_order?)" ordered_int nil)
    (reflexive_restrict application-judgement "(reflexive?[S])"
     ordered_int nil)
    (antisymmetric_restrict application-judgement "(antisymmetric?[S])"
     ordered_int nil)
    (transitive_restrict application-judgement "(transitive?[S])"
     ordered_int nil)
    (preorder_restrict application-judgement "(preorder?[S])"
     ordered_int nil)
    (partial_order_restrict application-judgement "(partial_order?[S])"
     ordered_int nil)
    (dichotomous_restrict application-judgement "(dichotomous?[S])"
     ordered_int nil)
    (total_order_restrict application-judgement "(total_order?[S])"
     ordered_int nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
(unrelated_empty 0
  (unrelated_empty-1 nil 3316218921 ("" (grind) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (restrict const-decl "R" restrict 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)
    (unrelated const-decl "set[T]" ordered_subset nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil))
   shostak)))

quality93%

¤ 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.0.6Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

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.