| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle lattices.prf Sprache: Lisp |
|||||||||
|
(lattices
(finite_set_is_tightly_bounded 0 (finite_set_is_tightly_bounded-1 nil 3314557049 ("" (skolem!) (("" (typepred "<=") (("" (expand* "tightly_bounded?" "lattice?") (("" (prop) (("1" (expand "upper_semilattice?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil) ("2" (expand "lower_semilattice?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= formal-const-decl "(lattice?[T])" lattices nil) (lattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil lattices nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (upper_semilattice? const-decl "bool" bounded_orders nil) (lower_semilattice? const-decl "bool" bounded_orders nil) (tightly_bounded? const-decl "bool" bounded_orders nil)) nil)) (add_preserves_tightly_bounded 0 (add_preserves_tightly_bounded-1 nil 3314627436 ("" (skolem-typepred) (("" (expand "tightly_bounded?") (("" (ground) nil nil)) nil)) nil) ((add_preserves_greatest_bounded_below application-judgement "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" lattices nil) (add_preserves_bounded_below application-judgement "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lattices nil) (add_preserves_least_bounded_above application-judgement "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))" lattices nil) (add_preserves_bounded_above application-judgement "(LAMBDA (S: set[T]): bounded_above?(S, <=))" lattices nil) (<= formal-const-decl "(lattice?[T])" lattices nil) (lattice? const-decl "bool" bounded_orders nil) (tightly_bounded? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil lattices nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (union_preserves_tightly_bounded 0 (union_preserves_tightly_bounded-1 nil 3314627436 ("" (skolem-typepred) (("" (expand "tightly_bounded?") (("" (ground) nil nil)) nil)) nil) ((union_preserves_greatest_bounded_below application-judgement "(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" lattices nil) (union_preserves_bounded_below application-judgement "(LAMBDA (S: set[T]): bounded_below?(S, <=))" lattices nil) (union_preserves_least_bounded_above application-judgement "(LAMBDA (S: set[T]): least_bounded_above?(S, <=))" lattices nil) (union_preserves_bounded_above application-judgement "(LAMBDA (S: set[T]): bounded_above?(S, <=))" lattices nil) (<= formal-const-decl "(lattice?[T])" lattices nil) (lattice? const-decl "bool" bounded_orders nil) (tightly_bounded? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil lattices nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil))) ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28