|
(lower_semilattices
(finite_set_is_greatest_bounded_below 0
(finite_set_is_greatest_bounded_below-1 nil 3315157450
("" (skolem!)
(("" (typepred "<=")
(("" (expand "lower_semilattice?")
(("" (flatten) (("" (inst?) nil nil)) nil)) nil))
nil))
nil)
((<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil lower_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))
(greatest_lower_bound_singleton 0
(greatest_lower_bound_singleton-1 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)
((greatest_lower_bound? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil lower_semilattices nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(lower_bound? const-decl "bool" bounded_orders nil))
shostak))
(glb_singleton 0
(glb_singleton-1 nil 3315157548
("" (skolem!)
(("" (invoke (typepred "%1") (! 1 l))
(("" (rewrite "unique_greatest_lower_bound")
(("" (rewrite "greatest_lower_bound_singleton") nil nil)) nil))
nil))
nil)
((nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_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 lower_semilattices nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(greatest_lower_bound_singleton formula-decl nil lower_semilattices
nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(unique_greatest_lower_bound formula-decl nil bounded_orders nil))
shostak))
(le_glb 0
(le_glb-1 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)
((glb const-decl "T" lower_semilattices nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(t!1 skolem-const-decl "T" lower_semilattices nil)
(u!1 skolem-const-decl "T" lower_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)
(lower_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 "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(greatest_lower_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 lower_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]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil))
shostak))
(glb_le_1 0
(glb_le_1-1 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)
((glb const-decl "T" lower_semilattices nil)
(= const-decl "[T, T -> boolean]" equalities 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" lower_semilattices nil)
(t!1 skolem-const-decl "T" lower_semilattices nil)
(lower_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 "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(greatest_lower_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 lower_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]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil))
shostak))
(glb_le_2 0
(glb_le_2-1 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)
((glb const-decl "T" lower_semilattices nil)
(= const-decl "[T, T -> boolean]" equalities 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" lower_semilattices nil)
(t!1 skolem-const-decl "T" lower_semilattices nil)
(lower_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 "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(greatest_lower_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 lower_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]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil))
shostak))
(union_preserves_bounded_below 0
(union_preserves_bounded_below-1 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)
((glb const-decl "T" lower_semilattices nil)
(union const-decl "set" sets nil)
(S1!1 skolem-const-decl
"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
nil)
(S2!1 skolem-const-decl
"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
nil)
(r!1 skolem-const-decl "(union[T](S1!1, S2!1))" lower_semilattices
nil)
(glb_le_1 formula-decl nil lower_semilattices nil)
(glb_le_2 formula-decl nil lower_semilattices nil)
(member const-decl "bool" sets nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(bounded_below? 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 lower_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_below 0
(add_preserves_bounded_below-1 nil 3315157450
("" (skolem-typepred)
(("" (rewrite "add_as_union")
(("" (rewrite "union_preserves_bounded_below") nil nil)) nil))
nil)
((add_as_union formula-decl nil sets_lemmas nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(union_preserves_bounded_below application-judgement
"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
nil)
(union_preserves_bounded_below judgement-tcc nil lower_semilattices
nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(bounded_below? 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 lower_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))
(greatest_lower_bound_union 0
(greatest_lower_bound_union-1 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)
((greatest_lower_bound? const-decl "bool" bounded_orders nil)
(r!2 skolem-const-decl "(S1!1)" lower_semilattices nil)
(union_preserves_bounded_below application-judgement
"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
nil)
(r!2 skolem-const-decl "(S2!1)" lower_semilattices nil)
(le_glb formula-decl nil lower_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 lower_semilattices nil)
(set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
(pred type-eq-decl nil defined_types nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(S1!1 skolem-const-decl
"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
lower_semilattices nil)
(S2!1 skolem-const-decl
"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
lower_semilattices nil)
(r!1 skolem-const-decl "(union(S1!1, S2!1))" lower_semilattices
nil)
(glb_le_1 formula-decl nil lower_semilattices nil)
(glb_le_2 formula-decl nil lower_semilattices nil)
(member const-decl "bool" sets nil)
(lower_bound? const-decl "bool" bounded_orders nil))
shostak))
(greatest_lower_bound_add 0
(greatest_lower_bound_add-1 nil 3315158032
("" (skosimp)
(("" (rewrite "add_as_union")
(("" (rewrite "greatest_lower_bound_union")
(("" (rewrite "greatest_lower_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)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(T formal-type-decl nil lower_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(union_preserves_bounded_below application-judgement
"(LAMBDA (S: set[T]): bounded_below?(S, <=))" lower_semilattices
nil)
(greatest_lower_bound_singleton formula-decl nil lower_semilattices
nil)
(greatest_lower_bound_union formula-decl nil lower_semilattices
nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil))
shostak))
(union_preserves_greatest_bounded_below 0
(union_preserves_greatest_bounded_below-1 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)
((glb const-decl "T" lower_semilattices nil)
(greatest_lower_bound_union formula-decl nil lower_semilattices
nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? 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 lower_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_greatest_bounded_below 0
(add_preserves_greatest_bounded_below-1 nil 3315157450
("" (skolem!)
(("" (rewrite "add_as_union")
(("" (rewrite "union_preserves_greatest_bounded_below") 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)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(T formal-type-decl nil lower_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(union_preserves_greatest_bounded_below application-judgement
"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
lower_semilattices nil)
(union_preserves_greatest_bounded_below judgement-tcc nil
lower_semilattices nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil))
nil))
(glb_union 0
(glb_union-1 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)
((union_preserves_greatest_bounded_below application-judgement
"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
lower_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 lower_semilattices nil)
(set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(union const-decl "set" sets nil)
(greatest_lower_bound_union formula-decl nil lower_semilattices
nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(glb const-decl "T" lower_semilattices nil)
(unique_greatest_lower_bound formula-decl nil bounded_orders nil)
(= const-decl "[T, T -> boolean]" equalities nil))
shostak))
(glb_add 0
(glb_add-1 nil 3315158200
("" (skolem!)
(("" (rewrite "add_as_union")
(("" (rewrite "glb_union")
(("" (rewrite "glb_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)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(<= formal-const-decl "(lower_semilattice?[T])" lower_semilattices
nil)
(T formal-type-decl nil lower_semilattices nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" lower_semilattices nil)
(nonempty_union2 application-judgement "(nonempty?)"
lower_semilattices nil)
(union_preserves_greatest_bounded_below application-judgement
"(LAMBDA (S: set[T]): greatest_bounded_below?(S, <=))"
lower_semilattices nil)
(glb_singleton formula-decl nil lower_semilattices nil)
(glb_union formula-decl nil lower_semilattices nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil))
shostak)))
¤ Dauer der Verarbeitung: 0.982 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.
|
