Quelle non_empty_bounded_sets.prf Sprache: Lisp

(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)))

quality100%

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.