|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
csequence_subsequence.pvs
Sprache: Lisp
Original von: PVS©
|
|
|
(sets_lemmas_aux
(union_complement 0
(union_complement-1 nil 3313990217
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (expand "complement")
(("" (expand "union")
(("" (expand "fullset")
(("" (flatten)
(("" (expand "member") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil sets_lemmas_aux nil)
(boolean nonempty-type-decl nil booleans nil)
(fullset const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(member const-decl "bool" sets nil))
shostak))
(intersection_complement 0
(intersection_complement-1 nil 3313990250
("" (skosimp)
(("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
nil)
((T formal-type-decl nil sets_lemmas_aux nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(member const-decl "bool" sets nil))
shostak))
(disjoint_complement 0
(disjoint_complement-1 nil 3322194982
("" (skosimp)
(("" (lemma "intersection_complement" ("a" "a!1"))
(("" (expand "disjoint?")
(("" (rewrite "emptyset_is_empty?") nil nil)) nil))
nil))
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 sets_lemmas_aux nil)
(intersection_complement formula-decl nil sets_lemmas_aux nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(intersection const-decl "set" sets nil)
(complement const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil))
shostak))
(disjoint_commutative 0
(disjoint_commutative-1 nil 3314018116
("" (expand "disjoint?")
(("" (skosimp) (("" (rewrite "intersection_commutative") nil nil))
nil))
nil)
((T formal-type-decl nil sets_lemmas_aux nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(intersection_commutative formula-decl nil sets_lemmas nil)
(disjoint? const-decl "bool" sets nil))
shostak))
(disjoint_empty 0
(disjoint_empty-1 nil 3314018543
("" (skosimp)
(("" (expand "disjoint?")
(("" (expand "intersection")
(("" (expand "empty?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "emptyset") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_intersection1 application-judgement "finite_set"
finite_sets nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(intersection const-decl "set" sets nil))
shostak))
(powerset_fullset 0
(powerset_fullset-1 nil 3321769783
("" (skosimp)
(("" (lemma "subset_powerset" ("a" "a!1" "b" "a!1"))
(("" (rewrite "subset_reflexive") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-type-decl nil sets_lemmas_aux nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset_powerset formula-decl nil sets_lemmas nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas_aux nil)
(subset_reflexive formula-decl nil sets_lemmas nil))
shostak))
(union_diff_inter 0
(union_diff_inter-1 nil 3321854850
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (expand "difference")
(("" (expand "intersection")
(("" (expand "union")
(("" (expand "member")
(("" (case-replace "a!1(x!1)")
(("1" (flatten) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil sets_lemmas_aux nil)
(boolean nonempty-type-decl nil booleans nil)
(intersection const-decl "set" sets nil)
(difference const-decl "set" sets nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(member const-decl "bool" sets nil))
shostak))
(disjoint_diff_inter 0
(disjoint_diff_inter-1 nil 3321854884
("" (skosimp)
(("" (expand "disjoint?")
(("" (expand "intersection")
(("" (expand "difference")
(("" (expand "empty?")
(("" (expand "member") (("" (skosimp*) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((disjoint? const-decl "bool" sets nil)
(difference const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil))
shostak))
(disjoint_member 0
(disjoint_member-1 nil 3321935681
("" (expand "disjoint?")
(("" (expand "intersection")
(("" (expand "empty?")
(("" (expand "member")
(("" (skosimp*)
(("" (inst - "x!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(T formal-type-decl nil sets_lemmas_aux nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil))
shostak)))
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
