(relation_iteratenil 3314540085"" (skolem!)"" (decompose-equality)"" (iff)"" (expand "o" )"" (prop)"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil defined_types nil )"bool" relation_props nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil relation_iterate nil ))nil 3314540148"" (skolem!)"" (decompose-equality)"" (iff)"" (expand "o" )"" (prop)"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil defined_types nil )"bool" relation_props nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil relation_iterate nil ))nil 3314540067 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3314540067 ("" (termination-tcc) nil nil ) nil nil ))nil 3314540217"" (induct "n" )"1" (skolem!)"1" (expand "iterate" + 3)"1" (rewrite "comp_equal_r" ) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "iterate" + (1 3))"2" (rewrite "assoc" :dir rl)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil relation_props2 nil )"posint" nil )nil relation_iterate nil )nil naturalnumbers nil )"bool" relation_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"pred[[T, T]]" relation_iterate nil )"[T, T -> boolean]" equalities nil )nil relation_iterate nil )nil defined_types 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 )"nonneg_int" nil ))nil 3314540329"" (skosimp)"" (rewrite "iterate_add" )"" (expand "o" ) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )nil relation_iterate nil )nil relation_iterate nil )nil booleans nil )nil booleans nil )nil defined_types 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 )"bool" relation_props nil ))nil 3314540378"" (skolem!)"" (expand * "iterate" "iterate" )"" (rewrite "comp_equal_l" ) nil nil )) nil ))nil )"pred[[T, T]]" relation_iterate nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil relation_iterate nil )nil relation_iterate nil ))nil 3314540410"" (skolem!)"" (use "iterate_add" ("m" "1" "n" "n!1" ))"" (replace -1 :hide? t) (("" (rewrite "iterate_1" ) nil nil ))nil ))nil ))nil )nil relation_iterate 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 relation_iterate nil )nil defined_types nil )"int" integers nil )"posint" nil )nil relation_iterate nil ))nil 3314540483"" (induct "n" )"1" (skolem!)"1" (expand "iterate" + (1 3)) (("1" (propax) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "iterate" + 1)"2" (inst?)"2" (rewrite "iterate_add" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil relation_iterate nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"pred[[T, T]]" relation_iterate nil )"[T, T -> boolean]" equalities nil )nil relation_iterate nil )nil defined_types 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 )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil 3314540542"" (decompose-equality)"" (expand "converse" )"" (rewrite "symmetry_of_equals" ) nil nil )) nil ))nil )nil equality_props nil )nil relation_iterate nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"pred[[T2, T1]]" relation_defs nil )nil defined_types nil )nil booleans nil ))nil 3314540571"" (skolem!)"" (decompose-equality)"" (iff)"" (expand * "o" "converse" )"" (prop)"1" (skosimp)"1" (inst?) (("1" (assert ) nil nil )) nil )) nil )"2" (skosimp)"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil defined_types nil )"pred[[T2, T1]]" relation_defs nil )"bool" relation_props nil )nil booleans nil )nil relation_iterate nil ))nil 3314540613"" (induct "n" )"1" (skolem!)"1" (expand "iterate" )"1" (rewrite "converse_equal" ) nil nil )) nil ))nil )"2" (skosimp*)"2" (rewrite "iterate_add_one" )"2" (expand "iterate" + 2)"2" (rewrite "converse_comp" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil relation_iterate nil )nil relation_iterate nil )nil relation_iterate nil )nil naturalnumbers nil )"pred[[T2, T1]]" relation_defs nil )"pred[[T, T]]" relation_iterate nil )"[T, T -> boolean]" equalities nil )nil relation_iterate nil )nil defined_types 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 ))nil 3314540754"" (expand * "subset?" "member" "o" )"" (skosimp*)"" (inst?)"" (inst?) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil relation_iterate nil )"bool" sets nil )"bool" relation_props nil )"bool" sets nil ))nil 3314540812"" (induct "n" )"1" (skosimp)"1" (expand * "iterate" "subset?" "member" )"1" (skosimp) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "iterate" +)"2" (rewrite "comp_is_monotone" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil relation_iterate nil )"(partial_order?[set[T]])" nil )"bool" sets nil )nil naturalnumbers nil )"pred[[T, T]]" relation_iterate nil )"bool" sets nil )set type-eq-decl nil sets nil )"[bool, bool -> bool]" booleans nil )nil relation_iterate nil )nil defined_types 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 ))quality 100%
¤ Dauer der Verarbeitung: 0.26 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
