products/sources/formale sprachen/PVS/digraphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: digraphs.prf   Sprache: Lisp

Original von: PVS©
(digraphs
 (empty_digraph_TCC1 0
  (empty_digraph_TCC1-1 nil 3561336327 ("" (subtype-tcc) nil nil)
   ((emptyset const-decl "set" sets nil)) nil))
 (edges_vert 0
  (edges_vert-1 nil 3507100927
   ("" (skosimp*)
    (("" (typepred "G!1")
      (("" (inst?)
        (("" (assert)
          (("" (flatten)
            (("" (expand "in?")
              (("" (split -3)
                (("1" (replace -1 :dir rl)
                  (("1" (inst + "PROJ_2(e!1)") (("1" (assert) nil nil))
                    nil))
                  nil)
                 ("2" (replace -1 :dir rl)
                  (("2" (inst + "PROJ_1(e!1)") (("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil digraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (in? const-decl "bool" pairs nil))
   nil))
 (other_vert 0
  (other_vert-1 nil 3507100927
   ("" (skosimp*)
    (("" (typepred "G!1")
      (("" (inst?)
        (("" (assert)
          (("" (flatten)
            (("" (expand "in?")
              (("" (split -3)
                (("1" (inst + "PROJ_2(e!1)")
                  (("1" (assert)
                    (("1" (flatten)
                      (("1" (apply-extensionality 2 :hide? t) nil nil))
                      nil))
                    nil))
                  nil)
                 ("2" (inst + "PROJ_1(e!1)")
                  (("2" (assert)
                    (("2" (flatten)
                      (("2" (apply-extensionality 1 :hide? t) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil digraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (in? const-decl "bool" pairs nil))
   nil))
 (edges_to_pair 0
  (edges_to_pair-1 nil 3507100927
   ("" (skosimp*)
    (("" (inst + "proj_1(e!1)" "proj_2(e!1)")
      (("" (assert)
        (("" (case "e!1 = (proj_1(e!1),proj_2(e!1))")
          (("1" (replace -1 -)
            (("1" (assert)
              (("1" (typepred "G!1")
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (apply-extensionality 1 :hide? t) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil digraphs nil)
    (edgetype type-eq-decl nil digraphs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil))
   nil))
 (empty?_rew 0
  (empty?_rew-1 nil 3507100927
   ("" (skosimp*)
    (("" (lemma " card_empty?[T]")
      (("" (inst?)
        (("" (expand "empty?" 1)
          (("" (replace -1) (("" (propax) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil digraphs nil)
    (card_empty? formula-decl nil finite_sets nil)
    (empty? const-decl "bool" digraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (edgetype type-eq-decl nil digraphs 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
 (empty_size 0
  (empty_size-1 nil 3559650566
   ("" (skeep)
    (("" (expand "size")
      (("" (rewrite "empty?_rew") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((size const-decl "nat" digraphs nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil digraphs nil)
    (empty?_rew formula-decl nil digraphs nil))
   shostak))
 (edges_of_empty 0
  (edges_of_empty-1 nil 3507100927
   ("" (skosimp*)
    (("" (expand "empty?")
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "emptyset")
          (("" (expand "empty?")
            (("" (expand "member")
              (("" (inst?)
                (("" (assert)
                  (("" (typepred "G!1")
                    (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" digraphs nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (predigraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (emptyset const-decl "set" sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil digraphs nil))
   nil))
 (singleton_edges 0
  (singleton_edges-1 nil 3507100927
   ("" (skosimp*)
    (("" (expand "singleton?")
      (("" (expand "size")
        (("" (lemma "card_one[T]")
          (("" (inst?)
            (("" (assert)
              (("" (hide -2)
                (("" (skosimp*)
                  (("" (expand "empty?")
                    (("" (skosimp*)
                      (("" (expand "member")
                        (("" (typepred "SG!1")
                          (("" (inst?)
                            (("" (inst?)
                              ((""
                                (assert)
                                ((""
                                  (flatten)
                                  ((""
                                    (replace -3)
                                    ((""
                                      (hide -3)
                                      ((""
                                        (expand "singleton")
                                        (("" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((singleton? const-decl "bool" digraphs nil)
    (T formal-type-decl nil digraphs nil)
    (card_one formula-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (simple_digraph type-eq-decl nil digraphs nil)
    (/= const-decl "boolean" notequal nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (edgetype type-eq-decl nil digraphs 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (size const-decl "nat" digraphs nil))
   nil))
 (edge_in_card_gt_1 0
  (edge_in_card_gt_1-1 nil 3507100927
   ("" (skosimp*)
    (("" (typepred "SG!1")
      (("" (inst?)
        (("" (inst?)
          (("" (assert)
            (("" (flatten)
              ((""
                (case "subset?(add(PROJ_1(e!1),singleton(PROJ_2(e!1))),vert(SG!1))")
                (("1" (lemma "card_subset[T]")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (rewrite "card_add")
                        (("1" (rewrite "card_singleton")
                          (("1" (hide -2)
                            (("1" (expand "singleton")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (grind) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((simple_digraph type-eq-decl nil digraphs nil)
    (/= const-decl "boolean" notequal nil)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (edgetype type-eq-decl nil digraphs nil)
    (T formal-type-decl nil digraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (card_subset formula-decl nil finite_sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (card_singleton formula-decl nil finite_sets nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (card_add formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets nil)
    (set type-eq-decl nil sets nil)
    (subset? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (not_singleton_2_vert 0
  (not_singleton_2_vert-1 nil 3507100927
   ("" (skosimp*)
    (("" (expand "empty?")
      (("" (lemma "card_empty?[T]")
        (("" (inst?)
          (("" (iff)
            (("" (assert)
              (("" (expand "singleton?")
                (("" (expand "size")
                  (("" (lemma "card_2_has_2[T]")
                    (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((empty? const-decl "bool" digraphs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (edgetype type-eq-decl nil digraphs nil)
    (predigraph type-eq-decl nil digraphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (digraph type-eq-decl nil digraphs nil)
    (size const-decl "nat" digraphs nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (card_2_has_2 formula-decl nil finite_sets nil)
    (singleton? const-decl "bool" digraphs nil)
    (card_empty? formula-decl nil finite_sets nil)
    (T formal-type-decl nil digraphs nil))
   nil))
 (proj_rew 0
  (proj_rew-1 nil 3507100927
   ("" (skosimp*)
    (("" (assert) (("" (apply-extensionality 1 :hide? t) nil nil))
      nil))
    nil)
   nil nil))
 (singleton_digraph_TCC1 0
  (singleton_digraph_TCC1-1 nil 3507100927
   ("" (skosimp*) (("" (grind) nil nil)) nil)
   ((emptyset const-decl "set" sets nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   nil))
 (is_sing 0
  (is_sing-1 nil 3507100927
   ("" (skosimp*)
    (("" (expand "singleton_digraph")
      (("" (expand "singleton?")
        (("" (expand "size") (("" (rewrite "card_singleton") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((singleton_digraph const-decl "digraph" digraphs nil)
    (size const-decl "nat" digraphs nil)
    (card_singleton formula-decl nil finite_sets nil)
    (T formal-type-decl nil digraphs nil)
    (singleton? const-decl "bool" digraphs nil))
   nil)))


¤ Dauer der Verarbeitung: 0.6 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.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff