|
(pointwise_orders
(pointwise_preserves_reflexive 0
(pointwise_preserves_reflexive-1 nil 3314638777
("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(PRED type-eq-decl nil defined_types nil)
(D formal-type-decl nil pointwise_orders nil)
(pointwise const-decl "bool" pointwise_orders nil)
(reflexive? const-decl "bool" relations nil))
nil))
(pointwise_preserves_transitive 0
(pointwise_preserves_transitive-1 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)
((pointwise const-decl "bool" pointwise_orders nil)
(D formal-type-decl nil pointwise_orders nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(R formal-type-decl nil pointwise_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(pointwise_preserves_preorder 0
(pointwise_preserves_preorder-1 nil 3314638777
("" (judgement-tcc) nil nil)
((pointwise_preserves_transitive application-judgement
"(transitive?[[D -> R]])" pointwise_orders nil)
(pointwise_preserves_reflexive application-judgement
"(reflexive?[[D -> R]])" pointwise_orders nil)
(preorder? const-decl "bool" orders nil))
nil))
(pointwise_preserves_antisymmetric 0
(pointwise_preserves_antisymmetric-1 nil 3314638777
("" (skolem-typepred)
(("" (expand* "antisymmetric?" "pointwise")
(("" (skosimp*)
(("" (decompose-equality)
(("" (inst?)
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pointwise const-decl "bool" pointwise_orders nil)
(D formal-type-decl nil pointwise_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(R formal-type-decl nil pointwise_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(pointwise_preserves_partial_order 0
(pointwise_preserves_partial_order-1 nil 3314638777
("" (judgement-tcc) nil nil)
((pointwise_preserves_antisymmetric application-judgement
"(antisymmetric?[[D -> R]])" pointwise_orders nil)
(pointwise_preserves_preorder application-judgement
"(preorder?[[D -> R]])" pointwise_orders nil)
(partial_order? const-decl "bool" orders nil))
nil))
(finiteness_lemma 0
(finiteness_lemma-1 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"
(case-replace
"{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)
((member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(D formal-type-decl nil pointwise_orders nil)
(R formal-type-decl nil pointwise_orders 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)
(f!1 skolem-const-decl "[D -> R]" pointwise_orders nil)
(nff!1 skolem-const-decl "non_empty_finite_set[[D -> R]]"
pointwise_orders nil)
(finite_image judgement-tcc nil function_image_aux nil)
(image const-decl "set[R]" function_image nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil))
shostak))
(least_upper_bound_pointwise 0
(least_upper_bound_pointwise-1 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"
(inst -
"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"
(lift-if)
(("1"
(prop)
(("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"
(inst?)
(("2"
(expand "pointwise")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((least_upper_bound? const-decl "bool" bounded_orders nil)
(x!1 skolem-const-decl "D" pointwise_orders nil)
(r!2 skolem-const-decl "(ff!1)" pointwise_orders nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(D formal-type-decl nil pointwise_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(pointwise const-decl "bool" pointwise_orders nil)
(f!1 skolem-const-decl "[D -> R]" pointwise_orders nil)
(ff!1 skolem-const-decl "set[[D -> R]]" pointwise_orders nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(r!1 skolem-const-decl "(ff!1)" pointwise_orders nil)
(x!1 skolem-const-decl "D" pointwise_orders nil)
(f!1 skolem-const-decl "[D -> R]" pointwise_orders nil))
shostak))
(least_bounded_above_pointwise 0
(least_bounded_above_pointwise-1 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)
((least_bounded_above? const-decl "bool" bounded_orders nil)
(skolemize_exists formula-decl nil skolemization nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(least_upper_bound_pointwise formula-decl nil pointwise_orders 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)
(D formal-type-decl nil pointwise_orders nil)
(R formal-type-decl nil pointwise_orders nil))
shostak))
(pointwise_preserves_upper_semilattices 0
(pointwise_preserves_upper_semilattices-1 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)
((pred type-eq-decl nil defined_types nil)
(R formal-type-decl nil pointwise_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil pointwise_orders nil)
(finiteness_lemma formula-decl nil pointwise_orders nil)
(nonempty? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(all_finite_least_bounded formula-decl nil bounded_orders nil)
(least_bounded_above_pointwise formula-decl nil pointwise_orders
nil)
(upper_semilattice? const-decl "bool" bounded_orders nil)
(pointwise_preserves_partial_order application-judgement
"(partial_order?[[D -> R]])" pointwise_orders nil))
nil))
(pointwise_preserves_complete_upper_semilattices 0
(pointwise_preserves_complete_upper_semilattices-1 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)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(pred type-eq-decl nil defined_types nil)
(all_least_bounded formula-decl nil bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(least_bounded_above_pointwise formula-decl nil pointwise_orders
nil)
(D formal-type-decl nil pointwise_orders nil)
(set type-eq-decl nil sets nil)
(partial_order? const-decl "bool" orders nil)
(pointwise_preserves_partial_order judgement-tcc nil
pointwise_orders nil)
(complete_upper_semilattice? const-decl "bool" bounded_orders nil)
(pointwise_preserves_upper_semilattices application-judgement
"(upper_semilattice?[[D -> R]])" pointwise_orders nil))
nil))
(greatest_lower_bound_pointwise 0
(greatest_lower_bound_pointwise-1 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"
(inst -
"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"
(lift-if)
(("1"
(ground)
(("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"
(inst?)
(("2"
(expand "pointwise")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((greatest_lower_bound? const-decl "bool" bounded_orders nil)
(x!1 skolem-const-decl "D" pointwise_orders nil)
(r!2 skolem-const-decl "(ff!1)" pointwise_orders nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(D formal-type-decl nil pointwise_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(f!1 skolem-const-decl "[D -> R]" pointwise_orders nil)
(ff!1 skolem-const-decl "set[[D -> R]]" pointwise_orders nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(pointwise const-decl "bool" pointwise_orders nil)
(r!1 skolem-const-decl "(ff!1)" pointwise_orders nil)
(x!1 skolem-const-decl "D" pointwise_orders nil)
(f!1 skolem-const-decl "[D -> R]" pointwise_orders nil))
shostak))
(greatest_bounded_below_pointwise 0
(greatest_bounded_below_pointwise-1 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)
((greatest_bounded_below? const-decl "bool" bounded_orders nil)
(skolemize_exists formula-decl nil skolemization nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pointwise_preserves_antisymmetric application-judgement
"(antisymmetric?[[D -> R]])" pointwise_orders nil)
(greatest_lower_bound_pointwise formula-decl nil pointwise_orders
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)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(D formal-type-decl nil pointwise_orders nil)
(R formal-type-decl nil pointwise_orders nil))
shostak))
(pointwise_preserves_lower_semilattices 0
(pointwise_preserves_lower_semilattices-1 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)
((pred type-eq-decl nil defined_types nil)
(R formal-type-decl nil pointwise_orders nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil pointwise_orders nil)
(finiteness_lemma formula-decl nil pointwise_orders nil)
(nonempty? const-decl "bool" sets nil)
(all_finite_greatest_bounded formula-decl nil bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(greatest_bounded_below_pointwise formula-decl nil pointwise_orders
nil)
(lower_semilattice? const-decl "bool" bounded_orders nil)
(pointwise_preserves_partial_order application-judgement
"(partial_order?[[D -> R]])" pointwise_orders nil))
nil))
(pointwise_preserves_complete_lower_semilattices 0
(pointwise_preserves_complete_lower_semilattices-1 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)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(pred type-eq-decl nil defined_types nil)
(all_greatest_bounded formula-decl nil bounded_orders nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil pointwise_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(greatest_bounded_below_pointwise formula-decl nil pointwise_orders
nil)
(partial_order? const-decl "bool" orders nil)
(pointwise_preserves_partial_order judgement-tcc nil
pointwise_orders nil)
(complete_lower_semilattice? const-decl "bool" bounded_orders nil)
(pointwise_preserves_lower_semilattices application-judgement
"(lower_semilattice?[[D -> R]])" pointwise_orders nil))
nil))
(pointwise_preserves_lattices 0
(pointwise_preserves_lattices-1 nil 3314638777
("" (judgement-tcc) nil nil)
((pointwise_preserves_upper_semilattices application-judgement
"(upper_semilattice?[[D -> R]])" pointwise_orders nil)
(pointwise_preserves_lower_semilattices application-judgement
"(lower_semilattice?[[D -> R]])" pointwise_orders nil)
(lattice? const-decl "bool" bounded_orders nil))
nil))
(pointwise_preserves_complete_lattices 0
(pointwise_preserves_complete_lattices-1 nil 3314638777
("" (judgement-tcc) nil nil)
((pointwise_preserves_complete_upper_semilattices
application-judgement "(complete_upper_semilattice?[[D -> R]])"
pointwise_orders nil)
(pointwise_preserves_lattices application-judgement
"(lattice?[[D -> R]])" pointwise_orders nil)
(pointwise_preserves_complete_lower_semilattices
application-judgement "(complete_lower_semilattice?[[D -> R]])"
pointwise_orders nil)
(complete_lattice? const-decl "bool" bounded_orders nil))
nil))
(lub_pointwise_def_TCC1 0
(lub_pointwise_def_TCC1-1 nil 3314638777
("" (skosimp)
(("" (rewrite "least_bounded_above_pointwise") nil nil)) nil)
((least_bounded_above_pointwise formula-decl nil pointwise_orders
nil)
(D formal-type-decl nil pointwise_orders nil)
(R formal-type-decl nil pointwise_orders 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)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil))
nil))
(lub_pointwise_def_TCC2 0
(lub_pointwise_def_TCC2-1 nil 3314638777 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(least_upper_bound? const-decl "bool" bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil))
nil))
(lub_pointwise_def 0
(lub_pointwise_def-1 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)
((lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))"
bounded_orders nil)
(least_bounded_above? const-decl "bool" bounded_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(D formal-type-decl nil pointwise_orders nil)
(least_upper_bound_pointwise formula-decl nil pointwise_orders nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pointwise const-decl "bool" pointwise_orders nil)
(lub_def formula-decl nil bounded_orders nil)
(pointwise_preserves_antisymmetric application-judgement
"(antisymmetric?[[D -> R]])" pointwise_orders nil))
shostak))
(glb_pointwise_def_TCC1 0
(glb_pointwise_def_TCC1-1 nil 3314638777
("" (skosimp)
(("" (rewrite "greatest_bounded_below_pointwise") nil nil)) nil)
((greatest_bounded_below_pointwise formula-decl nil pointwise_orders
nil)
(R formal-type-decl nil pointwise_orders nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(D formal-type-decl nil pointwise_orders nil)
(set type-eq-decl nil sets nil))
nil))
(glb_pointwise_def_TCC2 0
(glb_pointwise_def_TCC2-1 nil 3314638777 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(PRED type-eq-decl nil defined_types nil)
(antisymmetric? const-decl "bool" relations nil)
(lower_bound? const-decl "bool" bounded_orders nil)
(greatest_lower_bound? const-decl "bool" bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil))
nil))
(glb_pointwise_def 0
(glb_pointwise_def-1 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)
((glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))"
bounded_orders nil)
(greatest_bounded_below? const-decl "bool" bounded_orders nil)
(antisymmetric? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(R formal-type-decl nil pointwise_orders nil)
(D formal-type-decl nil pointwise_orders nil)
(greatest_lower_bound_pointwise formula-decl nil pointwise_orders
nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(pointwise const-decl "bool" pointwise_orders nil)
(glb_def formula-decl nil bounded_orders nil)
(pointwise_preserves_antisymmetric application-judgement
"(antisymmetric?[[D -> R]])" pointwise_orders nil))
shostak)))
¤ Dauer der Verarbeitung: 0.79 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.
|
