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