| products/sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: max_subgraphs.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(max_subgraphs
(prep0 0 (prep0-1 nil 3507100594 ("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (typepred "P!1") (("" (skosimp*) (("" (inst -3 "size(S!1)") (("1" (expand "member") (("1" (expand "is_one_of_size") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "subgraph_smaller") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (Gpred type-eq-decl nil max_subgraphs nil) (pred type-eq-decl nil defined_types nil) (subgraph? const-decl "bool" subgraphs 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) (T formal-type-decl nil max_subgraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (G!1 skolem-const-decl "graph[T]" max_subgraphs nil) (S!1 skolem-const-decl "graph[T]" max_subgraphs nil) (size const-decl "nat" graphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (<= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (upto nonempty-type-eq-decl nil nat_types nil) (is_one_of_size const-decl "bool" max_subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (member const-decl "bool" sets nil) (subgraph_smaller formula-decl nil subgraphs nil) (empty? const-decl "bool" sets nil)) nil)) (max_size_TCC1 0 (max_size_TCC1-1 nil 3507100594 ("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (skosimp*) (("" (lemma "prep0") (("" (inst?) (("" (inst?) (("" (expand "nonempty?") (("" (expand "empty?") (("" (skosimp*) (("" (expand "member") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (T formal-type-decl nil max_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) (upto nonempty-type-eq-decl nil nat_types nil) (size const-decl "nat" graphs nil) (<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (pred type-eq-decl nil defined_types nil) (subgraph? const-decl "bool" subgraphs nil) (Gpred type-eq-decl nil max_subgraphs nil) (prep0 formula-decl nil max_subgraphs nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil)) nil)) (prep 0 (prep-1 nil 3507100594 ("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (expand "max_size") (("" (typepred "max({n: upto[size(G!1)] | is_one_of_size(G!1,P!1,n)})") (("1" (hide -1 -3) (("1" (expand "is_one_of_size") (("1" (skosimp*) (("1" (inst -3 "S!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "prep0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (is_one_of_size const-decl "bool" max_subgraphs nil) (Gpred type-eq-decl nil max_subgraphs nil) (subgraph? const-decl "bool" subgraphs nil) (pred type-eq-decl nil defined_types nil) (max const-decl "{a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}" max_upto nil) (upto nonempty-type-eq-decl nil nat_types nil) (size const-decl "nat" graphs 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) (T formal-type-decl nil max_subgraphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (<= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Subgraph type-eq-decl nil subgraphs nil) (prep0 formula-decl nil max_subgraphs nil) (max_size const-decl "upto[size(G)]" max_subgraphs nil) (empty? const-decl "bool" sets nil)) nil)) (max_subgraph_TCC1 0 (max_subgraph_TCC1-1 nil 3507100594 ("" (inst 1 "(LAMBDA (G: graph[T], P: Gpred(G)): choose({S: Subgraph(G) | size(S) = max_size (("1" (skosimp*) (("1" (expand "maximal?") (("1" (skosimp*) (("1" (typepred "max_size(G!1,P!1)") (("1" (hide -1) (("1" (expand "max_size") (("1" (typepred "max({n: upto[size(G!1)] | is_one_of_size(G!1,P!1,n)})") (("1" (hide -1 -2) (("1" (inst -1 "size(SS!1)") (("1" (assert) (("1" (hide -1 2) (("1" (expand "is_one_of_size") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (typepred "SS!1") (("2" (hide -2 -2) (("2" (rewrite "subgraph_smaller") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (lemma "prep") (("2" (rewrite "prep0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "prep") (("2" (inst?) nil nil)) nil)) nil)) nil) ((max const-decl "{a: upto[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}" max_upto nil) (is_one_of_size const-decl "bool" max_subgraphs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (G!1 skolem-const-decl "graph[T]" max_subgraphs nil) (SS!1 skolem-const-decl "Subgraph[T](G!1)" max_subgraphs nil) (subgraph_smaller formula-decl nil subgraphs nil) (prep formula-decl nil max_subgraphs nil) (prep0 formula-decl nil max_subgraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (max_size const-decl "upto[size(G)]" max_subgraphs nil) (upto nonempty-type-eq-decl nil nat_types nil) (<= const-decl "bool" reals nil) (size const-decl "nat" graphs nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (maximal? const-decl "bool" max_subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (Gpred type-eq-decl nil max_subgraphs nil) (subgraph? const-decl "bool" subgraphs nil) (pred type-eq-decl nil defined_types 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) (graph type-eq-decl nil graphs nil) (T formal-type-decl nil max_subgraphs nil)) nil)) (max_subgraph_def 0 (max_subgraph_def-1 nil 3507100594 ("" (skosimp*) (("" (typepred "max_subgraph(G!1, P!1)") (("" (propax) nil nil)) nil)) nil) ((max_subgraph const-decl "{S: Subgraph(G) | maximal?(G, S, P)}" max_subgraphs nil) (maximal? const-decl "bool" max_subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (Gpred type-eq-decl nil max_subgraphs nil) (subgraph? const-decl "bool" subgraphs nil) (pred type-eq-decl nil defined_types nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (graph type-eq-decl nil graphs 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 max_subgraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (max_subgraph_in 0 (max_subgraph_in-1 nil 3507100594 ("" (skosimp*) (("" (typepred "max_subgraph(G!1, P!1)") (("" (hide -1 -2) (("" (expand "maximal?") (("" (flatten) nil nil)) nil)) nil)) nil)) nil) ((max_subgraph const-decl "{S: Subgraph(G) | maximal?(G, S, P)}" max_subgraphs nil) (maximal? const-decl "bool" max_subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (Gpred type-eq-decl nil max_subgraphs nil) (subgraph? const-decl "bool" subgraphs nil) (pred type-eq-decl nil defined_types nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (graph type-eq-decl nil graphs 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 max_subgraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (max_subgraph_is_max 0 (max_subgraph_is_max-1 nil 3507100594 ("" (skosimp*) (("" (typepred "max_subgraph(G!1, P!1)") (("" (hide -1 -2) (("" (expand "maximal?") (("" (flatten) (("" (hide -1) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((max_subgraph const-decl "{S: Subgraph(G) | maximal?(G, S, P)}" max_subgraphs nil) (maximal? const-decl "bool" max_subgraphs nil) (Subgraph type-eq-decl nil subgraphs nil) (Gpred type-eq-decl nil max_subgraphs nil) (subgraph? const-decl "bool" subgraphs nil) (pred type-eq-decl nil defined_types nil) (pregraph type-eq-decl nil graphs nil) (finite_set type-eq-decl nil finite_sets nil) (graph type-eq-decl nil graphs 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 max_subgraphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil))) ¤ Dauer der Verarbeitung: 0.31 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 |
