|
(upper_semilattices
(finite_set_is_least_bounded_above 0
(finite_set_is_least_bounded_above-1 nil 3314553924
("" (skolem!)
(("" (typepred "<=")
(("" (expand "upper_semilattice?")
(("" (flatten) (("" (inst?) nil nil)) nil)) nil))
nil))
nil)
((<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil upper_semilattices 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))
nil))
(least_upper_bound_singleton 0
(least_upper_bound_singleton-1 nil 3314553965
("" (skolem!)
(("" (expand* "least_upper_bound?" "upper_bound?")
(("" (split)
(("1" (typepred "<=")
(("1"
(expand* "upper_semilattice?" "partial_order?" "preorder?"
"reflexive?")
(("1" (skosimp :preds? t)
(("1" (expand "singleton")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst - "t!1")
(("2" (expand "singleton") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(t!1 skolem-const-decl "T" upper_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil upper_semilattices 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)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(preorder? const-decl "bool" orders nil)
(reflexive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil))
shostak))
(lub_singleton 0
(lub_singleton-1 nil 3314554034
("" (skolem!)
(("" (invoke (typepred "%1") (! 1 l))
(("" (rewrite "unique_least_upper_bound")
(("" (rewrite "least_upper_bound_singleton") nil nil)) nil))
nil))
nil)
((nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil upper_semilattices nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(least_upper_bound_singleton formula-decl nil upper_semilattices
nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(unique_least_upper_bound formula-decl nil bounded_orders nil))
shostak))
(lub_le 0
(lub_le-1 nil 3314554072
("" (skolem!)
(("" (expand "lub")
(("" (invoke (typepred "%1") (! 1 l l))
(("" (invoke (name-replace "L" "%1") (! 1 l l))
(("" (expand "least_upper_bound?")
(("" (typepred "<=")
(("" (prop)
(("1" (hide -4)
(("1" (expand "upper_bound?")
(("1" (inst - "t!1")
(("1"
(expand* "upper_semilattice?" "partial_order?"
"preorder?" "transitive?")
(("1" (flatten)
(("1" (inst - "t!1" "L" "s!1")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (expand* "union" "singleton" "member") nil
nil))
nil))
nil))
nil)
("2" (hide -4)
(("2" (expand "upper_bound?")
(("2" (inst - "u!1")
(("1"
(expand* "upper_semilattice?" "partial_order?"
"preorder?" "transitive?")
(("1" (flatten)
(("1" (inst - "u!1" "L" "s!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 "upper_bound?")
(("3" (skolem-typepred)
(("3" (expand* "union" "singleton" "member")
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lub const-decl "T" upper_semilattices nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(t!1 skolem-const-decl "T" upper_semilattices nil)
(u!1 skolem-const-decl "T" upper_semilattices nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(member const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(least_upper_bound? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonempty_finite_union1 application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil))
shostak))
(le_lub_1 0
(le_lub_1-1 nil 3314554256
("" (skosimp)
(("" (expand "lub")
(("" (invoke (typepred "%1") (! 1 r))
(("" (invoke (name-replace "L" "%1") (! 1 r))
(("" (expand "least_upper_bound?")
(("" (flatten)
(("" (hide -2)
(("" (expand "upper_bound?")
(("" (inst - "t!1")
(("1" (typepred "<=")
(("1"
(expand* "upper_semilattice?" "partial_order?"
"preorder?" "transitive?")
(("1" (flatten)
(("1" (inst - "s!1" "t!1" "L")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand* "union" "singleton" "member") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lub const-decl "T" upper_semilattices nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(member const-decl "bool" sets nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(u!1 skolem-const-decl "T" upper_semilattices nil)
(t!1 skolem-const-decl "T" upper_semilattices nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(least_upper_bound? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonempty_finite_union1 application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil))
shostak))
(le_lub_2 0
(le_lub_2-1 nil 3314554321
("" (skosimp)
(("" (expand "lub")
(("" (invoke (typepred "%1") (! 1 r))
(("" (invoke (name-replace "L" "%1") (! 1 r))
(("" (expand "least_upper_bound?")
(("" (flatten)
(("" (hide -2)
(("" (expand "upper_bound?")
(("" (inst - "u!1")
(("1" (typepred "<=")
(("1"
(expand* "upper_semilattice?" "partial_order?"
"preorder?" "transitive?")
(("1" (flatten)
(("1" (inst - "s!1" "u!1" "L")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (expand* "union" "singleton" "member") nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lub const-decl "T" upper_semilattices nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(member const-decl "bool" sets nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(u!1 skolem-const-decl "T" upper_semilattices nil)
(t!1 skolem-const-decl "T" upper_semilattices nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(least_upper_bound? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonempty_finite_union1 application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil))
shostak))
(union_preserves_bounded_above 0
(union_preserves_bounded_above-1 nil 3314553924
("" (skolem-typepred)
(("" (expand "bounded_above?")
(("" (skosimp*)
(("" (inst + "lub(t!1, t!2)")
(("" (expand "upper_bound?")
(("" (skolem-typepred)
(("" (expand* "union" "member")
(("" (split)
(("1" (inst?) (("1" (rewrite "le_lub_1") nil nil))
nil)
("2" (inst? -3) (("2" (rewrite "le_lub_2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((lub const-decl "T" upper_semilattices nil)
(union const-decl "set" sets nil)
(le_lub_1 formula-decl nil upper_semilattices nil)
(r!1 skolem-const-decl "(union[T](S1!1, S2!1))" upper_semilattices
nil)
(S2!1 skolem-const-decl
"(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
nil)
(S1!1 skolem-const-decl
"(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
nil)
(le_lub_2 formula-decl nil upper_semilattices nil)
(member const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(bounded_above? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(add_preserves_bounded_above 0
(add_preserves_bounded_above-1 nil 3314553924
("" (skolem-typepred)
(("" (rewrite "add_as_union")
(("" (rewrite "union_preserves_bounded_above") nil nil)) nil))
nil)
((add_as_union formula-decl nil sets_lemmas nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(union_preserves_bounded_above application-judgement
"(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
nil)
(union_preserves_bounded_above judgement-tcc nil upper_semilattices
nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(bounded_above? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(least_upper_bound_union 0
(least_upper_bound_union-1 nil 3314556714
("" (skosimp)
(("" (expand "least_upper_bound?")
(("" (prop)
(("1" (hide -4 -2)
(("1" (expand "upper_bound?")
(("1" (skolem-typepred)
(("1" (expand* "union" "member")
(("1" (inst - "r!1")
(("1" (rewrite "le_lub_1") nil nil)
("2" (assert)
(("2" (inst - "r!1")
(("2" (rewrite "le_lub_2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (rewrite "lub_le")
(("2" (split)
(("1" (hide -5 -4 -2)
(("1" (inst?)
(("1" (assert)
(("1" (expand "upper_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 "upper_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)
((least_upper_bound? const-decl "bool" bounded_orders nil)
(r!2 skolem-const-decl "(S1!1)" upper_semilattices nil)
(union_preserves_bounded_above application-judgement
"(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
nil)
(r!2 skolem-const-decl "(S2!1)" upper_semilattices nil)
(lub_le formula-decl nil upper_semilattices nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil upper_semilattices nil)
(set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
(pred type-eq-decl nil defined_types nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(S1!1 skolem-const-decl
"(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
upper_semilattices nil)
(S2!1 skolem-const-decl
"(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
upper_semilattices nil)
(r!1 skolem-const-decl "(union(S1!1, S2!1))" upper_semilattices
nil)
(le_lub_1 formula-decl nil upper_semilattices nil)
(le_lub_2 formula-decl nil upper_semilattices nil)
(member const-decl "bool" sets nil)
(upper_bound? const-decl "bool" bounded_orders nil))
shostak))
(least_upper_bound_add 0
(least_upper_bound_add-1 nil 3314556833
("" (skosimp)
(("" (rewrite "add_as_union")
(("" (rewrite "least_upper_bound_union")
(("" (rewrite "least_upper_bound_singleton") nil nil)) nil))
nil))
nil)
((add_as_union formula-decl nil sets_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(T formal-type-decl nil upper_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(union_preserves_bounded_above application-judgement
"(LAMBDA (S: set[T]): bounded_above?(S, <=))" upper_semilattices
nil)
(least_upper_bound_singleton formula-decl nil upper_semilattices
nil)
(least_upper_bound_union formula-decl nil upper_semilattices nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil))
shostak))
(union_preserves_least_bounded_above 0
(union_preserves_least_bounded_above-1 nil 3314553924
("" (skolem-typepred)
(("" (expand "least_bounded_above?")
(("" (skosimp*)
(("" (inst + "lub(t!1, t!2)")
(("" (rewrite "least_upper_bound_union") nil nil)) nil))
nil))
nil))
nil)
((lub const-decl "T" upper_semilattices nil)
(least_upper_bound_union formula-decl nil upper_semilattices nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(least_bounded_above? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(add_preserves_least_bounded_above 0
(add_preserves_least_bounded_above-1 nil 3314553924
("" (skolem-typepred)
(("" (rewrite "add_as_union")
(("" (rewrite "union_preserves_least_bounded_above") nil nil))
nil))
nil)
((add_as_union formula-decl nil sets_lemmas nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(union_preserves_least_bounded_above application-judgement
"(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
upper_semilattices nil)
(union_preserves_least_bounded_above judgement-tcc nil
upper_semilattices nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(least_bounded_above? 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 upper_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(lub_union 0
(lub_union-1 nil 3314556944
("" (skolem!)
(("" (invoke (typepred "%1" "%2" "%3") (! 1 l) (! 1 r 1) (! 1 r 2))
(("" (invoke (name-replace "LU" "%1") (! 1 l))
(("" (invoke (name-replace "L1" "%1") (! 1 r 1))
(("" (invoke (name-replace "L2" "%1") (! 1 r 2))
(("" (use "least_upper_bound_union")
(("" (assert)
(("" (use "unique_least_upper_bound") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((union_preserves_least_bounded_above application-judgement
"(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
upper_semilattices nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil upper_semilattices nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(union const-decl "set" sets nil)
(least_upper_bound_union formula-decl nil upper_semilattices nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(lub const-decl "T" upper_semilattices nil)
(unique_least_upper_bound formula-decl nil bounded_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(lub_add 0
(lub_add-1 nil 3314557004
("" (skolem!)
(("" (rewrite "add_as_union")
(("" (rewrite "lub_union")
(("" (rewrite "lub_singleton") nil nil)) nil))
nil))
nil)
((add_as_union formula-decl nil sets_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(upper_semilattice?[T])" upper_semilattices
nil)
(T formal-type-decl nil upper_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" upper_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
upper_semilattices nil)
(union_preserves_least_bounded_above application-judgement
"(LAMBDA (S: set[T]): least_bounded_above?(S, <=))"
upper_semilattices nil)
(lub_singleton formula-decl nil upper_semilattices nil)
(lub_union formula-decl nil upper_semilattices nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.9Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
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.
|
