(csequence_insert_removenil 3513480007"" (measure-induct+ "n" ("cseq" "n" ) :skolem-typepreds? t)"" (case-replace "x!2 = 0" )"1" (expand * "remove" "nth" "insert" "index?" )"1" (lift-if)"1" (assert ) (("1" (decompose-equality) nil nil )) nil ))nil ))nil )"2" (expand "index?" )"2" (ground)"2" (inst - "rest(x!1)" "x!2 - 1" )"2" (assert )"2" (expand "insert" +)"2" (expand "remove" +)"2" (expand "nth" +)"2" (decompose-equality 2) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil csequence_codt nil )"[[T, csequence] -> (nonempty?)]" nil )"[(nonempty?) -> T]" csequence_codt nil )"[(nonempty?) -> csequence]" csequence_codtnil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"csequence" csequence_remove nil )"T" csequence_nth nil )"nonempty_csequence" csequence_insert nil )nil csequence_props nil )"[csequence -> boolean]" nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil csequence_nth nil )"bool" csequence_nth 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 csequence_codt nil )nil csequence_insert_remove nil )nil measure_induction nil )"bool" orders nil )nil defined_types nil ))quality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
