Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/orders/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: subset_chain.prf Sprache: Lisp

Original von: PVS^©

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

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.