Quelle finite_orders.prf Sprache: Lisp

(finite_orders
(IMP_finite_types_TCC1 0
  (IMP_finite_types_TCC1-1 nil 3315153951
   ("" (rewrite "finite_type") nil nil)
   ((finite_type formula-decl nil finite_orders nil)) nil))
(finite_lower_semilattice_is_complete 0
  (finite_lower_semilattice_is_complete-1 nil 3315153982
   ("" (skosimp)
    (("" (expand* "complete_lower_semilattice?" "lower_semilattice?")
      (("" (prop)
        (("" (skolem!)
          (("" (case-replace "S!1 = emptyset")
            (("" (inst?) (("" (rewrite "emptyset_is_empty?") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((lower_semilattice? const-decl "bool" bounded_orders nil)
    (complete_lower_semilattice? const-decl "bool" bounded_orders nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (S!1 skolem-const-decl "set[T]" finite_orders nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (emptyset const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil finite_orders nil))
   shostak))
(finite_upper_semilattice_is_complete 0
  (finite_upper_semilattice_is_complete-1 nil 3315154016
   ("" (skosimp)
    (("" (expand* "complete_upper_semilattice?" "upper_semilattice?")
      (("" (prop)
        (("" (skolem!)
          (("" (case-replace "S!1 = emptyset")
            (("" (inst?) (("" (rewrite "emptyset_is_empty?") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((upper_semilattice? const-decl "bool" bounded_orders nil)
    (complete_upper_semilattice? const-decl "bool" bounded_orders nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (S!1 skolem-const-decl "set[T]" finite_orders nil)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil)
    (emptyset const-decl "set" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil finite_orders nil))
   shostak))
(finite_lattice_is_complete 0
  (finite_lattice_is_complete-1 nil 3315153951
   ("" (skolem-typepred)
    (("" (expand* "complete_lattice?" "lattice?")
      (("" (prop)
        (("1" (rewrite "finite_upper_semilattice_is_complete")
          (("1" (rewrite "least_bounded_above_emptyset")
            (("1" (rewrite "all_finite_greatest_bounded") nil nil))
            nil))
          nil)
         ("2" (rewrite "finite_lower_semilattice_is_complete")
          (("2" (rewrite "greatest_bounded_below_emptyset")
            (("2" (rewrite "all_finite_least_bounded") nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((complete_lattice? const-decl "bool" bounded_orders nil)
    (finite_lower_semilattice_is_complete formula-decl nil
     finite_orders nil)
    (all_finite_least_bounded formula-decl nil bounded_orders nil)
    (upper_semilattice? const-decl "bool" bounded_orders nil)
    (greatest_bounded_below_emptyset formula-decl nil bounded_orders
     nil)
    (finite_upper_semilattice_is_complete formula-decl nil
     finite_orders nil)
    (all_finite_greatest_bounded formula-decl nil bounded_orders 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)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (fullset const-decl "set" sets nil)
    (lower_semilattice? const-decl "bool" bounded_orders nil)
    (fullset_is_nonempty_finite name-judgement
     "non_empty_finite_set[T]" finite_orders nil)
    (least_bounded_above_emptyset formula-decl nil bounded_orders nil)
    (lattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil finite_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(finite_strict_order_is_well_founded 0
  (finite_strict_order_is_well_founded-1 nil 3315153951
   ("" (skolem-typepred)
    (("" (expand "well_founded?")
      (("" (measure-induct+ "card(p)" ("p"))
        (("" (skolem!)
          (("" (inst - "remove(y!1, x!2)")
            (("" (prop)
              (("1" (inst-cp + "y!1")
                (("1" (skosimp* t)
                  (("1" (inst + "y!2")
                    (("1" (skolem-typepred)
                      (("1" (inst-cp - "x!3")
                        (("1" (inst - "x!4")
                          (("1" (expand* "remove" "member" "/=")
                            (("1" (lemma "transitive")
                              (("1"
                                (inst - "x!1" "x!3" "y!1" "y!2")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand* "remove" "member" "/=")
                          (("2" (use "irreflexive")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand* "remove" "member")
                      (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (inst 2 "y!1")
                (("2" (skolem-typepred)
                  (("2" (inst + "x!3")
                    (("2" (expand* "remove" "member" "/=")
                      (("2" (use "irreflexive")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (rewrite "card_remove") (("3" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((well_founded? const-decl "bool" orders nil)
    (irreflexive? const-decl "bool" relations nil)
    (irreflexive formula-decl nil relations_extra nil)
    (x!4 skolem-const-decl "(x!2)" finite_orders nil)
    (transitive formula-decl nil relations_extra nil)
    (PRED type-eq-decl nil defined_types nil)
    (transitive? const-decl "bool" relations nil)
    (/= const-decl "boolean" notequal nil)
    (member const-decl "bool" sets nil)
    (x!3 skolem-const-decl "(x!2)" finite_orders nil)
    (finite_remove application-judgement "finite_set[T]" finite_orders
     nil)
    (y!2 skolem-const-decl "(remove(y!1, x!2))" finite_orders nil)
    (y!1 skolem-const-decl "T" finite_orders nil)
    (x!2 skolem-const-decl "pred[T]" finite_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)
    (card_remove formula-decl nil finite_sets nil)
    (remove const-decl "set" sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (naturalnumber type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (measure_induction formula-decl nil measure_induction nil)
    (strict_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil finite_orders nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(finite_strict_total_order_is_well_ordered 0
  (finite_strict_total_order_is_well_ordered-1 nil 3315153951
   ("" (skolem-typepred)
    (("" (expand "well_ordered?")
      (("" (rewrite "finite_strict_order_is_well_founded") nil nil))
      nil))
    nil)
   ((well_ordered? const-decl "bool" orders nil)
    (strict_order? const-decl "bool" orders nil)
    (finite_strict_order_is_well_founded judgement-tcc nil
     finite_orders nil)
    (strict_total_order? const-decl "bool" orders nil)
    (pred type-eq-decl nil defined_types nil)
    (T formal-nonempty-type-decl nil finite_orders 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.18 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.