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/graphs/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: cross_3D.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)))