Quelle subset_chain.prf Sprache: Lisp

(subset_chain
(subset_chain_min 0
  (subset_chain_min-1 nil 3314727715 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil subset_chain nil)
    (set type-eq-decl nil sets nil)
    (chain? const-decl "bool" chain nil)
    (chain nonempty-type-eq-decl nil chain nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     subset_chain nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas 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)
    (restrict const-decl "R" restrict nil)
    (dichotomous? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil)
    (Intersection const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil))
   shostak))
(subset_chain_intersection 0
  (subset_chain_intersection-1 nil 3314727727
   ("" (skosimp :preds? t)
    (("" (expand "maximal_chain?")
      (("" (lemma "subset_chain_min" ("C" "C!1"))
        (("" (inst + "add(Intersection(C!1), C!1)")
          (("1" (expand "strict_subset?")
            (("1" (use "subset_add[set[T]]")
              (("1" (assert)
                (("1" (decompose-equality)
                  (("1" (inst - "Intersection(C!1)")
                    (("1" (expand* "add" "member") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (grind :if-match nil)
            (("1" (expand "Intersection")
              (("1" (decompose-equality)
                (("1" (inst - "x!2")
                  (("1" (assert) (("1" (inst - "y!1") nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (inst - "x!1")
              (("2" (inst - "x!3")
                (("2" (assert)
                  (("2" (expand "Intersection")
                    (("2" (decompose-equality)
                      (("2" (inst - "x!3") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("3" (inst -6 "x!1" "y!1")
              (("3" (split)
                (("1" (inst - "x!2") (("1" (assert) nil nil)) nil)
                 ("2" (inst - "x!3") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((maximal_chain? const-decl "bool" chain nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" subset_chain nil)
    (Intersection_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (C!1 skolem-const-decl "chain[set[T], subset?]" subset_chain nil)
    (Intersection const-decl "set" sets nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (add const-decl "(nonempty?)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (subset_add formula-decl nil sets_lemmas nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (strict_subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     subset_chain 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)
    (restrict const-decl "R" restrict nil)
    (dichotomous? const-decl "bool" orders nil)
    (total_order? const-decl "bool" orders nil)
    (subset_chain_min formula-decl nil subset_chain nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil subset_chain nil)
    (set type-eq-decl nil sets nil)
    (subset? const-decl "bool" sets nil)
    (chain? const-decl "bool" chain nil)
    (chain nonempty-type-eq-decl nil chain nil))
   shostak)))

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:

sprechenden Kalenders