| products/sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: horizontal.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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.31 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.Bot Zugriff |
