(lower_semilatticesnil 3315157450"" (skolem!)"" (typepred "<=" )"" (expand "lower_semilattice?" )"" (flatten) (("" (inst?) nil nil )) nil )) nil ))nil ))nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )nil defined_types nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil ))nil ))nil 3315157495"" (skolem!)"" (expand "greatest_lower_bound?" )"" (split)"1" (typepred "<=" )"1" expand * "singleton" "lower_bound?" "lower_semilattice?" "partial_order?" "preorder?" "reflexive?" )"1" (skosimp :preds? t)"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skosimp)"2" (expand * "singleton" "lower_bound?" )"2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )nil defined_types nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"(singleton?)" sets nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )"bool" bounded_orders nil ))nil 3315157548"" (skolem!)"" (invoke (typepred "%1" ) (! 1 l))"" (rewrite "unique_greatest_lower_bound" )"" (rewrite "greatest_lower_bound_singleton" ) nil nil )) nil ))nil ))nil )"non_empty_finite_set[T]" lower_semilattices nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil lower_semilattices nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" sets nil )"(singleton?)" sets nil )nil lower_semilatticesnil )"bool" relations nil )nil defined_types nil )nil bounded_orders nil ))nil 3315157580"" (skolem!)"" (expand "glb" )"" (invoke (typepred "%1" ) (! 1 l r))"" (invoke (name-replace "L" "%1" ) (! 1 l r))"" (typepred "<=" )"" (expand "greatest_lower_bound?" )"" (prop)"1" (hide -4)"1" (expand "lower_bound?" )"1" (inst - "t!1" )"1" expand * "lower_semilattice?" "partial_order?" "preorder?" "transitive?" )"1" (flatten)"1" (inst - "s!1" "L" "t!1" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand * "union" "singleton" "member" ) nil nil ))nil ))nil ))nil )"2" (hide -4)"2" (expand "lower_bound?" )"2" (inst - "u!1" )"1" expand * "lower_semilattice?" "partial_order?" "preorder?" "transitive?" )"1" (flatten)"1" (inst - "s!1" "L" "u!1" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (expand * "union" "singleton" "member" ) nil nil ))nil ))nil ))nil )"3" (hide -4)"3" (inst - "s!1" )"3" (assert )"3" expand * "union" "singleton" "member" "lower_bound?" )"3" (skolem-typepred)"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" lower_semilattices nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"T" lower_semilattices nil )"T" lower_semilattices nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )"bool" sets nil )"bool" bounded_orders nil )"(singleton?)" sets nil )"bool" sets nil )"set" sets nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"non_empty_finite_set[T]" lower_semilattices nil ))nil 3315157701"" (skosimp)"" (expand "glb" )"" (invoke (typepred "%1" ) (! 1 l))"" (invoke (name-replace "L" "%1" ) (! 1 l))"" (expand * "greatest_lower_bound?" "lower_bound?" )"" (flatten)"" (inst - "t!1" )"1" (typepred "<=" )"1" expand * "lower_semilattice?" "partial_order?" "preorder?" "transitive?" )"1" (flatten)"1" (inst - "L" "t!1" "s!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand * "union" "singleton" "member" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" lower_semilattices nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )"T" lower_semilattices nil )"T" lower_semilattices nil )"bool" bounded_orders nil )"(singleton?)" sets nil )"bool" sets nil )"set" sets nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"non_empty_finite_set[T]" lower_semilattices nil ))nil 3315157757"" (skosimp)"" (expand "glb" )"" (invoke (typepred "%1" ) (! 1 l))"" (invoke (name-replace "L" "%1" ) (! 1 l))"" (expand * "greatest_lower_bound?" "lower_bound?" )"" (flatten)"" (inst - "u!1" )"1" (typepred "<=" )"1" expand * "lower_semilattice?" "partial_order?" "preorder?" "transitive?" )"1" (flatten)"1" (inst - "L" "u!1" "s!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand * "union" "singleton" "member" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" lower_semilattices nil )"[T, T -> boolean]" equalities nil )"bool" sets nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )"T" lower_semilattices nil )"T" lower_semilattices nil )"bool" bounded_orders nil )"(singleton?)" sets nil )"bool" sets nil )"set" sets nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"non_empty_finite_set[T]" lower_semilattices nil ))nil 3315157450"" (skolem-typepred)"" (expand "bounded_below?" )"" (skosimp*)"" (inst + "glb(t!1, t!2)" )"" (expand "lower_bound?" )"" (skolem-typepred)"" (expand * "union" "member" )"" (inst?)"1" (rewrite "glb_le_1" ) nil nil )"2" (assert )"2" (inst?) (("2" (rewrite "glb_le_2" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" lower_semilattices nil )"set" sets nil )"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilatticesnil )"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilatticesnil )"(union[T](S1!1, S2!1))" lower_semilatticesnil )nil lower_semilattices nil )nil lower_semilattices nil )"bool" sets nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315157450"" (skolem-typepred)"" (rewrite "add_as_union" )"" (rewrite "union_preserves_bounded_below" ) nil nil )) nil ))nil )nil sets_lemmas nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilatticesnil )nil lower_semilatticesnil )"bool" sets nil )"(singleton?)" sets nil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315157910"" (skosimp)"" (expand "greatest_lower_bound?" )"" (prop)"1" (hide -4 -2)"1" (expand "lower_bound?" )"1" (skolem-typepred)"1" (expand * "union" "member" )"1" (inst - "r!1" )"1" (rewrite "glb_le_1" ) nil nil )"2" (assert )"2" (inst - "r!1" )"2" (rewrite "glb_le_2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (rewrite "le_glb" )"2" (split)"1" (hide -5 -4 -2)"1" (inst?)"1" (assert )"1" (expand "lower_bound?" )"1" (skolem!)"1" (inst - "r!2" )"1" (expand * "union" "member" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -4 -3 -2)"2" (inst?)"2" (assert )"2" (expand "lower_bound?" )"2" (skolem!)"2" (inst - "r!2" )"2" (expand * "union" "member" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"(S1!1)" lower_semilattices nil )"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilatticesnil )"(S2!1)" lower_semilattices nil )nil lower_semilattices nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil lower_semilattices nil )set type-eq-decl nil sets nil ) (union const-decl "set" sets nil )nil defined_types nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" nil )"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" nil )"(union(S1!1, S2!1))" lower_semilatticesnil )nil lower_semilattices nil )nil lower_semilattices nil )"bool" sets nil )"bool" bounded_orders nil ))nil 3315158032"" (skosimp)"" (rewrite "add_as_union" )"" (rewrite "greatest_lower_bound_union" )"" (rewrite "greatest_lower_bound_singleton" ) nil nil )) nil ))nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )nil lower_semilattices nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilatticesnil )nil lower_semilatticesnil )nil lower_semilatticesnil )"bool" sets nil )"(singleton?)" sets nil ))nil 3315157450"" (skolem-typepred)"" (expand "greatest_bounded_below?" )"" (skosimp*)"" (inst + "glb(t!1, t!2)" )"" (rewrite "greatest_lower_bound_union" ) nil nil )) nil ))nil ))nil ))nil )"T" lower_semilattices nil )nil lower_semilatticesnil )"(lower_semilattice?[T])" lower_semilatticesnil )"bool" bounded_orders nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil lower_semilattices nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315157450"" (skolem!)"" (rewrite "add_as_union" )"" (rewrite "union_preserves_greatest_bounded_below" ) nil nil ))nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )nil lower_semilattices nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" nil )nil nil )"bool" sets nil )"(singleton?)" sets nil ))nil ))nil 3315158151"" (skolem!)"" (invoke (typepred "%1" "%2" "%3" ) (! 1 l) (! 1 r 1) (! 1 r 2))"" (invoke (name-replace "GU" "%1" ) (! 1 l))"" (invoke (name-replace "G1" "%1" ) (! 1 r 1))"" (invoke (name-replace "G2" "%1" ) (! 1 r 2))"" (use "greatest_lower_bound_union" )"" (assert )"" (use "unique_greatest_lower_bound" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil lower_semilattices nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )"set" sets nil )nil lower_semilatticesnil )nil defined_types nil )"bool" relations nil )"T" lower_semilattices nil )nil bounded_orders nil )"[T, T -> boolean]" equalities nil ))nil 3315158200"" (skolem!)"" (rewrite "add_as_union" )"" (rewrite "glb_union" )"" (rewrite "glb_singleton" ) nil nil )) nil ))nil ))nil )nil sets_lemmas nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"(lower_semilattice?[T])" lower_semilatticesnil )nil lower_semilattices nil )"non_empty_finite_set[T]" lower_semilattices nil )"(nonempty?)" nil )"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))" nil )nil lower_semilattices nil )nil lower_semilattices nil )"bool" sets nil )"(singleton?)" sets nil ))quality 100%
¤ 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.0.21Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
