(pointwise_ordersnil 3314638777"" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil pointwise_orders nil )nil defined_types nil )nil pointwise_orders nil )"bool" pointwise_orders nil )"bool" relations nil ))nil ))nil 3314638777"" (skolem-typepred)"" (expand * "transitive?" "pointwise" )"" (skosimp*)"" (inst - "x!1(x!2)" "y!1(x!2)" "z!1(x!2)" )"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" pointwise_orders nil )nil pointwise_orders nil )"bool" relations nil )nil defined_types nil )nil pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3314638777"" (judgement-tcc) nil nil )"(transitive?[[D -> R]])" pointwise_orders nil )"(reflexive?[[D -> R]])" pointwise_orders nil )"bool" orders nil ))nil ))nil 3314638777"" (skolem-typepred)"" (expand * "antisymmetric?" "pointwise" )"" (skosimp*)"" (decompose-equality)"" (inst?)"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" pointwise_orders nil )nil pointwise_orders nil )"bool" relations nil )nil defined_types nil )nil pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3314638777"" (judgement-tcc) nil nil )"(antisymmetric?[[D -> R]])" pointwise_orders nil )"(preorder?[[D -> R]])" pointwise_orders nil )"bool" orders nil ))nil ))nil 3314639098"" (skolem!)"" (split)"1" (typepred "nff!1" )"1" (expand * "nonempty?" "empty?" "member" )"1" (skolem!)"1" (inst - "x!2(x!1)" ) (("1" (inst?) nil nil )) nil ))nil ))nil ))nil )"2" "{s | EXISTS f: nff!1(f) & s = f(x!1)} = image(LAMBDA f: f(x!1), nff!1)" )"1" (rewrite "finite_image" ) nil nil )"2" (hide 2)"2" (decompose-equality)"2" (expand "image" )"2" (iff)"2" (prop)"1" (skosimp* t) (("1" (inst?) nil nil )) nil )"2" (skolem-typepred)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil pointwise_orders nil )nil pointwise_orders nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"[D -> R]" pointwise_orders nil )"non_empty_finite_set[[D -> R]]" nil )nil function_image_aux nil )"set[R]" function_image nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"finite_set[R]" nil ))nil 3314639347"" (skolem!)"" (prop)"1" (skolem!)"1" (expand "least_upper_bound?" )"1" (prop)"1" (hide -2)"1" (expand "upper_bound?" )"1" (skosimp* t)"1" (inst?)"1" (expand "pointwise" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" "LAMBDA x: IF x = x!1 THEN r!1 ELSE f1!1(x) ENDIF" )"2" (split)"1" (expand "pointwise" -1) (("1" (inst?) nil nil ))nil )"2" (expand "upper_bound?" )"2" (skolem-typepred)"2" (inst? -3)"2" (inst - "r!2(x!1)" )"1" (expand "pointwise" )"1" (skolem!)"1" "1" "1" (assert ) nil nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "least_upper_bound?" +)"2" (split)"1" expand * "pointwise" "least_upper_bound?" "upper_bound?" )"1" (skosimp* t)"1" (inst?)"1" (flatten)"1" (inst?) (("1" (inst? +) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (expand "pointwise" + :occurrence 2)"2" (skosimp*)"2" (inst?)"2" (expand "least_upper_bound?" )"2" (flatten)"2" (hide -2)"2" (inst?)"2" (assert )"2" (expand "upper_bound?" )"2" (skosimp* t)"2" "2" expand "pointwise" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"D" pointwise_orders nil )"(ff!1)" pointwise_orders nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil pointwise_orders nil )nil pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" pointwise_orders nil )"[D -> R]" pointwise_orders nil )"set[[D -> R]]" pointwise_orders nil )"bool" bounded_orders nil )"(ff!1)" pointwise_orders nil )"D" pointwise_orders nil )"[D -> R]" pointwise_orders nil ))nil 3314640074"" (skolem!)"" (expand "least_bounded_above?" )"" (prop)"1" (skosimp*)"1" (inst + "t!1(x!1)" )"1" (rewrite "least_upper_bound_pointwise" )"1" (inst?) nil nil )) nil ))nil ))nil )"2" (rewrite "skolemize_exists" )"2" (skolem!)"2" (use "least_upper_bound_pointwise" )"2" (replace *)"2" (assert ) (("2" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )nil skolemization nil )"bool" bounded_orders nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil pointwise_orders nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil pointwise_orders nil )nil pointwise_orders nil ))nil 3314638777"" (expand "upper_semilattice?" )"" (skosimp* t)"" (rewrite "least_bounded_above_pointwise" )"" (skolem!)"" (rewrite "all_finite_least_bounded" )"" (use "finiteness_lemma" )"" (expand "nonempty?" ) (("" (prop) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil defined_types nil )nil pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil pointwise_orders nil )nil pointwise_orders nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil bounded_orders nil )nil pointwise_ordersnil )"bool" bounded_orders nil )"(partial_order?[[D -> R]])" pointwise_orders nil ))nil ))nil 3314638777"" (expand "complete_upper_semilattice?" )"" (skolem-typepred)"" (rewrite "pointwise_preserves_partial_order" )"" (skolem!)"" (rewrite "least_bounded_above_pointwise" )"" (skolem!) (("" (rewrite "all_least_bounded" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil pointwise_orders nil )nil defined_types nil )nil bounded_orders nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil pointwise_ordersnil )nil pointwise_orders nil )set type-eq-decl nil sets nil )"bool" orders nil )nil nil )"bool" bounded_orders nil )"(upper_semilattice?[[D -> R]])" pointwise_orders nil ))nil ))nil 3314640323"" (skolem!)"" (prop)"1" (skolem!)"1" (expand "greatest_lower_bound?" )"1" (prop)"1" (hide -2)"1" (expand * "lower_bound?" "pointwise" )"1" (skosimp* t)"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (skosimp)"2" "LAMBDA x: IF x = x!1 THEN r!1 ELSE f1!1(x) ENDIF" )"2" (split)"1" (expand "pointwise" -1) (("1" (inst?) nil nil ))nil )"2" (expand "lower_bound?" )"2" (skolem-typepred)"2" (inst? -3)"2" (inst - "r!2(x!1)" )"1" (expand "pointwise" )"1" (skolem!)"1" "1" "1" (inst?) nil nil ))nil ))nil ))nil ))nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "greatest_lower_bound?" +)"2" (split)"1" expand * "greatest_lower_bound?" "lower_bound?" "pointwise" )"1" (skosimp* t)"1" (inst?)"1" (flatten)"1" (inst?) (("1" (inst? +) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (expand "pointwise" + :occurrence 2)"2" (skosimp*)"2" (inst?)"2" (expand "greatest_lower_bound?" )"2" (flatten)"2" (hide -2)"2" (inst?)"2" (assert )"2" (expand "lower_bound?" )"2" (skosimp* t)"2" "2" expand "pointwise" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"D" pointwise_orders nil )"(ff!1)" pointwise_orders nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil pointwise_orders nil )nil pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[D -> R]" pointwise_orders nil )"set[[D -> R]]" pointwise_orders nil )"bool" bounded_orders nil )"bool" pointwise_orders nil )"(ff!1)" pointwise_orders nil )"D" pointwise_orders nil )"[D -> R]" pointwise_orders nil ))nil 3314640605"" (skolem!)"" (expand "greatest_bounded_below?" )"" (prop)"1" (skosimp*)"1" (inst + "t!1(x!1)" )"1" (rewrite "greatest_lower_bound_pointwise" )"1" (inst?) nil nil )) nil ))nil ))nil )"2" (rewrite "skolemize_exists" )"2" (skolem!)"2" (use "greatest_lower_bound_pointwise" )"2" (replace *)"2" (assert ) (("2" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )nil skolemization nil )"bool" bounded_orders nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"(antisymmetric?[[D -> R]])" pointwise_orders nil )nil pointwise_ordersnil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil defined_types nil )"bool" relations nil )nil pointwise_orders nil )nil pointwise_orders nil ))nil 3314638777"" (expand "lower_semilattice?" )"" (skosimp* t)"" (rewrite "greatest_bounded_below_pointwise" )"" (skolem!)"" (rewrite "all_finite_greatest_bounded" )"" (use "finiteness_lemma" )"" (expand "nonempty?" ) (("" (prop) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil defined_types nil )nil pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil pointwise_orders nil )nil pointwise_orders nil )"bool" sets nil )nil bounded_orders nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"bool" relations nil )nil defined_types nil )nil pointwise_ordersnil )"bool" bounded_orders nil )"(partial_order?[[D -> R]])" pointwise_orders nil ))nil ))nil 3314638777"" (expand "complete_lower_semilattice?" )"" (skolem-typepred)"" (rewrite "pointwise_preserves_partial_order" )"" (skolem!)"" (rewrite "greatest_bounded_below_pointwise" )"" (skolem!)"" (rewrite "all_greatest_bounded" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil pointwise_orders nil )nil defined_types nil )nil bounded_orders nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil pointwise_orders nil )"bool" relations nil )nil defined_types nil )nil pointwise_ordersnil )"bool" orders nil )nil nil )"bool" bounded_orders nil )"(lower_semilattice?[[D -> R]])" pointwise_orders nil ))nil ))nil 3314638777"" (judgement-tcc) nil nil )"(upper_semilattice?[[D -> R]])" pointwise_orders nil )"(lower_semilattice?[[D -> R]])" pointwise_orders nil )"bool" bounded_orders nil ))nil ))nil 3314638777"" (judgement-tcc) nil nil )"(complete_upper_semilattice?[[D -> R]])" nil )"(lattice?[[D -> R]])" pointwise_orders nil )"(complete_lower_semilattice?[[D -> R]])" nil )"bool" bounded_orders nil ))nil ))nil 3314638777"" (skosimp)"" (rewrite "least_bounded_above_pointwise" ) nil nil )) nil )nil pointwise_ordersnil )nil pointwise_orders nil )nil pointwise_orders nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )nil defined_types nil )"bool" relations nil ))nil ))nil 3314638777 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil pointwise_orders nil )nil defined_types nil )"bool" relations nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"bool" bounded_orders nil ))nil ))nil 3314640889"" (skosimp)"" (invoke (name-replace "L" "%1" :hide? nil ) (! 1 2))"" (rewrite "lub_def[[D -> R]]" )"" (rewrite "least_upper_bound_pointwise" )"" (skolem!)"" (decompose-equality)"" (inst?) (("" (rewrite "lub_def[R]" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(LAMBDA (t): least_upper_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"bool" relations nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil pointwise_orders nil )nil pointwise_orders nil )nil pointwise_orders nil )"[bool, bool -> bool]" booleans nil )"bool" pointwise_orders nil )nil bounded_orders nil )"(antisymmetric?[[D -> R]])" pointwise_orders nil ))nil 3314638777"" (skosimp)"" (rewrite "greatest_bounded_below_pointwise" ) nil nil )) nil )nil pointwise_ordersnil )nil pointwise_orders nil )nil booleans nil )nil booleans nil )nil defined_types nil )"bool" relations nil )nil pointwise_orders nil )set type-eq-decl nil sets nil ))nil ))nil 3314638777 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil pointwise_orders nil )nil defined_types nil )"bool" relations nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"bool" bounded_orders nil ))nil ))nil 3314641025"" (skosimp)"" (invoke (name-replace "L" "%1" :hide? nil ) (! 1 2))"" (rewrite "glb_def[[D -> R]]" )"" (rewrite "greatest_lower_bound_pointwise" )"" (skolem!)"" (decompose-equality)"" (inst?) (("" (rewrite "glb_def[R]" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"bool" relations nil )nil defined_types nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" bounded_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil pointwise_orders nil )nil pointwise_orders nil )nil pointwise_ordersnil )"[bool, bool -> bool]" booleans nil )"bool" pointwise_orders nil )nil bounded_orders nil )"(antisymmetric?[[D -> R]])" pointwise_orders nil ))quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.7Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
