|
(non_empty_bounded_sets
(non_empty_bounded_above_is_nonempty 0
(non_empty_bounded_above_is_nonempty-1 nil 3314558697
("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" non_empty_bounded_sets nil)
(T formal-subtype-decl nil non_empty_bounded_sets nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(bounded_above? const-decl "bool" bounded_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(total_order_restrict application-judgement "(total_order?[S])"
restrict_order_props nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(non_empty_bounded_above_is_bounded_above 0
(non_empty_bounded_above_is_bounded_above-1 nil 3314558697
("" (judgement-tcc) nil nil)
((bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(nonempty? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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)
(restrict const-decl "R" restrict nil)
(T formal-subtype-decl nil non_empty_bounded_sets nil)
(T_pred const-decl "[real -> boolean]" non_empty_bounded_sets 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)
(upper_bound? const-decl "bool" bounded_orders nil)
(bounded_above? const-decl "bool" bounded_orders nil))
nil))
(non_empty_bounded_below_is_nonempty 0
(non_empty_bounded_below_is_nonempty-1 nil 3314558697
("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" non_empty_bounded_sets nil)
(T formal-subtype-decl nil non_empty_bounded_sets nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(bounded_below? const-decl "bool" bounded_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(total_order_restrict application-judgement "(total_order?[S])"
restrict_order_props nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(non_empty_bounded_below_is_bounded_below 0
(non_empty_bounded_below_is_bounded_below-1 nil 3314558697
("" (judgement-tcc) nil nil)
((bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(nonempty? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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)
(restrict const-decl "R" restrict nil)
(T formal-subtype-decl nil non_empty_bounded_sets nil)
(T_pred const-decl "[real -> boolean]" non_empty_bounded_sets nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(bounded_below? const-decl "bool" bounded_orders nil))
nil))
(non_empty_finite_bounded_above 0
(non_empty_finite_bounded_above-1 nil 3314558697
("" (skolem-typepred)
(("" (lemma "all_finite_least_bounded")
(("" (inst - "x!1" "reals.<=")
((""
(expand* "least_bounded_above?" "least_upper_bound?"
"non_empty_bounded_above?" "nonempty?" "bounded_above?")
(("" (skosimp) (("" (inst? +) nil nil)) nil)) nil))
nil))
nil))
nil)
((all_finite_least_bounded formula-decl nil bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(nonempty? const-decl "bool" sets nil)
(bounded_above? const-decl "bool" bounded_orders nil)
(non_empty_bounded_above? const-decl "bool" non_empty_bounded_sets
nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(total_order_restrict application-judgement "(total_order?[S])"
restrict_order_props nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil non_empty_bounded_sets nil)
(T_pred const-decl "[real -> boolean]" non_empty_bounded_sets 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_finite_bounded_below 0
(non_empty_finite_bounded_below-1 nil 3314558697
("" (skolem-typepred)
(("" (lemma "all_finite_greatest_bounded")
(("" (inst - "x!1" "reals.<=")
((""
(expand* "greatest_bounded_below?" "greatest_lower_bound?"
"non_empty_bounded_below?" "nonempty?" "bounded_below?")
(("" (skosimp) (("" (inst? +) nil nil)) nil)) nil))
nil))
nil))
nil)
((all_finite_greatest_bounded formula-decl nil bounded_orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(nonempty? const-decl "bool" sets nil)
(bounded_below? const-decl "bool" bounded_orders nil)
(non_empty_bounded_below? const-decl "bool" non_empty_bounded_sets
nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(<= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(total_order_restrict application-judgement "(total_order?[S])"
restrict_order_props nil)
(dichotomous_restrict application-judgement "(dichotomous?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-subtype-decl nil non_empty_bounded_sets nil)
(T_pred const-decl "[real -> boolean]" non_empty_bounded_sets 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)))
¤ Dauer der Verarbeitung: 0.7 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.
|
