| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/complex/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quellcode-Bibliothek di_subgraphs.prf Sprache: Lisp |
|||||||||
|
(di_subgraphs
(finite_vert_subset 0 (finite_vert_subset-1 nil 3253624236 ("" (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 di_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) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" 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) (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)) (finite_edge_subset 0 (finite_edge_subset-1 nil 3307706313 ("" (skosimp*) (("" (lemma "finite_subset[edgetype[T]]") (("" (inst?) (("" (inst - "edges(G!1)") (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil di_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) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets 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)) (di_subgraph_TCC1 0 (di_subgraph_TCC1-1 nil 3253624236 ("" (skosimp*) (("" (lemma "finite_subset[edgetype[T]]") (("" (inst?) (("" (inst - "edges(G!1)") (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((edgetype type-eq-decl nil digraphs nil) (T formal-type-decl nil di_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) (digraph type-eq-decl nil digraphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (predigraph type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets 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)) (di_subgraph_TCC2 0 (di_subgraph_TCC2-1 nil 3307703845 ("" (skosimp*) (("" (rewrite "finite_vert_subset") nil nil)) nil) ((finite_vert_subset formula-decl nil di_subgraphs nil) (T formal-type-decl nil di_subgraphs nil) (edgetype type-eq-decl nil digraphs nil) (finite_set type-eq-decl nil finite_sets nil) (predigraph type-eq-decl nil digraphs nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (digraph type-eq-decl nil digraphs nil) (set type-eq-decl nil sets nil)) nil)) (di_subgraph_TCC3 0 (di_subgraph_TCC3-2 nil 3307706135 ("" (skosimp*) (("" (prop) (("1" (skosimp*) (("1" (typepred "G!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "di_subgraph?") (("2" (prop) (("1" (grind) nil nil) ("2" (grind) 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 di_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) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (di_subgraph? const-decl "bool" di_subgraphs nil)) nil) (di_subgraph_TCC3-1 nil 3307703845 ("" (subtype-tcc) nil nil) ((edgetype type-eq-decl nil digraphs nil) (predigraph type-eq-decl nil digraphs nil) (digraph type-eq-decl nil digraphs nil)) nil)) (di_subgraph_vert_sub 0 (di_subgraph_vert_sub-1 nil 3253624236 ("" (skosimp*) (("" (expand "di_subgraph") (("" (apply-extensionality 1 :hide? t) (("" (expand "subset?") (("" (inst?) (("" (expand "member") (("" (iff 1) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((di_subgraph const-decl "di_subgraph(G)" di_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) (edgetype type-eq-decl nil digraphs 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) (digraph type-eq-decl nil digraphs nil) (set type-eq-decl nil sets nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil di_subgraphs nil)) nil)) (di_subgraph_lem 0 (di_subgraph_lem-1 nil 3253624236 ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil)) (di_subgraph_smaller 0 (di_subgraph_smaller-1 nil 3253624236 ("" (skosimp*) (("" (expand "size") (("" (expand "di_subgraph?") (("" (rewrite "card_subset[T]") nil nil)) nil)) nil)) nil) ((size const-decl "nat" digraphs 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) (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) (T formal-type-decl nil di_subgraphs nil) (di_subgraph? const-decl "bool" di_subgraphs nil)) nil))) ¤ 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.0.1Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28