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.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Diese beiden folgenden Angebotsgruppen bietet das Unternehmen

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.