|
(bounded_integers
(non_empty_bounded_above_has_greatest_lem 0
(non_empty_bounded_above_has_greatest_lem-1 nil 3314629024
("" (induct "c" :name "NAT_induction")
(("" (skosimp*)
((""
(case "upper_bound?[T](i!1, S!1, restrict[[real, real], [T, T], boolean](<=))")
(("1" (expand* "has_greatest?" "greatest?")
(("1" (inst? +) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "upper_bound?" +)
(("2" (expand "restrict" 1)
(("2" (skolem!)
(("2" (inst - "j!2 - r!1")
(("1" (assert)
(("1" (inst - "S!1" "r!1" "j!2")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand* "upper_bound?" "restrict")
(("2" (inst - "r!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(r!1 skolem-const-decl "(S!1)" bounded_integers nil)
(S!1 skolem-const-decl "set[T]" bounded_integers nil)
(j!2 skolem-const-decl "T" bounded_integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(greatest? const-decl "bool" minmax_orders nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(NAT_induction formula-decl nil naturalnumbers nil)
(has_greatest? 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)
(<= const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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))
(non_empty_bounded_above_has_greatest 0
(non_empty_bounded_above_has_greatest-1 nil 3314628965
("" (skolem-typepred)
(("" (expand* "non_empty_bounded_above?" "bounded_above?")
(("" (flatten)
(("" (rewrite "nonempty_exists")
(("" (skosimp* :preds? t)
(("" (hide -2 -1)
(("" (lemma "non_empty_bounded_above_has_greatest_lem")
(("" (inst?)
(("" (inst?)
(("" (inst - "t!1 - x!2")
(("1" (assert) nil nil)
("2" (expand* "upper_bound?" "restrict")
(("2" (inst - "x!2") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" bounded_orders nil)
(nonempty_exists formula-decl nil sets_lemmas nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(x!2 skolem-const-decl "(x!1)" bounded_integers nil)
(x!1 skolem-const-decl "(non_empty_bounded_above?)"
bounded_integers nil)
(t!1 skolem-const-decl "T" bounded_integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(upper_bound? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(non_empty_bounded_above_has_greatest_lem formula-decl nil
bounded_integers nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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))
(non_empty_bounded_below_has_least_lem 0
(non_empty_bounded_below_has_least_lem-1 nil 3314629266
("" (induct "c" :name "NAT_induction")
(("" (skosimp*)
((""
(case "lower_bound?[T](i!1, S!1, restrict[[real, real], [T, T], boolean](<=))")
(("1" (expand* "has_least?" "least?")
(("1" (inst? +) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "lower_bound?" +)
(("2" (expand "restrict" 1)
(("2" (skolem!)
(("2" (inst - "r!1 - j!2")
(("1" (assert)
(("1" (inst - "S!1" "r!1" "j!2")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand* "lower_bound?" "restrict")
(("2" (inst - "r!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(j!2 skolem-const-decl "T" bounded_integers nil)
(r!1 skolem-const-decl "(S!1)" bounded_integers nil)
(S!1 skolem-const-decl "set[T]" bounded_integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(least? const-decl "bool" minmax_orders nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(NAT_induction formula-decl nil naturalnumbers 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)
(<= const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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))
(non_empty_bounded_below_has_least 0
(non_empty_bounded_below_has_least-1 nil 3314628965
("" (skolem-typepred)
(("" (expand* "non_empty_bounded_below?" "bounded_below?")
(("" (flatten)
(("" (rewrite "nonempty_exists")
(("" (skosimp* :preds? t)
(("" (hide -2 -1)
(("" (lemma "non_empty_bounded_below_has_least_lem")
(("" (inst?)
(("" (inst?)
(("" (inst - "x!2 - t!1")
(("1" (assert) nil nil)
("2" (expand* "lower_bound?" "restrict")
(("2" (inst - "x!2") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" bounded_orders nil)
(nonempty_exists formula-decl nil sets_lemmas nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(t!1 skolem-const-decl "T" bounded_integers nil)
(x!2 skolem-const-decl "(x!1)" bounded_integers nil)
(x!1 skolem-const-decl "(non_empty_bounded_below?)"
bounded_integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(lower_bound? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(non_empty_bounded_below_has_least_lem formula-decl nil
bounded_integers nil)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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))
(remove_least_TCC1 0
(remove_least_TCC1-1 nil 3314628965
("" (skosimp)
(("" (rewrite "non_empty_bounded_below_has_least")
(("" (expand "non_empty_bounded_below?") (("" (propax) nil nil))
nil))
nil))
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_preserves_bounded_below application-judgement
"(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_integers nil)
(non_empty_bounded_below_has_least judgement-tcc nil
bounded_integers 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]" bounded_integers nil)
(T formal-subtype-decl nil bounded_integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(remove const-decl "set" sets nil)
(pred type-eq-decl nil defined_types 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))
nil))
(remove_least 0
(remove_least-1 nil 3314629437
("" (skosimp)
(("" (invoke (typepred "%1" "%2") (! 1 l) (! 1 r))
(("" (hide -4 -1)
(("" (invoke (name-replace "X" "%1") (! 1 l))
(("" (invoke (name-replace "Y" "%1") (! 1 r))
((""
(expand* "least?" "remove" "member" "/=" "lower_bound?"
"restrict")
(("" (flatten)
(("" (inst - "Y") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((remove_preserves_bounded_below application-judgement
"(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_integers 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]" bounded_integers nil)
(T formal-subtype-decl nil bounded_integers nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil 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)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(remove const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(member const-decl "bool" sets nil)
(Sl!1 skolem-const-decl "(non_empty_bounded_below?)"
bounded_integers nil)
(X skolem-const-decl
"{t: (Sl!1) | least?(t, Sl!1, restrict[[real, real], [T, T], bool](<=))}"
bounded_integers nil)
(Y skolem-const-decl "{t: (remove(X, Sl!1)) |
least?(t, remove(X, Sl!1),
restrict[[real, real], [T, T], bool](<=))}"
bounded_integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(remove_least_monotone 0
(remove_least_monotone-1 nil 3314629975
("" (expand* "subset?" "remove" "member")
(("" (skosimp*)
(("" (inst-cp - "x!1")
(("" (prop)
(("" (invoke (typepred "%1") (! -1 l))
(("" (replace -4 :hide? t)
(("" (use "antisymmetric_restrict[real, T]")
(("" (rewrite "least_def") (("" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((least_def formula-decl nil minmax_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(Sl2!1 skolem-const-decl "(non_empty_bounded_below?)"
bounded_integers nil)
(Sl1!1 skolem-const-decl "(non_empty_bounded_below?)"
bounded_integers nil)
(r!1 skolem-const-decl "(Sl1!1)" bounded_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric_restrict judgement-tcc nil restrict_order_props nil)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(<= const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil)
(least? const-decl "bool" minmax_orders nil)
(has_least? const-decl "bool" minmax_orders nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil))
shostak))
(remove_greatest_TCC1 0
(remove_greatest_TCC1-1 nil 3314628965
("" (skosimp)
(("" (rewrite "non_empty_bounded_above_has_greatest")
(("" (expand "non_empty_bounded_above?") (("" (propax) nil nil))
nil))
nil))
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_preserves_bounded_above application-judgement
"(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_integers nil)
(non_empty_bounded_above_has_greatest judgement-tcc nil
bounded_integers 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]" bounded_integers nil)
(T formal-subtype-decl nil bounded_integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(remove const-decl "set" sets nil)
(pred type-eq-decl nil defined_types nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil))
nil))
(remove_greatest 0
(remove_greatest-1 nil 3314629695
("" (skosimp)
(("" (invoke (typepred "%1" "%2") (! 1 r) (! 1 l))
(("" (hide -4 -1)
(("" (invoke (name-replace "X" "%1") (! 1 l))
(("" (invoke (name-replace "Y" "%1") (! 1 r))
((""
(expand* "greatest?" "remove" "member" "/="
"upper_bound?" "restrict")
(("" (flatten)
(("" (inst - "X") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((remove_preserves_bounded_above application-judgement
"(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_integers 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]" bounded_integers nil)
(T formal-subtype-decl nil bounded_integers nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(greatest? const-decl "bool" minmax_orders nil)
(greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(remove const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(member const-decl "bool" sets nil)
(Su!1 skolem-const-decl "(non_empty_bounded_above?)"
bounded_integers nil)
(X skolem-const-decl "{t:
(remove(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su!1),
Su!1)) |
greatest?(t,
remove(greatest[T]
(restrict[[real, real], [T, T], bool](<=))
(Su!1),
Su!1),
restrict[[real, real], [T, T], bool](<=))}"
bounded_integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(remove_greatest_monotone 0
(remove_greatest_monotone-1 nil 3314630088
("" (expand* "subset?" "remove" "member")
(("" (skosimp*)
(("" (inst-cp - "x!1")
(("" (prop)
(("" (invoke (typepred "%1") (! -1 l))
(("" (replace -4 :hide? t)
(("" (use "antisymmetric_restrict[real, T]")
(("" (rewrite "greatest_def") (("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((greatest_def formula-decl nil minmax_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(Su2!1 skolem-const-decl "(non_empty_bounded_above?)"
bounded_integers nil)
(Su1!1 skolem-const-decl "(non_empty_bounded_above?)"
bounded_integers nil)
(r!1 skolem-const-decl "(Su1!1)" bounded_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric_restrict judgement-tcc nil restrict_order_props nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(<= const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil))
shostak))
(intersection_greatest 0
(intersection_greatest-1 nil 3314634466
("" (skosimp :preds? t)
(("" (lemma "non_empty_bounded_above_has_greatest")
(("" (inst-cp - "Su2!1")
(("" (inst - "Su1!1")
(("" (expand* "disjoint?" "empty?" "member")
(("" (expand "restrict")
(("" (skolem!)
(("" (lemma "non_empty_bounded_above_has_greatest_lem")
((""
(inst - "intersection(Su1!1, Su2!1)"
"max(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1!1), greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2!1)) - x!1"
"x!1"
"max(greatest[T](restrict[[real, real], [T, T], bool](<=))(Su1!1), greatest[T](restrict[[real, real], [T, T], bool](<=))(Su2!1))")
(("1" (assert)
(("1" (expand "restrict")
(("1" (expand* "upper_bound?" "max")
(("1" (skolem-typepred)
(("1" (expand* "intersection" "member")
(("1"
(lift-if)
(("1"
(prop)
(("1"
(lemma "greatest_ge")
(("1"
(inst
-
"restrict[[real, real], [T, T], bool](<=)"
"Su2!1"
"r!1")
(("1"
(expand "restrict")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma "greatest_ge")
(("2"
(inst
-
"restrict[[real, real], [T, T], bool](<=)"
"Su1!1"
"r!1")
(("2"
(expand "restrict")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "max")
(("2" (expand* "max" "intersection" "member")
(("2" (expand "restrict")
(("2" (propax) nil nil)) nil))
nil))
nil)
("3" (expand* "max" "intersection" "member")
(("3" (lift-if)
(("3" (prop)
(("1" (lemma "greatest_ge")
(("1"
(inst -
"restrict[[real, real], [T, T], bool](<=)"
"Su2!1" "x!1")
(("1"
(expand "restrict" -1 :occurrence 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "greatest_ge")
(("2"
(inst -
"restrict[[real, real], [T, T], bool](<=)"
"Su1!1" "x!1")
(("2"
(expand "restrict" -1 :occurrence 1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((non_empty_bounded_above_has_greatest judgement-tcc nil
bounded_integers nil)
(restrict const-decl "R" restrict nil)
(non_empty_bounded_above_has_greatest_lem formula-decl nil
bounded_integers nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(r!1 skolem-const-decl "(intersection(Su1!1, Su2!1))"
bounded_integers nil)
(greatest_ge formula-decl nil minmax_orders nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(intersection const-decl "set" sets nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(x!1 skolem-const-decl "T" bounded_integers nil)
(Su2!1 skolem-const-decl "(non_empty_bounded_above?)"
bounded_integers nil)
(Su1!1 skolem-const-decl "(non_empty_bounded_above?)"
bounded_integers nil)
(<= const-decl "bool" reals nil)
(greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders
nil)
(greatest? const-decl "bool" minmax_orders nil)
(has_greatest? const-decl "bool" minmax_orders nil)
(pred type-eq-decl nil defined_types nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_max application-judgement "{k: int | i <= k AND j <= k}"
real_defs nil)
(rat_max application-judgement "{s: rat | s >= q AND s >= r}"
real_defs 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(disjoint? const-decl "bool" sets nil)
(intersection1_preserves_bounded_above application-judgement
"(LAMBDA (S: set[T]): bounded_above?(S, R))" bounded_integers nil)
(member const-decl "bool" sets nil)
(empty? 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)
(T_pred const-decl "[int -> boolean]" bounded_integers nil)
(T formal-subtype-decl nil bounded_integers nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil))
shostak))
(intersection_least 0
(intersection_least-1 nil 3314635936
("" (auto-rewrite "restrict")
(("" (skosimp :preds? t)
(("" (lemma "non_empty_bounded_below_has_least")
(("" (inst-cp - "Sl2!1")
(("" (inst - "Sl1!1")
(("" (expand* "disjoint?" "empty?" "member")
(("" (skolem!)
(("" (lemma "non_empty_bounded_below_has_least_lem")
((""
(inst - "intersection(Sl1!1, Sl2!1)"
"x!1 - min(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1!1), least[T](restrict[[real, real], [T, T], bool](<=))(Sl2!1))"
"x!1"
"min(least[T](restrict[[real, real], [T, T], bool](<=))(Sl1!1), least[T](restrict[[real, real], [T, T], bool](<=))(Sl2!1))")
(("1" (assert)
(("1" (expand* "lower_bound?" "min")
(("1" (skolem-typepred)
(("1" (expand* "intersection" "member")
(("1" (lift-if)
(("1"
(prop)
(("1"
(lemma "least_le")
(("1"
(inst
-
"restrict[[real, real], [T, T], bool](<=)"
"Sl2!1"
"r!1")
nil
nil))
nil)
("2"
(lemma "least_le")
(("2"
(inst
-
"restrict[[real, real], [T, T], bool](<=)"
"Sl1!1"
"r!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "min")
(("2" (expand* "min" "intersection" "member")
(("2" (prop)
(("1" (lemma "least_le")
(("1"
(inst -
"restrict[[real, real], [T, T], bool](<=)"
"Sl2!1" "x!1")
(("1"
(expand "restrict" -1 :occurrence 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "least_le")
(("2"
(inst -
"restrict[[real, real], [T, T], bool](<=)"
"Sl1!1" "x!1")
(("2"
(expand "restrict" -1 :occurrence 1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand* "min" "intersection" "member")
(("3" (lift-if)
(("3" (prop)
(("1" (lemma "least_le")
(("1"
(inst -
"restrict[[real, real], [T, T], bool](<=)"
"Sl2!1" "x!1")
(("1"
(expand "restrict" -1 :occurrence 1)
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (lemma "least_le")
(("2"
(inst -
"restrict[[real, real], [T, T], bool](<=)"
"Sl1!1" "x!1")
(("2"
(expand "restrict" -1 :occurrence 1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil bounded_integers nil)
(T_pred const-decl "[int -> boolean]" bounded_integers 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)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(intersection1_preserves_bounded_below application-judgement
"(LAMBDA (S: set[T]): bounded_below?(S, R))" bounded_integers nil)
(disjoint? const-decl "bool" sets nil)
(non_empty_bounded_below_has_least_lem formula-decl nil
bounded_integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(least_le formula-decl nil minmax_orders nil)
(r!1 skolem-const-decl "(intersection(Sl1!1, Sl2!1))"
bounded_integers nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(intersection const-decl "set" sets nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Sl2!1 skolem-const-decl "(non_empty_bounded_below?)"
bounded_integers nil)
(Sl1!1 skolem-const-decl "(non_empty_bounded_below?)"
bounded_integers 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)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(x!1 skolem-const-decl "T" bounded_integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(non_empty_bounded_below_has_least judgement-tcc nil
bounded_integers nil))
shostak)))
¤ Dauer der Verarbeitung: 0.49 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.
|
