| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/measure_integration/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 5 kB |
|
Quelle product_sections.prf Sprache: Lisp |
|||||||||
|
(product_sections
(x_section_emptyset 0 (x_section_emptyset-1 nil 3455512524 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T2 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (emptyset const-decl "set" sets nil) (x_section const-decl "set[T2]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T1 formal-type-decl nil product_sections nil) (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (x_section_complement 0 (x_section_complement-1 nil 3455512530 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T2 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (complement const-decl "set" sets nil) (x_section const-decl "set[T2]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T1 formal-type-decl nil product_sections nil) (member const-decl "bool" sets nil)) shostak)) (x_section_union 0 (x_section_union-1 nil 3455512540 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T2 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (union const-decl "set" sets nil) (x_section const-decl "set[T2]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T1 formal-type-decl nil product_sections nil) (member const-decl "bool" sets nil)) shostak)) (x_section_intersection 0 (x_section_intersection-1 nil 3455512548 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T2 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (intersection const-decl "set" sets nil) (x_section const-decl "set[T2]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T1 formal-type-decl nil product_sections nil) (member const-decl "bool" sets nil)) shostak)) (x_section_disjoint 0 (x_section_disjoint-1 nil 3455512555 ("" (skosimp) (("" (expand "disjoint?") (("" (expand "intersection") (("" (expand "empty?") (("" (expand "member") (("" (skosimp) (("" (expand "x_section") (("" (inst - "(a!1,x!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (T2 formal-type-decl nil product_sections nil) (T1 formal-type-decl nil product_sections nil) (x_section const-decl "set[T2]" cross_product "topology/") (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil)) shostak)) (y_section_emptyset 0 (y_section_emptyset-1 nil 3455512611 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T1 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (emptyset const-decl "set" sets nil) (y_section const-decl "set[T1]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T2 formal-type-decl nil product_sections nil) (finite_emptyset name-judgement "finite_set" finite_sets nil)) shostak)) (y_section_complement 0 (y_section_complement-1 nil 3455512620 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T1 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (complement const-decl "set" sets nil) (y_section const-decl "set[T1]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T2 formal-type-decl nil product_sections nil) (member const-decl "bool" sets nil)) shostak)) (y_section_union 0 (y_section_union-1 nil 3455512630 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T1 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (union const-decl "set" sets nil) (y_section const-decl "set[T1]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T2 formal-type-decl nil product_sections nil) (member const-decl "bool" sets nil)) shostak)) (y_section_intersection 0 (y_section_intersection-1 nil 3455512637 ("" (skosimp) (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil)) nil) ((T1 formal-type-decl nil product_sections nil) (boolean nonempty-type-decl nil booleans nil) (intersection const-decl "set" sets nil) (y_section const-decl "set[T1]" cross_product "topology/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (T2 formal-type-decl nil product_sections nil) (member const-decl "bool" sets nil)) shostak)) (y_section_disjoint 0 (y_section_disjoint-1 nil 3455512644 ("" (skosimp) (("" (expand "disjoint?") (("" (expand "empty?") (("" (skosimp) (("" (inst - "(x!1,b!1)") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (y_section const-decl "set[T1]" cross_product "topology/") (T2 formal-type-decl nil product_sections nil) (T1 formal-type-decl nil product_sections nil) (empty? const-decl "bool" sets nil)) shostak))) ¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28