| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: chain.pvs Sprache: SMLOriginal von: PVS© |
|
||||||
|
(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 --> -------------------- ¤ Dauer der Verarbeitung: 1.113 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
