(csequence_sequencenil 3513771080"" case "FORALL (seq: sequence[T], x: nat): NOT has_length(coreduce[T, sequence](from_sequence_struct)(seq), x)" )"1" (skolem!)"1" (rewrite "is_finite_def" )"1" (skolem!) (("1" (inst - "seq!1" "n!1" ) nil nil )) nil ))nil ))nil )"2" (delete 2)"2" (induct "x" )"1" (expand * "has_length" "from_sequence_struct" "coreduce" )nil nil )"2" (skosimp*)"2" (expand "has_length" -2)"2" (prop)"2" (expand "from_sequence_struct" )"2" (expand "coreduce" -1)"2" (inst - "LAMBDA n: seq!1(1 + n)" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil naturalnumbers nil )nil defined_types nil )nil csequence_props 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 csequence_sequence nil )nil sequences nil )NOT const-decl "[bool -> bool]" booleans nil )nil csequence_codt nil )"bool" csequence_props nil )nil csequence_codt_coreduce nil )OR const-decl "[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[csequence_struct -> boolean]" nil )"[csequence -> boolean]" csequence_codtnil )"[csequence_struct -> boolean]" nil )"[csequence -> boolean]" nil )"{c: csequence[T] | AND empty?(c) OR AND nonempty?(c)}" nil )"csequence_struct" nil ))nil ))nil 3513771080"" (skolem!) (("" (use "index?_infinite" ) nil nil )) nil )"infinite_csequence" csequence_sequencenil )nil sequences 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 csequence_props nil )"bool" csequence_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil csequence_codt nil )nil csequence_nth nil )nil csequence_sequence nil ))nil ))nil 3513771218"" (induct "n" )"1" expand * "nth" "from_sequence" "from_sequence_struct" "coreduce" )nil nil )"2" (skosimp*)"2" (expand "nth" +)"2" (expand * "from_sequence" "from_sequence_struct" )"2" (expand "coreduce" +)"2" (inst - "LAMBDA n: seq!1(1 + n)" ) nil nil )) nil ))nil ))nil ))nil )"3" (skolem!) (("3" (use "from_sequence_nth_TCC1" ) nil nil ))nil ))nil )nil csequence_sequence nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"csequence_struct" nil )"{c: csequence[T] | AND empty?(c) OR AND nonempty?(c)}" nil )nil naturalnumbers nil )"T" csequence_nth nil )nil csequence_nth nil )"[T, T -> boolean]" equalities nil )nil defined_types 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 csequence_sequence nil )nil sequences nil )nil csequence_codt nil )"bool" csequence_nth nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" csequence_props nil )nil csequence_props nil )"infinite_csequence" csequence_sequencenil ))nil 3513771080"" (skolem!) (("" (use "index?_infinite" ) nil nil )) 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 csequence_props nil )"bool" csequence_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil csequence_codt nil )nil csequence_nth nil )nil csequence_sequence nil ))nil ))nil 3513771313"" (expand "to_sequence" ) (("" (propax) nil nil )) nil )"sequence" csequence_sequence nil ))nil 3513771324"" (skolem!)"" (decompose-equality)"" (expand "to_sequence" )"" (rewrite "from_sequence_nth" ) nil nil )) nil ))nil ))nil )nil csequence_codt nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" csequence_props nil )nil csequence_props nil )nil sequences nil )"sequence" csequence_sequence nil )"infinite_csequence" csequence_sequencenil )nil csequence_sequence 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_sequence nil ))nil 3513771359"" (skolem!)"" (use "nth_extensionality" )"" (assert )"" (hide 2)"" (split)"1" (decompose-equality)"1" (rewrite "index?_infinite" )"1" (rewrite "index?_infinite" ) nil nil )) nil ))nil )"2" (skolem!)"2" (rewrite "from_sequence_nth" )"2" (rewrite "to_sequence_nth" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil csequence_nth nil )nil csequence_sequence nil )"sequence" csequence_sequence nil )"infinite_csequence" csequence_sequencenil )nil csequence_props nil )"bool" csequence_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil sequences 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_sequence nil )nil csequence_nth nil )nil csequence_sequence nil )"bool" csequence_nth nil )nil csequence_nth nil ))quality 92%
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
