| products/sources/formale sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: continuity_def.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(graph_from_edges
(finite_lem 0 (finite_lem-1 nil 3375355954 ("" (skosimp) (("" (lemma "Union_finite[T]") (("" (inst -1 "ES!1") (("" (typepred "ES!1") (("" (prop) (("1" (grind) nil nil) ("2" (lemma "finite_dbl[T]") (("2" (expand "every") (("2" (hide (2 3)) (("2" (hide -2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "extend") (("2" (prop) (("2" (skosimp) (("2" (inst -3 "x!2" "y!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil graph_from_edges nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_dbl formula-decl nil doubletons nil) (nil application-judgement "finite_set[T]" graphs nil) (injective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (x!1 skolem-const-decl "(extend[setof[T], doubleton[T], bool, FALSE](ES!1))" graph_from_edges nil) (ES!1 skolem-const-decl "finite_set[doubleton[T]]" graph_from_edges nil) (y!1 skolem-const-decl "T" graph_from_edges nil) (x!2 skolem-const-decl "T" graph_from_edges nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (every const-decl "bool" sets nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "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) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (Union_to_pred 0 (Union_to_pred-1 nil 3375356366 ("" (grind) 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 graph_from_edges 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) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (injective? const-decl "bool" functions nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (setof type-eq-decl nil defined_types nil) (Union const-decl "set" sets nil)) shostak)) (pred_to_Union 0 (pred_to_Union-1 nil 3375356392 ("" (skosimp) (("" (expand "Union") (("" (skolem -1 "d!1") (("" (flatten) (("" (inst 1 "d!1") (("" (expand "extend") (("" (prop) (("" (typepred "d!1") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Union const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (ES!1 skolem-const-decl "finite_set[doubleton[T]]" graph_from_edges nil) (d!1 skolem-const-decl "doubleton[T]" graph_from_edges nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "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) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil graph_from_edges nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil)) shostak)) (verts_of_TCC1 0 (verts_of_TCC1-1 nil 3367125257 ("" (use "finite_lem") nil nil) ((finite_lem formula-decl nil graph_from_edges nil)) nil)) (verts_from_TCC1 0 (verts_from_TCC1-1 nil 3375524256 ("" (skosimp*) (("" (expand "restrict") (("" (lemma "verts_of_TCC1") (("" (inst - "ES!1") (("" (case-replace "{t: T | EXISTS (d: doubleton[T]): d(t) AND ES!1(d)} = (Union[T](extend[setof[T (("" (hide -1 2) (("" (apply-extensionality 1 :hide? t) (("" (iff 1) (("" (prop) (("1" (skosimp*) (("1" (expand "Union") (("1" (inst?) (("1" (expand "extend") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "Union") (("2" (skosimp*) (("2" (typepred "a!1") (("2" (expand "extend") (("2" (ground) (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((verts_of_TCC1 subtype-tcc nil graph_from_edges nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (d!1 skolem-const-decl "doubleton[T]" graph_from_edges nil) (ES!1 skolem-const-decl "finite_set[doubleton[T]]" graph_from_edges nil) (nil application-judgement "finite_set[T]" graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" 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) (T formal-type-decl nil graph_from_edges nil)) nil)) (verts_from_of 0 (verts_from_of-1 nil 3375527862 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "verts_of") (("" (expand "verts_from") (("" (iff 1) (("" (prop) (("1" (lemma "Union_to_pred") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "pred_to_Union") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil graph_from_edges nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (verts_from const-decl "finite_set[T]" graph_from_edges nil) (verts_of const-decl "finite_set[T]" graph_from_edges nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" 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) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (Union_to_pred formula-decl nil graph_from_edges nil) (pred_to_Union formula-decl nil graph_from_edges nil)) shostak)) (graph_from_edgeset_TCC1 0 (graph_from_edgeset_TCC1-1 nil 3367125257 ("" (skosimp) (("" (split) (("1" (use "pred_to_Union") (("1" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil) ((Union const-decl "set" sets nil) (verts_of const-decl "finite_set[T]" graph_from_edges nil) (nil application-judgement "finite_set[T]" graphs nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil graph_from_edges 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) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (pred_to_Union formula-decl nil graph_from_edges nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (member const-decl "bool" sets nil) (isolated_vert? const-decl "bool" graph_from_edges nil)) nil)) (graph_from_edgeset_rew1 0 (graph_from_edgeset_rew1-1 nil 3375356563 ("" (grind) nil nil) ((verts_of const-decl "finite_set[T]" graph_from_edges nil) (graph_from_edgeset const-decl "es_graph" graph_from_edges nil)) shostak)) (graph_from_edgeset_rew2 0 (graph_from_edgeset_rew2-1 nil 3375356569 ("" (grind) nil nil) ((verts_of const-decl "finite_set[T]" graph_from_edges nil) (graph_from_edgeset const-decl "es_graph" graph_from_edges nil)) shostak)) (no_isolated_verts 0 (no_isolated_verts-1 nil 3375356574 ("" (grind) 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 graph_from_edges 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) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (verts_of const-decl "finite_set[T]" graph_from_edges nil) (graph_from_edgeset const-decl "es_graph" graph_from_edges nil) (Union const-decl "set" sets nil) (member const-decl "bool" sets nil) (isolated_vert? const-decl "bool" graph_from_edges nil)) shostak))) ¤ Dauer der Verarbeitung: 0.23 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 |
