| products/sources/formale sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: ClassString.java Sprache: LispOriginal von: PVS© |
|
||||||
|
(graphs
(edg_TCC1 0 (edg_TCC1-1 nil 3250875543 ("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil) ((T formal-type-decl nil graphs nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal nil)) nil)) (edge?_TCC1 0 (edge?_TCC1-1 nil 3250875543 ("" (subtype-tcc) 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 graphs nil) (set type-eq-decl nil sets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil) (y!1 skolem-const-decl "T" graphs nil) (x!1 skolem-const-decl "T" graphs nil) (nil application-judgement "finite_set[T]" graphs nil) (/= const-decl "boolean" notequal nil)) nil)) (edge?_comm 0 (edge?_comm-1 nil 3250875543 ("" (skosimp*) (("" (expand "edge?") (("" (rewrite "dbl_comm") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((nil application-judgement "finite_set[T]" graphs nil) (edge? const-decl "bool" graphs nil) (T formal-type-decl nil graphs nil) (dbl_comm formula-decl nil doubletons nil)) nil)) (edges_vert 0 (edges_vert-1 nil 3250875543 ("" (skosimp*) (("" (typepred "e!1") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (lemma "dbl_to_pair_lem") (("" (inst?) (("" (assert) (("" (prop) (("1" (hide -1) (("1" (expand "dbl" -1) (("1" (prop) (("1" (inst 2 "y!1") (("1" (assert) (("1" (typepred "G!1") (("1" (inst?) (("1" (assert) (("1" (inst -1 "y!1") (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (inst?) (("2" (typepred "G!1") (("2" (inst?) (("1" (assert) (("1" (inst?) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) (("2" (hide -1 3) (("2" (apply-extensionality :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "dbl" -1) (("2" (split) (("1" (replace -1) (("1" (hide -1) (("1" (inst 2 "y!1") (("1" (assert) (("1" (typepred "G!1") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (inst 2 "x!2") (("2" (assert) (("2" (typepred "G!1") (("2" (inst?) (("1" (assert) (("1" (inst?) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (dbl_to_pair_lem formula-decl nil doubletons nil) (nil application-judgement "finite_set[T]" graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil)) nil)) (other_vert 0 (other_vert-1 nil 3250875543 ("" (skosimp*) (("" (typepred "e!1") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (expand "dbl" -1) (("" (prop) (("1" (replace -1) (("1" (hide -1) (("1" (inst 2 "y!1") (("1" (typepred "G!1") (("1" (inst?) (("1" (assert) (("1" (inst -1 "y!1") (("1" (expand "dbl" -1) (("1" (assert) (("1" (hide -1 -2) (("1" (apply-extensionality 2 :hide? t) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) (("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (hide -1) (("2" (inst 2 "x!1") (("2" (typepred "G!1") (("2" (inst?) (("1" (assert) (("1" (inst -1 "x!1") (("1" (assert) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) 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) (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nil application-judgement "finite_set[T]" graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (pregraph type-eq-decl nil graphs nil) (graph type-eq-decl nil graphs nil)) nil)) (edge_has_2_verts 0 (edge_has_2_verts-1 nil 3250875543 ("" (skosimp*) (("" (typepred "e!1") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (apply-extensionality 3 :hide? t) (("" (expand "dbl") (("" (iff) (("" (ground) nil 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) (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nil application-judgement "finite_set[T]" graphs nil)) nil)) (edges_vert_in 0 (edges_vert_in-1 nil 3349190365 ("" (skosimp*) (("" (typepred "G!1") (("" (inst?) (("" (assert) (("" (replace -2) (("" (hide -2) (("" (inst-cp -1 "x!1") (("" (expand "dbl") (("" (assert) (("" (inst -1 "y!1") 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 graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nil application-judgement "finite_set[T]" graphs nil)) nil)) (vert_in 0 (vert_in-2 "Few TCC" 3358448762 ("" (skosimp*) (("" (typepred "G!1") (("" (inst -1 "dbl[T](x!1, y!1)") (("1" (expand "edge?") (("1" (prop) (("1" (inst -1 "x!1") (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil) ("2" (inst -1 "y!1") (("2" (expand "dbl") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "edge?") (("2" (inst 1 "x!1" "y!1") (("2" (prop) nil nil)) nil)) 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 graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (edge? const-decl "bool" graphs nil) (y!1 skolem-const-decl "T" graphs nil) (x!1 skolem-const-decl "T" graphs nil) (nil application-judgement "finite_set[T]" graphs nil)) shostak) (vert_in-1 nil 3358159836 ("" (skosimp*) (("" (lemma "edges_vert_in") (("" (inst -1 "G!1" "dbl[T](x!1,y!1)" "x!1" "y!1") (("" (prop) nil nil)) nil)) nil)) nil) ((doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil)) shostak)) (empty?_rew 0 (empty?_rew-1 nil 3250875543 ("" (skosimp*) (("" (lemma " card_empty?[T]") (("" (inst?) (("" (expand "empty?" 1) (("" (replace -1) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil graphs nil) (card_empty? formula-decl nil finite_sets nil) (empty? const-decl "bool" graphs nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs 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) (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)) (edges_of_empty 0 (edges_of_empty-1 nil 3250875543 ("" (skosimp*) (("" (expand "empty?") (("" (apply-extensionality 1 :hide? t) (("" (expand "emptyset") (("" (expand "empty?") (("" (typepred "x!1") (("" (skosimp*) (("" (inst -3 "y!1") (("" (expand "member") (("" (typepred "G!1") (("" (inst?) (("" (assert) (("" (inst -1 "y!1") (("" (replace -2) (("" (expand "dbl") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (nil application-judgement "finite_set[T]" graphs nil) (member const-decl "bool" sets 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) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (emptyset const-decl "set" 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) (T formal-type-decl nil graphs nil)) nil)) (singleton_edges 0 (singleton_edges-1 nil 3250875543 ("" (skosimp*) (("" (expand "singleton?") (("" (expand "size") (("" (lemma "card_one[T]") (("" (inst?) (("" (assert) (("" (hide -2) (("" (skosimp*) (("" (expand "empty?") (("" (skosimp*) (("" (expand "member") (("" (typepred "x!2") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (typepred "G!1") (("" (inst?) (("1" (assert) (("1" (inst-cp -1 "x!3") (("1" (inst -1 "y!1") (("1" (expand "dbl") (("1" (hide -4) (("1" (replace -3) (("1" (hide -3) (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton? const-decl "bool" graphs nil) (T formal-type-decl nil graphs nil) (card_one formula-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (singleton const-decl "(singleton?)" sets nil) (nil application-judgement "finite_set[T]" graphs nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (graph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pregraph type-eq-decl nil graphs 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) (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" graphs nil)) nil)) (edge_in_card_gt_1 0 (edge_in_card_gt_1-1 nil 3250875543 ("" (skosimp*) (("" (typepred "e!1") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (typepred "G!1") (("" (assert) (("" (inst?) (("1" (assert) (("1" (hide -2) (("1" (inst-cp -1 "x!1") (("1" (inst -1 "y!1") (("1" (expand "dbl") (("1" (case "subset?(add(x!1,singleton(y!1)),vert(G!1))") (("1" (lemma "card_subset[T]") (("1" (inst?) (("1" (rewrite "card_add") (("1" (rewrite "card_singleton") (("1" (assert) (("1" (hide -2) (("1" (expand "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (rewrite "finite_singleton") nil nil)) nil)) nil) ("2" (rewrite "finite_add") (("2" (rewrite "finite_singleton") nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) 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) (set type-eq-decl nil sets nil) (/= const-decl "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans 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) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set" finite_sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (card_singleton formula-decl nil finite_sets 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (card_add formula-decl nil finite_sets nil) (card_subset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (nil application-judgement "finite_set[T]" graphs 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 3250875543 ("" (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" graphs 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) (size const-decl "nat" graphs 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" graphs nil) (card_empty? formula-decl nil finite_sets nil) (T formal-type-decl nil graphs nil)) nil)) (singleton_graph_TCC1 0 (singleton_graph_TCC1-1 nil 3250875543 ("" (skosimp*) (("" (prop) (("1" (skosimp*) (("1" (expand "emptyset") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "singleton?") (("2" (expand "size") (("2" (rewrite "card_singleton") nil nil)) nil)) nil)) nil)) nil) ((emptyset const-decl "set" sets nil) (size const-decl "nat" graphs nil) (T formal-type-decl nil graphs nil) (card_singleton formula-decl nil finite_sets nil) (singleton? const-decl "bool" graphs nil)) nil))) ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤ |
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 |
