Quelle csequence_constant.prf
Sprache: Lisp
(csequence_constantnil 3513602349 ("" (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 3513602349 ("" (termination-tcc) nil nil )nil nil ))nil 3513602349"" (expand "is_finite" ) (("" (propax) nil nil )) nil )"bool" csequence_props nil )) nil ))nil 3513602385"" (skolem!)"" (expand "constant_cseq" )"" (lift-if) (("" (ground) nil nil )) nil )) nil ))nil )"finite_csequence" csequence_constant nil )"int" integers nil ))nil 3513602407 ("" (grind) nil nil )"finite_csequence" csequence_constant nil )nil csequence_constant nil )"(singleton_cseq?)" csequence_singletonnil ))nil 3513602349"" (skosimp)"" (expand "constant_cseq" ) (("" (assert ) nil nil )) nil )) nil )"finite_csequence" csequence_constant nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil ))nil 3513602464"" (skosimp)"" (expand "constant_cseq" ) (("" (assert ) nil nil )) nil )) nil )"finite_csequence" csequence_constant nil )"(strict_total_order?[real])" real_props nil ))nil 3513602349 ("" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3513602539"" (skosimp)"" (expand "constant_cseq" 1 1) (("" (assert ) nil nil )) nil ))nil )"finite_csequence" csequence_constant nil )"(strict_total_order?[real])" real_props nil )"int" integers nil ))nil 3513602568"" (induct "n" )"1" (expand * "constant_cseq" "length" ) nil nil )"2" (skosimp*)"2" (expand "constant_cseq" +)"2" (expand "length" +) (("2" (inst - "t!1" ) nil nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )"finite_csequence" csequence_constant nil )"{n | has_length(fseq, n)}" csequence_length nil )"bool" csequence_props nil )nil csequence_props nil )"bool" csequence_props nil )nil csequence_codt nil )"[T, T -> boolean]" equalities nil )nil csequence_constant 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 3513602615"" (skolem!)"" (rewrite "index?_finite" )"" (rewrite "constant_cseq_length" ) (("" (prop) nil nil )) nil ))nil ))nil )nil csequence_nth nil )nil csequence_codt nil )nil booleans nil )nil booleans nil )"bool" csequence_props nil )nil csequence_props 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 )"finite_csequence" csequence_constant nil )nil csequence_constant nil )"(strict_total_order?[real])" real_props nil )nil csequence_constant nil ))nil 3513602349"" (skolem!)"" (rewrite "index?_finite" )"" (rewrite "constant_cseq_length" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil csequence_nth nil )nil csequence_codt nil )nil booleans nil )nil booleans nil )"bool" csequence_props nil )nil csequence_props 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 )"finite_csequence" csequence_constant nil )"bool" reals nil )nil nat_types nil )nil csequence_constant nil )"(strict_total_order?[real])" real_props nil )nil csequence_constant nil ))nil ))nil 3513602648"" (induct "n" )"1" (skolem-typepred) nil nil )"2" (skosimp*)"2" (expand "constant_cseq" +)"2" (expand "nth" +)"2" (lift-if)"2" (ground) (("2" (inst - "t!1" "m!1 - 1" ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (skolem!) (("3" (use "constant_cseq_nth_TCC1" ) nil nil ))nil ))nil )nil csequence_constant nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" 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_constant nil )"bool" reals nil )nil nat_types nil )nil csequence_codt nil )"bool" csequence_nth nil )"bool" csequence_props nil )nil csequence_props nil )"finite_csequence" csequence_constant nil ))nil 3513602705"" (expand "constant_cseq" + 2) (("" (propax) nil nil )) nil )"finite_csequence" csequence_constant nil ))nil 3513602720"" (induct "n" )"1" (skosimp) (("1" (assert ) nil nil )) nil )"2" (skosimp*)"2" (expand "constant_cseq" +)"2" (expand "last" )"2" (expand "nth" +)"2" (expand "length" +)"2" (lift-if)"2" (inst - "t!1" )"2" (expand "constant_cseq" 1 1)"2" (expand "length" 1 1)"2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (use "constant_cseq_first_TCC1" ) (("3" (assert ) nil nil ))nil ))nil ))nil )nil csequence_constant nil )"{n | has_length(fseq, n)}" csequence_length nil )"int" integers nil )"posint" nil )"T" csequence_nth nil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"T" csequence_nth nil )nil csequence_props 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_constant nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil csequence_codt nil )"[csequence -> boolean]" nil )"bool" csequence_props nil )nil csequence_props nil )"finite_csequence" csequence_constant nil ))nil 3513603136"" (induct "n" )"1" (expand * "constant_cseq" "some" ) nil nil )"2" (skosimp*)"2" (inst - "t!1" "p!1" )"2" (expand "constant_cseq" +)"2" (expand "some" +) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"finite_csequence" csequence_constant nil )nil csequence_props nil )"bool" csequence_props nil )"boolean" csequence_codt nil )nil csequence_codt nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil csequence_constant 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 3513603181"" (induct "n" )"1" (expand * "constant_cseq" "every" ) nil nil )"2" (skosimp*)"2" (inst - "t!1" "p!1" )"2" (expand "constant_cseq" +)"2" (expand "every" +) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"finite_csequence" csequence_constant nil )nil csequence_props nil )"bool" csequence_props nil )"boolean" csequence_codt nil )nil csequence_codt nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )nil csequence_constant 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 3513602349"" (skolem!)"" (rewrite "is_finite_def" )"" (rewrite "not_exists" )"" (induct "x" )"1" expand * "has_length" "constant_cseq_struct" "coreduce" )nil nil )"2" (skosimp)"2" (expand "constant_cseq_struct" )"2" (expand "coreduce" -)"2" (expand "has_length" -) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil csequence_props nil )nil csequence_codt nil )nil csequence_codt_coreduce nil )nil booleans nil )nil booleans 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[T, T]" nil )nil csequence_constant nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil naturalnumbers 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 )"bool" csequence_props nil )nil quantifier_props nil ))nil ))nil 3513603454"" (expand * "constant_cseq" "constant_cseq_struct" "coreduce" ) nil nil )"{c: csequence[T] | AND empty?(c) OR AND nonempty?(c)}" nil )"csequence_struct[T, T]" nil )"infinite_csequence" csequence_constantnil ))nil 3513603484"" (expand * "constant_cseq" "constant_cseq_struct" )"" (expand "coreduce" 1 1) (("" (propax) nil nil )) nil )) nil )"{c: csequence[T] | AND empty?(c) OR AND nonempty?(c)}" nil )"infinite_csequence" csequence_constantnil )"csequence_struct[T, T]" nil ))nil 3513602349"" (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 )"infinite_csequence" csequence_constantnil )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_constant nil ))nil ))nil 3513603542"" (induct "n" )"1" expand * "nth" "constant_cseq" "constant_cseq_struct" "coreduce" )nil nil )"2" (skosimp*)"2" (inst - "t!1" )"2" (expand "nth" +)"2" (expand * "constant_cseq" "constant_cseq_struct" )"2" (expand "coreduce" +) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (skolem!) (("3" (use "constant_cseq_inf_nth_TCC1" ) nil nil ))nil ))nil )nil csequence_constant nil )"csequence_struct[T, T]" 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_constant 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_constantnil ))nil 3513603611"" (expand * "constant_cseq" "constant_cseq_struct" )"" (expand "coreduce" 1 2) (("" (propax) nil nil )) nil )) nil )"{c: csequence[T] | AND empty?(c) OR AND nonempty?(c)}" nil )"infinite_csequence" csequence_constantnil )"csequence_struct[T, T]" nil ))nil 3513603630"" (skolem!)"" (prop)"1" (lemma "some_induction" )"1" "p!1" "LAMBDA (cseq: csequence): FORALL t: cseq = constant_cseq(t) IMPLIES p!1(t)" )"1" (split)"1" (inst - "constant_cseq(t!1)" )"1" (assert ) (("1" (inst - "t!1" ) nil nil )) nil )) nil )"2" (delete -1 2)"2" (skosimp*)"2" (lift-if)"2" (ground)"1" (use "constant_cseq_inf_first" )"1" (assert ) nil nil )) nil )"2" (inst - "t!2" )"2" (replace -3)"2" (rewrite "constant_cseq_inf_rest" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand * "constant_cseq" "constant_cseq_struct" "coreduce" "some" )"2" (flatten) nil nil )) nil ))nil ))nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil defined_types nil )nil csequence_codt nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" csequence_props nil )nil csequence_props nil )"infinite_csequence" csequence_constantnil )nil csequence_constant nil )nil csequence_constant nil )nil csequence_codt nil )nil csequence_constant nil )"{c: csequence[T] | AND empty?(c) OR AND nonempty?(c)}" nil )"boolean" csequence_codt nil )"csequence_struct[T, T]" nil ))nil 3513603731"" (skolem!)"" (rewrite "every_some_rew" )"" (rewrite "constant_cseq_inf_some" )"" (expand "pred_NOT" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil )nil csequence_props nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil csequence_codt nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" csequence_props nil )nil csequence_props nil )"infinite_csequence" csequence_constantnil )nil csequence_constant nil )nil csequence_constant nil )"bool" csequence_props nil ))quality 100%
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
