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