Quelle range.prf Sprache: Lisp

(range (range_TCC1 0
        (range_TCC1-1 nil 3318610662
         ("" (inst + "{r | 0 <= r AND r <= 1}")
          (("" (existence-tcc) nil nil)) nil)
         ((real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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))
       (min_range_TCC1 0
        (min_range_TCC1-1 nil 3318610662
         ("" (inst + "{t: T | t = epsilon! (x: T): TRUE}")
          (("" (existence-tcc) nil nil)) nil)
         ((NOT const-decl "[bool -> bool]" booleans nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (TRUE const-decl "bool" booleans nil)
          (epsilon const-decl "T" epsilons nil)
          (= const-decl "[T, T -> boolean]" equalities nil)
          (restrict const-decl "R" restrict nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (pred type-eq-decl nil defined_types nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (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))
         nil))
       (max_range_TCC1 0
        (max_range_TCC1-1 nil 3318610662
         ("" (inst + "{t: T | t = epsilon! (x: T): TRUE}")
          (("" (existence-tcc) nil nil)) nil)
         ((NOT const-decl "[bool -> bool]" booleans nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (TRUE const-decl "bool" booleans nil)
          (epsilon const-decl "T" epsilons nil)
          (= const-decl "[T, T -> boolean]" equalities nil)
          (restrict const-decl "R" restrict nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (pred type-eq-decl nil defined_types nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (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))
         nil))
       (c_range_TCC1 0
        (c_range_TCC1-1 nil 3318610662
         ("" (inst + "{t: T | t = epsilon! (x: T): TRUE}")
          (("" (existence-tcc) nil nil)) nil)
         ((NOT const-decl "[bool -> bool]" booleans nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (TRUE const-decl "bool" booleans nil)
          (epsilon const-decl "T" epsilons nil)
          (= const-decl "[T, T -> boolean]" equalities nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (pred type-eq-decl nil defined_types nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (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))
         nil))
       (o_range_TCC1 0
        (o_range_TCC1-1 nil 3318610662
         ("" (inst + "emptyset[T]") (("" (existence-tcc) nil nil)) nil)
         ((greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (emptyset const-decl "set" sets nil)
          (has_non_greatest? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (restrict const-decl "R" restrict nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (pred type-eq-decl nil defined_types nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (OR const-decl "[bool, bool -> bool]" booleans nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (finite_emptyset name-judgement "finite_set" finite_sets nil)
          (finite_emptyset name-judgement "finite_set[T]" range 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))
         nil))
       (c_range_is_nonempty 0
        (c_range_is_nonempty-1 nil 3318610662
         ("" (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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (set type-eq-decl nil sets nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (<= const-decl "bool" reals nil)
          (range nonempty-type-eq-decl nil range nil)
          (pred type-eq-decl nil defined_types nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (member const-decl "bool" sets nil)
          (empty? const-decl "bool" sets nil)
          (nonempty? const-decl "bool" sets nil))
         nil))
       (oc_range_is_nonempty 0
        (oc_range_is_nonempty-1 nil 3318610662
         ("" (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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (set type-eq-decl nil sets nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (<= const-decl "bool" reals nil)
          (range nonempty-type-eq-decl nil range nil)
          (OR const-decl "[bool, bool -> bool]" booleans nil)
          (pred type-eq-decl nil defined_types nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_non_least? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (oc_range type-eq-decl nil range nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders 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)
          (member const-decl "bool" sets nil)
          (empty? const-decl "bool" sets nil)
          (nonempty? const-decl "bool" sets nil))
         nil))
       (co_range_is_nonempty 0
        (co_range_is_nonempty-1 nil 3318610662
         ("" (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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (set type-eq-decl nil sets nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (<= const-decl "bool" reals nil)
          (range nonempty-type-eq-decl nil range nil)
          (pred type-eq-decl nil defined_types nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (OR const-decl "[bool, bool -> bool]" booleans nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (has_non_greatest? const-decl "bool" range nil)
          (co_range type-eq-decl nil range nil)
          (x!1 skolem-const-decl "co_range" range nil)
          (r!1 skolem-const-decl "T" range nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (member const-decl "bool" sets nil)
          (empty? const-decl "bool" sets nil)
          (nonempty? const-decl "bool" sets nil))
         nil))
       (closed_range_TCC1 0
        (closed_range_TCC1-1 nil 3318610662
         ("" (grind :if-match all) nil nil)
         ((<= const-decl "bool" reals nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (member const-decl "bool" sets nil)
          (restrict const-decl "R" restrict nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (has_greatest? const-decl "bool" minmax_orders nil))
         nil))
       (nontrivial_closed_range_TCC1 0
        (nontrivial_closed_range_TCC1-1 nil 3318610662
         ("" (grind :if-match all)
          ((""
            (typepred "least(lesseq)({r | r1!1 <= r AND r <= r2!1})")
            (("1"
              (typepred
               "greatest(lesseq)({r | r1!1 <= r AND r <= r2!1})")
              (("1"
                (expand* "greatest?" "upper_bound?" "least?"
                 "lower_bound?")
                (("1" (expand "restrict" -4 :occurrence 1)
                  (("1" (expand "restrict" -8 :occurrence 1)
                    (("1" (inst - "r2!1")
                      (("1" (inst - "r1!1") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (inst + "r2!1") (("2" (assert) nil nil)) nil))
              nil)
             ("2" (inst + "r1!1") (("2" (assert) nil nil)) nil))
            nil))
          nil)
         ((pred type-eq-decl nil defined_types nil)
          (set type-eq-decl nil sets nil)
          (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders
           nil)
          (greatest const-decl "{t: (S) | greatest?(t, S, <=)}"
           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)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (< const-decl "bool" reals nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (open_closed_range_TCC1 0
        (open_closed_range_TCC1-1 nil 3318610662
         ("" (grind :if-match nil)
          (("1" (inst + "r2!1") (("1" (assert) nil nil)) nil)
           ("2" (inst + "r1!1")
            (("2" (assert :quant-simp? t)
              (("2" (skosimp)
                (("2" (inst-cp -8 "r2!1")
                  (("2" (inst -8 "t!1")
                    (("2" (assert)
                      (("2" (inst - "r1!2") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (< const-decl "bool" reals nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (closed_open_range_TCC1 0
        (closed_open_range_TCC1-1 nil 3318610662
         ("" (grind :if-match nil)
          (("1" (inst + "r2!1")
            (("1" (assert :quant-simp? t)
              (("1" (skosimp)
                (("1" (inst-cp -8 "r1!1")
                  (("1" (assert)
                    (("1" (inst -8 "r1!2") (("1" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (inst + "r1!1") (("2" (assert) nil nil)) nil))
          nil)
         ((<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (< const-decl "bool" reals nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (has_non_greatest? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (open_range_TCC1 0
        (open_range_TCC1-1 nil 3318610662
         ("" (grind :if-match nil)
          (("1" (inst + "r2!1")
            (("1" (assert :quant-simp? t)
              (("1" (skosimp)
                (("1" (inst-cp -7 "t!1")
                  (("1" (assert)
                    (("1" (inst -7 "r1!2") (("1" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (inst + "r1!1")
            (("2" (assert :quant-simp? t)
              (("2" (skosimp)
                (("2" (inst-cp -7 "t!1")
                  (("2" (assert)
                    (("2" (inst -7 "r1!2") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((< const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (has_non_greatest? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (nontrivial_open_range_TCC1 0
        (nontrivial_open_range_TCC1-1 nil 3318610662
         ("" (grind :if-match nil)
          (("1" (inst - "t!1") (("1" (assert) nil nil)) nil)
           ("2" (inst + "r2!1")
            (("2" (assert :quant-simp? t)
              (("2" (skosimp)
                (("2" (inst-cp -10 "t!1")
                  (("2" (assert)
                    (("2" (inst -10 "r1!2") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (inst + "r1!1")
            (("3" (assert :quant-simp? t)
              (("3" (skosimp)
                (("3" (inst-cp -10 "t!1")
                  (("3" (assert)
                    (("3" (inst -10 "r1!2") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (< const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (nonempty? const-decl "bool" sets nil)
          (empty? const-decl "bool" sets nil)
          (has_non_greatest? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (open_closed_range_TCC2 0
        (open_closed_range_TCC2-1 nil 3318610662
         ("" (subtype-tcc) nil nil)
         ((no_least const-decl "bool" range nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (<= const-decl "bool" reals 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)
          (member const-decl "bool" sets nil)
          (restrict const-decl "R" restrict nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (has_greatest? const-decl "bool" minmax_orders nil))
         nil))
       (closed_open_range_TCC2 0
        (closed_open_range_TCC2-1 nil 3318610662
         ("" (subtype-tcc) nil nil)
         ((no_greatest const-decl "bool" range nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (<= const-decl "bool" reals 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)
          (member const-decl "bool" sets nil)
          (restrict const-decl "R" restrict nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (has_non_greatest? const-decl "bool" range nil))
         nil))
       (left_open_range_TCC1 0
        (left_open_range_TCC1-1 nil 3318610662
         ("" (grind :if-match nil)
          (("1" (inst + "r!1")
            (("1" (assert)
              (("1" (skolem-typepred)
                (("1" (inst - "r!2") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (inst 2 "r!1")
            (("2" (assert :quant-simp? t)
              (("2" (skosimp)
                (("2" (assert)
                  (("2" (inst -5 "r1!1") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (inst + "t!1")
            (("3" (assert)
              (("3" (skolem-typepred)
                (("3" (inst - "r!2") (("3" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ((r!2 skolem-const-decl "({r | r <= r!1})" range nil)
          (r!1 skolem-const-decl "(no_least)" range nil)
          (<= const-decl "bool" reals nil)
          (< const-decl "bool" reals 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)
          (no_least const-decl "bool" range nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (nonempty? const-decl "bool" sets nil)
          (empty? const-decl "bool" sets nil)
          (has_non_greatest? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (right_open_range_TCC1 0
        (right_open_range_TCC1-1 nil 3318610662
         ("" (grind :if-match nil)
          (("1" (inst + "r!1")
            (("1" (assert)
              (("1" (skolem-typepred)
                (("1" (inst - "r!2") (("1" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (inst + "t!1")
            (("2" (assert)
              (("2" (skolem-typepred)
                (("2" (inst - "r!2") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("3" (inst 2 "r!1")
            (("3" (assert :quant-simp? t)
              (("3" (skosimp)
                (("3" (assert)
                  (("3" (inst -5 "r1!1") (("3" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((r!2 skolem-const-decl "({r | r!1 <= r})" range nil)
          (r!1 skolem-const-decl "(no_greatest)" range nil)
          (<= const-decl "bool" reals nil)
          (< const-decl "bool" reals 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)
          (no_greatest const-decl "bool" range nil)
          (NOT const-decl "[bool -> bool]" booleans nil)
          (bool nonempty-type-eq-decl nil booleans nil)
          (nonempty? const-decl "bool" sets nil)
          (empty? const-decl "bool" sets nil)
          (has_non_greatest? const-decl "bool" range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (has_non_least? const-decl "bool" range nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (restrict const-decl "R" restrict nil)
          (member const-decl "bool" sets nil))
         nil))
       (c_range_construction 0
        (c_range_construction-1 nil 3318611493
         ("" (skolem-typepred)
          ((""
            (expand* "has_least?" "least?" "lower_bound?"
             "has_greatest?" "greatest?" "upper_bound?" "restrict"
             "member")
            (("" (skosimp*)
              (("" (inst-cp - "t!2")
                (("" (inst + "t!1" "t!2")
                  (("" (apply-extensionality :hide? t)
                    (("" (expand "closed_range")
                      (("" (inst - "t!1" "t!2" "x!1")
                        (("" (smash)
                          (("1" (inst -6 "x!1") nil nil)
                           ("2" (inst - "x!1") nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((least? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (R!1 skolem-const-decl "c_range" range nil)
          (t!2 skolem-const-decl "T" range nil)
          (closed_range const-decl "c_range" range nil)
          (t!1 skolem-const-decl "T" range nil)
          (real_le_is_total_order name-judgement "(total_order?[real])"
           real_props nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (pred type-eq-decl nil defined_types nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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))
       (ntc_range_construction 0
        (ntc_range_construction-1 nil 3318611591
         ("" (skolem-typepred)
          ((""
            (expand* "has_least?" "least?" "lower_bound?"
             "has_greatest?" "greatest?" "upper_bound?" "member")
            (("" (expand "restrict" (-2 -3))
              (("" (skosimp*)
                (("" (inst + "t!1" "t!2")
                  (("1" (apply-extensionality :hide? t)
                    (("1" (expand "nontrivial_closed_range")
                      (("1" (iff)
                        (("1" (ground)
                          (("1" (inst -4 "x!1") nil nil)
                           ("2" (inst -6 "x!1") nil nil)
                           ("3" (inst - "t!1" "t!2" "x!1")
                            (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (inst - "least(lesseq)(R!1)")
                    (("2" (inst - "greatest(lesseq)(R!1)")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((upper_bound? const-decl "bool" bounded_orders nil)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (nontrivial_closed_range const-decl "ntc_range" range 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)
          (t!2 skolem-const-decl "T" range nil)
          (t!1 skolem-const-decl "T" range nil)
          (real_lt_is_strict_total_order name-judgement
           "(strict_total_order?[real])" real_props nil)
          (ntc_range type-eq-decl nil range nil)
          (greatest const-decl "{t: (S) | greatest?(t, S, <=)}"
           minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders
           nil)
          (least? const-decl "bool" minmax_orders nil)
          (< const-decl "bool" reals nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (pred type-eq-decl nil defined_types nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (<= const-decl "bool" reals nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (set type-eq-decl nil sets nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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))
       (c_range_endpoints 0
        (c_range_endpoints-1 nil 3318611692
         ("" (grind)
          (("" (typepred "least(lesseq)(R!1)")
            (("" (expand* "least?" "lower_bound?")
              (("" (expand "restrict" -3 :occurrence 1)
                (("" (inst - "greatest(lesseq)(R!1)") nil nil)) nil))
              nil))
            nil))
          nil)
         ((greatest const-decl "{t: (S) | greatest?(t, S, <=)}"
           minmax_orders nil)
          (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders
           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)
          (lower_bound? const-decl "bool" bounded_orders nil)
          (least? const-decl "bool" minmax_orders nil)
          (upper_bound? const-decl "bool" bounded_orders nil)
          (greatest? const-decl "bool" minmax_orders 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (set type-eq-decl nil sets nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (<= const-decl "bool" reals nil)
          (member const-decl "bool" sets nil)
          (range nonempty-type-eq-decl nil range nil)
          (pred type-eq-decl nil defined_types nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (c_range nonempty-type-eq-decl nil range nil))
         shostak))
       (ntc_range_endpoints 0
        (ntc_range_endpoints-1 nil 3318611749
         ("" (skolem-typepred) 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)
          (T_pred const-decl "[real -> boolean]" range nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (set type-eq-decl nil sets nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (<= const-decl "bool" reals nil)
          (member const-decl "bool" sets nil)
          (range nonempty-type-eq-decl nil range nil)
          (pred type-eq-decl nil defined_types nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (restrict const-decl "R" restrict nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (< const-decl "bool" reals nil)
          (least? const-decl "bool" minmax_orders nil)
          (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders
           nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (greatest const-decl "{t: (S) | greatest?(t, S, <=)}"
           minmax_orders nil)
          (ntc_range type-eq-decl nil range nil))
         shostak))
       (c_range_min 0
        (c_range_min-1 nil 3318611762
         ("" (skolem!)
          (("" (typepred "least(lesseq)(closed_range(r1!1, r2!1))")
            (("" (expand* "least?" "lower_bound?")
              (("" (expand "closed_range" -2 :occurrence 1)
                (("" (flatten)
                  (("" (expand "restrict" -4 :occurrence 1)
                    (("" (inst - "r1!1")
                      (("1" (assert) nil nil)
                       ("2" (expand "closed_range" 1)
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((closed_range const-decl "c_range" range nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
          (set type-eq-decl nil sets nil)
          (pred type-eq-decl nil defined_types nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (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)
          (r2!1 skolem-const-decl "{r | r1!1 <= r}" range nil)
          (r1!1 skolem-const-decl "T" range nil)
          (lower_bound? const-decl "bool" bounded_orders nil))
         shostak))
       (c_range_max 0
        (c_range_max-1 nil 3318611834
         ("" (skolem!)
          (("" (typepred "greatest(lesseq)(closed_range(r1!1, r2!1))")
            (("" (expand* "greatest?" "upper_bound?")
              (("" (expand "closed_range" -2 :occurrence 1)
                (("" (flatten)
                  (("" (expand "restrict" -4 :occurrence 1)
                    (("" (inst - "r2!1")
                      (("1" (assert) nil nil)
                       ("2" (expand "closed_range" 1)
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((closed_range const-decl "c_range" range nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (has_least? const-decl "bool" minmax_orders nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (<= const-decl "bool" reals nil)
          (restrict const-decl "R" restrict nil)
          (greatest const-decl "{t: (S) | greatest?(t, S, <=)}"
           minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (set type-eq-decl nil sets nil)
          (pred type-eq-decl nil defined_types nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (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)
          (r2!1 skolem-const-decl "{r | r1!1 <= r}" range nil)
          (r1!1 skolem-const-decl "T" range nil)
          (upper_bound? const-decl "bool" bounded_orders nil))
         shostak))
       (ntc_range_min 0
        (ntc_range_min-1 nil 3318611885
         ("" (skolem!)
          ((""
            (typepred
             "least(lesseq)(nontrivial_closed_range(r1!1, r2!1))")
            (("" (expand* "least?" "lower_bound?")
              (("" (expand "nontrivial_closed_range" -2 :occurrence 1)
                (("" (flatten)
                  (("" (expand "restrict" -4 :occurrence 1)
                    (("" (inst - "r1!1")
                      (("1" (assert) nil nil)
                       ("2" (expand "nontrivial_closed_range" 1)
                        (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ((nontrivial_closed_range const-decl "ntc_range" range nil)
          (ntc_range type-eq-decl nil range nil)
          (greatest const-decl "{t: (S) | greatest?(t, S, <=)}"
           minmax_orders nil)
          (greatest? const-decl "bool" minmax_orders nil)
          (c_range nonempty-type-eq-decl nil range nil)
          (has_greatest? const-decl "bool" minmax_orders nil)
          (range nonempty-type-eq-decl nil range nil)
          (member const-decl "bool" sets nil)
          (AND const-decl "[bool, bool -> bool]" booleans nil)
          (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
          (< const-decl "bool" reals 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)
          (set type-eq-decl nil sets nil)
          (pred type-eq-decl nil defined_types nil)
          (T formal-nonempty-subtype-decl nil range nil)
          (T_pred const-decl "[real -> boolean]" range 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)
          (reflexive_restrict application-judgement "(reflexive?[S])"
           restrict_order_props nil)
--> --------------------

--> maximum size reached

--> --------------------

quality97%

¤ Dauer der Verarbeitung: 0.32 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.