Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: subgraphs.prf Sprache: Lisp

Original von: PVS^©

(subgraphs
(finite_vert_subset 0
  (finite_vert_subset-1 nil 3251040622
   ("" (skosimp*)
    (("" (lemma "finite_subset[T]")
      (("" (inst?)
        (("" (inst -1 "vert(G!1)")
          (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil subgraphs nil)
    (finite_subset formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(subgraph_TCC1 0
  (subgraph_TCC1-1 nil 3251040622
   ("" (skosimp*)
    (("" (lemma "finite_subset[doubleton[T]]")
      (("" (inst?)
        (("" (assert)
          (("" (inst - "edges(G!1)")
            (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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-type-decl nil subgraphs nil)
    (finite_subset formula-decl nil finite_sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite const-decl "bool" finite_sets nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil))
   nil))
(subgraph_TCC2 0
  (subgraph_TCC2-1 nil 3307708398
   ("" (skosimp*)
    (("" (lemma "finite_vert_subset") (("" (inst?) nil nil)) nil)) nil)
   ((finite_vert_subset formula-decl nil subgraphs nil)
    (T formal-type-decl nil subgraphs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil))
   nil))
(subgraph_TCC3 0
  (subgraph_TCC3-2 nil 3307713815
   ("" (skosimp*)
    (("" (split +)
      (("1" (skosimp*)
        (("1" (typepred "G!1")
          (("1" (inst?)
            (("1" (assert)
              (("1" (inst?)
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (grind) nil nil))
      nil))
    nil)
   ((graph type-eq-decl nil graphs nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil subgraphs 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)
    (subset? const-decl "bool" sets nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil))
   nil)
  (subgraph_TCC3-1 nil 3307708398 ("" (subtype-tcc) nil nil) nil nil))
(subgraph_vert_sub 0
  (subgraph_vert_sub-1 nil 3251040622
   ("" (skosimp*)
    (("" (expand "subgraph")
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "subset?")
          (("" (inst?)
            (("" (expand "member")
              (("" (iff 1) (("" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subgraph const-decl "Subgraph(G)" subgraphs nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil subgraphs nil))
   nil))
(subgraph_lem 0
  (subgraph_lem-1 nil 3251040622
   ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil))
(subgraph_smaller 0
  (subgraph_smaller-1 nil 3251040622
   ("" (skosimp*)
    (("" (expand "size")
      (("" (expand "subgraph?")
        (("" (rewrite "card_subset[T]") nil nil)) nil))
      nil))
    nil)
   ((size const-decl "nat" graphs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (card_subset formula-decl nil finite_sets 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (T formal-type-decl nil subgraphs nil)
    (subgraph? const-decl "bool" subgraphs nil))
   nil)))

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