|
(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.19 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.
|
