| products/Sources/formale Sprachen/PVS/digraphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: min_walk_reduced.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(indexed_sets_aux
(disjoint_indexed_set_TCC1 0 (disjoint_indexed_set_TCC1-1 nil 3321840714 ("" (expand "disjoint?") (("" (skosimp*) (("" (expand "emptyset") (("" (expand "disjoint?") (("" (expand "intersection") (("" (expand "empty?") (("" (expand "member") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (emptyset const-decl "set" sets nil) (disjoint? const-decl "bool" indexed_sets_aux nil)) shostak)) (IComplement_IComplement 0 (IComplement_IComplement-1 nil 3314370637 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (expand "IComplement") (("" (rewrite "complement_complement") nil nil)) nil)) nil)) nil) ((index formal-type-decl nil indexed_sets_aux nil) (T formal-type-decl nil indexed_sets_aux nil) (boolean nonempty-type-decl nil booleans nil) (IComplement const-decl "set[T]" indexed_sets_aux nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (complement_complement formula-decl nil sets_lemmas nil)) shostak)) (IDemorgan1 0 (IDemorgan1-1 nil 3314357924 ("" (skosimp) (("" (rewrite "IUnion_Union") (("" (rewrite "IIntersection_Intersection") (("" (expand "fullset") (("" (expand "image") (("" (expand "image") (("" (expand "IComplement") (("" (expand "Union") (("" (expand "Intersection") (("" (expand "complement") (("" (apply-extensionality :hide? t) (("" (expand "member") (("" (case-replace "(FORALL (a: ({y: set[T] | EXISTS (x_1: ({x: index | TRUE})): y = complement(A!1(x_1))})): a(x!1)) ") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (inst - "complement(a!1)") (("1" (expand "complement") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "x!2") (("2" (expand "complement") (("2" (apply-extensionality :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "A!1(x!2)") (("1" (replace -1) (("1" (expand "complement") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IUnion_Union formula-decl nil indexed_sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (index formal-type-decl nil indexed_sets_aux nil) (T formal-type-decl nil indexed_sets_aux nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (fullset const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (Union const-decl "set" sets nil) (complement const-decl "set" sets nil) (x!2 skolem-const-decl "({x: index | TRUE})" indexed_sets_aux nil) (a!1 skolem-const-decl "({y: set[T] | EXISTS (x_1: ({x | TRUE})): y = A!1(x_1)})" indexed_sets_aux nil) (A!1 skolem-const-decl "[index -> set[T]]" indexed_sets_aux nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (Intersection const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (IComplement const-decl "set[T]" indexed_sets_aux nil) (IIntersection_Intersection formula-decl nil indexed_sets nil)) shostak)) (IDemorgan2 0 (IDemorgan2-1 nil 3314358248 ("" (skosimp) (("" (rewrite "IUnion_Union") (("" (rewrite "IIntersection_Intersection") (("" (expand "fullset") (("" (expand "IComplement") (("" (expand "complement") (("" (expand "image") (("" (expand "image") (("" (expand "Intersection") (("" (expand "Union") (("" (expand "member") (("" (apply-extensionality :hide? t) (("" (case-replace "(EXISTS (a: ({y: set[T] | EXISTS (x_1: ({x: index | TRUE})): y = ({x: T | NOT member(x, A!1(x_1))})})): a(x!1))") (("1" (skosimp) (("1" (typepred "a!1") (("1" (skosimp) (("1" (inst - "complement(a!1)") (("1" (expand "complement") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "x!2") (("2" (replace -1) (("2" (expand "complement") (("2" (expand "member") (("2" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (skosimp) (("2" (inst + "complement(a!1)") (("1" (expand "complement") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil) ("2" (inst + "x!2") (("2" (apply-extensionality :hide? t) (("2" (expand "complement") (("2" (expand "member") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((IUnion_Union formula-decl nil indexed_sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (IComplement const-decl "set[T]" indexed_sets_aux nil) (index formal-type-decl nil indexed_sets_aux nil) (T formal-type-decl nil indexed_sets_aux nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (fullset const-decl "set" sets nil) (complement const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (Union const-decl "set" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (a!1 skolem-const-decl "({y: set[T] | EXISTS (x_1: ({x | TRUE})): y = A!1(x_1)})" indexed_sets_aux nil) (a!1 skolem-const-decl "({y: set[T] | EXISTS (x_1: ({x: index | TRUE})): y = ({x: T | NOT member(x, A!1(x_1))})})" indexed_sets_aux nil) (A!1 skolem-const-decl "[index -> set[T]]" indexed_sets_aux nil) (member const-decl "bool" sets nil) (Intersection const-decl "set" sets nil) (image const-decl "set[R]" function_image nil) (Intersection_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (IIntersection_Intersection formula-decl nil indexed_sets nil)) shostak))) ¤ Dauer der Verarbeitung: 0.4 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 |
