(finite_pointwise_ordersnil 3314641151"" (forward-chain "nat_infinite" ) nil nil )nil numbers_infinite nil )) nil ))nil 3314641151"" (forward-chain "domain_finiteness" ) nil nil )nil finite_pointwise_orders nil ))nil ))nil 3314641222"" (skolem!)"" (use "infinite_pigeonhole" )"" (skolem!)"" (inst?)"" (use "enumerable" )"1" (skolem-typepred)"1" (inst?)"1" (skolem!)"1" (decompose-equality)"1" (inst - "f!2(n!1)" )"1" expand * "image" "inverse_image" "singleton" "member" )"1" (replace *)"1" (assert )"1" (inst?)"1" expand "fullset" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand * "strictly_monotone?" "preserves" "preserves" "restrict" )nil nil ))nil ))nil )"2" (expand * "enumerable?" "bounded_below?" )"2" (assert )"2" (inst + 0)"2" (expand * "lower_bound?" "restrict" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil infinite_pigeonhole nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil finite_pointwise_orders nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"bool" integer_enumerations nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" functions nil )"nat" finite_pointwise_orders nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"set[R]" function_image nil )"set" sets nil )"(strictly_monotone?)" nil )"bool" reals nil )"R" restrict nil )"bool" functions nil )nil defined_types nil )"(strict_total_order?[S])" restrict_order_props nil )"(trichotomous?[S])" nil )"(strict_order?[S])" nil )"(transitive?[S])" nil )"(antisymmetric?[S])" nil )"(irreflexive?[S])" nil )"(strict_total_order?[real])" real_props nil )"non_empty_finite_set[T]" bounded_orders nil )"D" finite_pointwise_orders nil )"(singleton?)" sets nil )"bool" sets nil )"[nat -> D]" finite_pointwise_orders nil )"set[D]" function_image nil )"bool" integer_enumerations nil )set type-eq-decl nil sets nil )nil integer_enumerations nil ))nil 3314641512"" (skosimp)"" (expand "descending?" )"" (inst?)"" expand * "strictly_pointwise" "irreflexive_kernel" "difference" "member" )"" (flatten)"" (decompose-equality)"" expand * "pointwise" "reflexive_closure" "union" "member" )"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" monotone_sequences nil )"(irreflexive?)" closure_ops nil )"bool" sets nil )"set" sets nil )"pred[[[D -> R], [D -> R]]]" nil )"(preorder?)" well_foundedness nil )"(preorder?[[D -> R]])" finite_pointwise_orders nil )"(transitive?[[D -> R]])" finite_pointwise_orders nil )"(reflexive?[[D -> R]])" finite_pointwise_orders nil )"posint" nil )nil finite_pointwise_orders nil )nil finite_pointwise_orders nil )"bool" pointwise_orders nil )"set" sets nil )"(reflexive?)" closure_ops nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"int" integers nil )"posint" nil )"(total_order?[real])" nil ))nil 3314641603"" (expand "descending?" )"" (skosimp*)"" (inst?)"" expand * "strictly_pointwise" "irreflexive_kernel" "difference" "member" "pointwise" )"" (flatten) (("" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil )"(irreflexive?)" closure_ops nil )"bool" sets nil )"bool" pointwise_orders nil )"set" sets nil )"pred[[[D -> R], [D -> R]]]" nil )nil finite_pointwise_orders nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" monotone_sequences nil ))nil 3314641647"" (skosimp)"" (use "infinite_pigeonhole" )"" "LAMBDA n: epsilon({d | rel!1(seq!1(n + 1)(d), seq!1(n)(d))})" )"1" (skolem-typepred)"1" (inst? +)"1" (inst? +)"1" (expand "descending?" +)"1" (skolem!)"1" (inst - "n!1" )"1" (use "epsilon_ax[D]" )"1" (replace -3 :hide? t)"1" (split)"1" (lemma "descending_lem[R]" )"1" "reflexive_closure(rel!1)" "LAMBDA n: seq!1(n)(d!1)" )"1" expand *"preserves" "restrict" "converse" "reflexive_closure" "union" "member" )"1" "g!1(n!1) + 1" "g!1(1 + n!1)" )"1" assert )"1" "1" "transitive[R]" )"1" "rel!1" "seq!1(g!1(1 + n!1))(d!1)" "seq!1(g!1(n!1) + 1)(d!1)" "seq!1(g!1(n!1))(d!1)" )"1" (assert ) nil nil ))nil ))nil )"2" expand *"preserves" "preserves" "restrict" )"2" "n!1" "n!1 + 1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "descending_reflexive_closure" )nil nil ))nil ))nil )"2" (rewrite "descending_exists" ) nil nil ))nil ))nil )"2" (inst + "d!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (use "descending_exists" )"2" (assert ) (("2" (skolem!) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil finite_pointwise_orders nil )"int" integers nil )"even_int" integersnil )"bool" reals nil )"R" restrict nil )"bool" functions nil )NOT const-decl "[bool -> bool]" booleans nil )nil epsilons nil )"(preorder?)" well_foundedness nil )nil sequences nil )"bool" relations nil )"(reflexive?)" closure_ops nil )"(transitive?[R])" finite_pointwise_ordersnil )"[nat -> [D -> R]]" nil )"D" finite_pointwise_orders nil )"posint" nil )nil relations_extra nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"pred[[T2, T1]]" relation_defs nil )"set" sets nil )"bool" sets nil )nil nil )nil monotone_sequences nil )nil finite_pointwise_orders nil )"bool" monotone_sequences nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" relations nil )nil defined_types nil )nil finite_pointwise_orders nil )"T" epsilons nil )nil defined_types nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil finite_pointwise_orders nil )nil booleans nil )nil booleans nil )"bool" booleans nil )"posint" nil ))nil 3314641151"" (skolem-typepred)"" (expand "well_founded_order?" )"" (prop)"1" (rewrite "no_infinite_descending_sequence[R]" )"1" (rewrite "no_infinite_descending_sequence[[D->R]]" )"1" (expand * "empty?" "member" )"1" (skolem!)"1" (forward-chain "pointwise_pigeonhole" )"1" (skolem!) (("1" (inst?) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "strictly_pointwise" )"2" (invoke (typepred "%1" ) (! 1 1))"2" (expand "strict_order?" ) (("2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"(strict_order?)" nil )"(reflexive?)" closure_ops nil )"bool" relations nil )"bool" pointwise_orders nil )"(irreflexive?)" closure_ops nil )"bool" relations nil )"bool" orders nil )"(reflexive?[[D -> R]])" finite_pointwise_orders nil )"(partial_order?)" nil )nil well_foundednessnil )"bool" sets nil )"bool" sets nil )nil finite_pointwise_orders nil )nil defined_types nil )"bool" relations nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil sequences nil )"bool" functions nil )"R" restrict nil )"bool" reals nil )nil finite_pointwise_orders nil )"pred[[[D -> R], [D -> R]]]" nil )"bool" well_foundedness nil )nil defined_types nil )nil finite_pointwise_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.23 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
