|
(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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.60Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
