|
(ordered_nat
(upto_has_greatest 0
(upto_has_greatest-1 nil 3316219709
("" (skolem!)
((""
(expand* "restrict" "has_greatest?" "greatest?" "upto"
"reflexive_closure" "union" "member" "upper_bound?")
(("" (inst + "n!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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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))
(above_has_least 0
(above_has_least-1 nil 3316219709
("" (skolem!)
((""
(expand* "restrict" "has_least?" "least?" "above"
"irreflexive_kernel" "difference" "member" "lower_bound?")
(("" (inst + "n!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)
(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))
nil))
(upfrom_has_least 0
(upfrom_has_least-1 nil 3316219709
("" (skolem!)
((""
(expand* "restrict" "has_least?" "least?" "upfrom"
"reflexive_closure" "union" "member" "lower_bound?")
(("" (inst + "n!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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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))
(nonzero_below_greatest 0
(nonzero_below_greatest-1 nil 3316219881
("" (skosimp)
(("" (ground)
(("1"
(expand* "has_greatest?" "greatest?" "restrict" "below"
"irreflexive_kernel" "difference" "member" "upper_bound?")
(("1" (inst + "n!1 - 1") (("1" (reduce) nil nil)) nil)) nil)
("2" (rewrite "greatest_def")
(("2"
(expand* "restrict" "greatest?" "below" "irreflexive_kernel"
"difference" "member" "upper_bound?")
nil nil))
nil))
nil))
nil)
((reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(real_ge_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)
(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)
(has_greatest? const-decl "bool" minmax_orders nil)
(restrict const-decl "R" restrict nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(difference const-decl "set" sets nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(greatest? const-decl "bool" minmax_orders nil)
(prefix? const-decl "bool" ordered_subset nil)
(order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (<= const-decl "bool" reals nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(greatest_def formula-decl nil minmax_orders nil))
shostak))
(upto_greatest 0
(upto_greatest-1 nil 3316220279
("" (grind :rewrites ("greatest_def" "greatest?")) nil nil)
((total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(restrict const-decl "R" restrict nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops 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)
(linear_order_to_total_order application-judgement "(total_order?)"
ordered_nat 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)
(greatest_def formula-decl nil minmax_orders nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(prefix? const-decl "bool" ordered_subset nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(above_least 0
(above_least-1 nil 3316220322
("" (grind :rewrites ("least_def" "least?")) nil nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(above const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(restrict const-decl "R" restrict nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops 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)
(linear_order_to_strict_total_order application-judgement
"(strict_total_order?)" ordered_nat 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)
(least_def formula-decl nil minmax_orders nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(suffix? const-decl "bool" ordered_subset nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(upfrom_least 0
(upfrom_least-1 nil 3316220347
("" (grind :rewrites ("least_def" "least?")) nil nil)
((total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(has_least? const-decl "bool" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(restrict const-decl "R" restrict nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops 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)
(linear_order_to_total_order application-judgement "(total_order?)"
ordered_nat 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)
(least_def formula-decl nil minmax_orders nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(suffix? const-decl "bool" ordered_subset nil)
(<= const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil))
shostak))
(below_prelude 0
(below_prelude-1 nil 3316220368 ("" (grind-with-ext) 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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(linear_order_to_strict_total_order application-judgement
"(strict_total_order?)" ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(fullset const-decl "set" sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil))
shostak))
(upto_prelude 0
(upto_prelude-1 nil 3316220471 ("" (grind-with-ext) 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)
(>= 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(linear_order_to_total_order application-judgement "(total_order?)"
ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(fullset const-decl "set" sets nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(prefix? const-decl "bool" ordered_subset nil)
(order? const-decl "bool" relations_extra nil)
(pred type-eq-decl nil defined_types nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil))
shostak))
(prefix_finite 0
(prefix_finite-1 nil 3316220558
("" (skosimp :preds? t)
((""
(expand* "full?" "prefix?" "member" "is_finite" "injective?"
"restrict")
(("" (skolem!)
(("" (inst + "x!1" "LAMBDA (x: (pre!1)): x")
(("1" (skosimp) nil nil)
("2" (skolem!)
(("2" (inst - "x!1" "x!2") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(member const-decl "bool" sets nil)
(full? const-decl "bool" sets nil)
(pre!1 skolem-const-decl "(LAMBDA (S: set[nat]):
prefix?(S, restrict[[real, real], [nat, nat], boolean](<=)))"
ordered_nat nil)
(< const-decl "bool" reals nil)
(x!1 skolem-const-decl "nat" ordered_nat nil)
(below type-eq-decl nil nat_types 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)
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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 3316267591
(""
(measure-induct+ "IF is_finite(pre) THEN card(pre) ELSE 0 ENDIF"
("pre"))
(("" (typepred "x!1")
((""
(case "has_greatest?[nat](x!1, restrict[[real, real], [nat, nat], boolean](<=))")
(("1"
(inst -
"remove(greatest[nat](restrict[[real, real], [nat, nat], boolean](<=))(x!1), x!1)")
(("1" (use "finite_remove[nat]")
(("1" (assert)
(("1" (use "card_remove[nat]")
(("1"
(typepred
"greatest[nat](restrict[[real, real], [nat, nat], boolean](<=))(x!1)")
(("1" (expand "greatest?")
(("1" (assert)
(("1" (replace -3)
(("1" (decompose-equality -7)
(("1" (apply-extensionality :hide? t)
(("1"
(expand* "below" "irreflexive_kernel"
"difference" "remove" "empty?" "member")
(("1"
(expand "restrict" +)
(("1"
(iff)
(("1"
(ground)
(("1"
(inst - "x!2 - 1")
(("1"
(expand
"restrict"
-2
:occurrence
2)
(("1"
(expand* "prefix?" "member")
(("1"
(expand "restrict" -7)
(("1"
(inst - "x!2 - 1" "x!2")
(("1"
(assert)
(("1"
(assert)
(("1"
(expand
"upper_bound?")
(("1"
(expand
"restrict"
-3
:occurrence
1)
(("1"
(inst - "x!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst - "x!2 - 1")
(("2"
(expand
"restrict"
-3
:occurrence
2)
(("2"
(expand* "prefix?" "member")
(("2"
(expand "restrict" -8)
(("2"
(inst - "x!2 - 1" "x!2")
(("2"
(assert)
(("2"
(assert)
(("2"
(expand
"upper_bound?")
(("2"
(expand
"restrict"
-4
:occurrence
1)
(("2"
(inst - "x!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(case-replace "x!2 = 0")
(("1"
(expand*
"has_greatest?"
"greatest?"
"upper_bound?"
"prefix?"
"member"
"restrict")
(("1"
(skosimp)
(("1"
(inst - "0" "t!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(inst - "x!2 - 1")
(("1"
(expand
"restrict"
-2
:occurrence
2)
(("1"
(assert)
(("1"
(flatten)
(("1"
(expand "upper_bound?")
(("1"
(expand
"restrict"
-4
:occurrence
1)
(("1"
(inst - "x!2 - 1")
(("1"
(expand*
"prefix?"
"member")
(("1"
(inst
-
"x!2"
"greatest[nat](restrict[[real, real], [nat, nat], boolean](<=))(x!1)")
(("1"
(expand
"restrict"
-8
:occurrence
1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "prefix?" "member")
(("2" (skosimp :preds? t)
(("2" (expand* "remove" "member")
(("2" (expand "restrict" (-3 -5))
(("2" (flatten)
(("2" (inst - "t!1" "r!1")
(("2" (ground)
(("2"
(typepred
"greatest[nat](restrict[[real, real], [nat, nat], boolean](<=))(x!1)")
(("2" (expand* "greatest?" "upper_bound?")
(("2" (expand "restrict" -2 :occurrence 1)
(("2"
(inst - "r!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (use "total_order_restrict[real, nat]")
(("2" (use "non_empty_finite_has_greatest")
(("2" (use "empty_card")
(("2" (assert)
(("2" (replace -1)
(("2" (apply-extensionality :hide? t)
(("2"
(expand* "below" "irreflexive_kernel"
"difference" "remove" "empty?" "member")
(("2" (inst?)
(("2" (assert)
(("2" (expand "restrict" -1)
(("2" (flatten) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((NOT const-decl "[bool -> bool]" booleans nil)
(total_order_restrict judgement-tcc nil restrict_order_props nil)
(total_order? const-decl "bool" orders nil)
(empty_card formula-decl nil finite_sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_has_greatest formula-decl nil minmax_orders nil)
(x!1 skolem-const-decl "(LAMBDA (S: set[nat]):
prefix?(S, restrict[[real, real], [nat, nat], boolean](<=)))"
ordered_nat nil)
(remove const-decl "set" sets nil)
(greatest? const-decl "bool" minmax_orders nil)
(greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_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)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(t!1 skolem-const-decl "nat" ordered_nat nil)
(x!2 skolem-const-decl "nat" ordered_nat nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(card_remove formula-decl nil finite_sets nil)
(finite_remove judgement-tcc nil finite_sets nil)
(r!1 skolem-const-decl "(remove[nat]
(greatest[nat](restrict[[real, real], [nat, nat], boolean](<=))(x!1),
x!1))" ordered_nat nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(order? const-decl "bool" relations_extra nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(naturalnumber type-eq-decl nil naturalnumbers 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)
(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)
(measure_induction formula-decl nil measure_induction nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(well_founded? const-decl "bool" orders nil))
shostak))
(prefix_upto_TCC1 0
(prefix_upto_TCC1-1 nil 3316219709
("" (skosimp)
(("" (rewrite "empty_card") (("" (assert) nil nil)) nil)) nil)
((empty_card formula-decl nil finite_sets nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(prefix_upto 0
(prefix_upto-1 nil 3316270652
("" (skosimp)
(("" (forward-chain "prefix_below")
(("" (decompose-equality)
(("" (apply-extensionality :hide? t)
(("1" (inst - "x!1")
(("1"
(expand* "below" "irreflexive_kernel" "difference" "upto"
"reflexive_closure" "union" "remove" "empty?" "member"
"restrict")
(("1" (iff) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (forward-chain "prefix_upto_TCC1") nil nil))
nil))
nil))
nil))
nil)
((prefix_below formula-decl nil ordered_nat 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)
(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)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(pre!1 skolem-const-decl "(LAMBDA (S: set[nat]):
prefix?(S, restrict[[real, real], [nat, nat], boolean](<=)))"
ordered_nat nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(union const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(difference const-decl "set" sets nil)
(prefix_upto_TCC1 subtype-tcc nil ordered_nat nil)
(real_le_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])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(order? const-decl "bool" relations_extra nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil))
shostak))
(below_is_finite 0
(below_is_finite-1 nil 3316219709
("" (skolem!)
(("" (expand "is_finite")
((""
(inst + "n!1"
"LAMBDA (x: (below(n!1, restrict[[real, real], [nat, nat], boolean](<=)))): x")
(("1" (expand "injective?") (("1" (skosimp) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(linear_order_to_strict_total_order application-judgement
"(strict_total_order?)" ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(injective? const-decl "bool" functions nil)
(below type-eq-decl nil nat_types 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)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(prefix? const-decl "bool" ordered_subset nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(n!1 skolem-const-decl "nat" ordered_nat nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil))
nil))
(upto_is_finite 0
(upto_is_finite-1 nil 3316219709
("" (skolem!)
(("" (expand "is_finite")
((""
(inst + "1 + n!1"
"LAMBDA (x: (upto(n!1, restrict[[real, real], [nat, nat], boolean](<=)))): x")
(("1" (expand "injective?") (("1" (skosimp) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil)
((is_finite const-decl "bool" finite_sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(linear_order_to_total_order application-judgement "(total_order?)"
ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(injective? const-decl "bool" functions nil)
(below type-eq-decl nil nat_types 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)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(set type-eq-decl nil sets nil)
(prefix? const-decl "bool" ordered_subset nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(n!1 skolem-const-decl "nat" ordered_nat nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil))
nil))
(below_card 0
(below_card-1 nil 3316270925
("" (induct "n")
(("1" (grind :rewrites ("card_empty?")) nil nil)
("2" (skosimp)
(("2" (case "below(j!1 + 1) = add(j!1, below(j!1))")
(("1" (use "card_add")
(("1" (expand "below" -1 :occurrence 3)
(("1" (expand* "irreflexive_kernel" "difference" "member")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (apply-extensionality :hide? t)
(("2"
(expand* "below" "irreflexive_kernel" "difference" "add"
"member" "restrict")
(("2" (iff) (("2" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
("3" (skolem!) (("3" (use "below_is_finite") nil nil)) nil))
nil)
((below_is_finite judgement-tcc nil ordered_nat nil)
(card_add formula-decl nil finite_sets nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_empty? formula-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(irreflexive_kernel const-decl "(irreflexive?)" closure_ops nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(prefix? const-decl "bool" ordered_subset nil)
(below const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil))
shostak))
(upto_card 0
(upto_card-1 nil 3316271102
("" (induct "n")
(("1" (rewrite "card_one")
(("1" (inst + "0")
(("1" (apply-extensionality :hide? t)
(("1"
(expand* "upto" "reflexive_closure" "union" "member"
"singleton" "restrict")
(("1" (iff) (("1" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (case "upto(j!1 + 1) = add(j!1 + 1, upto(j!1))")
(("1" (use "card_add")
(("1" (expand "upto" -1 :occurrence 3)
(("1"
(expand* "reflexive_closure" "union" "member" "restrict")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (apply-extensionality :hide? t)
(("2"
(expand* "upto" "reflexive_closure" "union" "add" "member"
"restrict")
(("2" (iff) (("2" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
("3" (skolem!) (("3" (use "upto_is_finite") nil nil)) nil))
nil)
((upto_is_finite judgement-tcc nil ordered_nat nil)
(card_add formula-decl nil finite_sets nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(card_one formula-decl nil finite_sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" ordered_nat nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops 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)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(pred type-eq-decl nil defined_types nil)
(order? const-decl "bool" relations_extra nil)
(prefix? const-decl "bool" ordered_subset nil)
(upto const-decl "(LAMBDA (S): prefix?(S, ord))" ordered_subset
nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil))
shostak))
(suffix_empty 0
(suffix_empty-1 nil 3316271348
("" (skosimp :preds? t)
(("" (expand* "suffix?" "member" "restrict")
(("" (assert)
(("" (lemma "non_empty_finite_has_greatest")
(("" (inst - "suf!1" "lesseq")
((""
(expand* "has_greatest?" "greatest?" "upper_bound?"
"restrict")
(("" (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)
(greatest? const-decl "bool" minmax_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(suf!1 skolem-const-decl "(LAMBDA (S: set[nat]):
suffix?(S, restrict[[real, real], [nat, nat], boolean](<=)))"
ordered_nat nil)
(t!1 skolem-const-decl "nat" ordered_nat nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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 3316271535
("" (skosimp :preds? t)
(("" (use "every_nonempty_set_has_least")
(("1"
(inst +
"least(restrict[[real, real], [nat, nat], boolean](<=))(suf!1)")
(("1" (apply-extensionality :hide? t)
(("1"
(expand* "upfrom" "reflexive_closure" "union" "suffix?"
"member")
(("1"
(typepred
"least(restrict[[real, real], [nat, nat], boolean](<=))(suf!1)")
(("1" (expand "least?")
(("1" (flatten)
(("1"
(inst - "x!1"
"least(restrict[[real, real], [nat, nat], boolean](<=))(suf!1)")
(("1" (expand "restrict" -4 :occurrence 1)
(("1" (expand "restrict" 1 :occurrence 1)
(("1" (iff)
(("1" (smash)
(("1" (expand "lower_bound?")
(("1"
(expand "restrict" -2 :occurrence 1)
(("1" (inst - "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?") (("2" (propax) nil nil)) nil))
nil))
nil)
((every_nonempty_set_has_least judgement-tcc nil bounded_nats nil)
(nonempty? const-decl "bool" sets nil)
(suf!1 skolem-const-decl "(LAMBDA (S: set[nat]):
suffix?(S, restrict[[real, real], [nat, nat], boolean](<=)))"
ordered_nat nil)
(order? const-decl "bool" relations_extra nil)
(upfrom const-decl "(LAMBDA (S): suffix?(S, ord))" ordered_subset
nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(least? const-decl "bool" minmax_orders nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
ordered_nat nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
ordered_nat nil)
(transitive_restrict application-judgement "(transitive?[S])"
ordered_nat nil)
(preorder_restrict application-judgement "(preorder?[S])"
ordered_nat nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
ordered_nat nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
ordered_nat nil)
(total_order_restrict application-judgement "(total_order?[S])"
ordered_nat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 1.61 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
