(csequence_propsnil 3513451673 ("" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3513451673 ("" (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 3513451673 ("" (termination-tcc) nil nil ) nil nil ))nil 3513451692"" (induct "n" )"1" (skosimp)"1" (expand "has_length" ) (("1" (ground) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "has_length" (-2 -3))"2" (ground)"2" (inst - "rest(cseq!1)" "m!1 - 1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" nil )"posint" nil )"[csequence -> boolean]" nil )"[(nonempty?) -> csequence]" csequence_codtnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" csequence_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil csequence_codt nil )nil csequence_props 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 3513451673 ("" (subtype-tcc) nil nil ) nil nil ))nil 3513451736"" (skolem!)"" (prop)"1" (generalize-skolem-constants)"1" (induct "cseq_1" :name "is_finite_induction" )"1" (skosimp)"1" (case "empty?(cseq!2)" )"1" (inst + 0)"1" (expand "has_length" ) (("1" (assert ) nil nil ))nil ))nil )"2" (ground)"2" (skolem!)"2" (inst + "1 + n!1" )"2" (expand "has_length" +)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem!)"2" (generalize-skolem-constants)"2" (induct "n_1" )"1" (skosimp)"1" (expand * "has_length" "is_finite" )"1" (ground) nil nil )) nil ))nil )"2" (skosimp*)"2" (expand "has_length" -2)"2" (expand "is_finite" +)"2" (ground)"2" (inst - "rest(cseq!2)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil csequence_props nil )"[csequence -> boolean]" csequence_codtnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )nil csequence_props nil )nil csequence_codt nil )"bool" 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 )"bool" csequence_props nil )"[(nonempty?) -> csequence]" csequence_codtnil )"[csequence -> boolean]" nil )nil naturalnumbers nil )nil defined_types nil ))nil 3513451673"" (expand "is_finite" ) (("" (propax) nil nil )) nil )"bool" csequence_props nil )) nil ))nil 3513451673"" (skolem-typepred)"" (expand "is_finite" ) (("" (propax) nil nil )) nil )) nil )"bool" csequence_props nil )nil csequence_props nil )"[csequence -> boolean]" csequence_codtnil )nil csequence_codt nil )nil csequence_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3513451673"" (skolem-typepred)"" (expand "is_finite" ) (("" (assert ) nil nil )) nil )) nil )nil csequence_props nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" csequence_props nil )nil booleans nil )nil booleans nil )nil csequence_codt nil )nil csequence_props nil ))nil ))nil 3513452041"" (skolem!)"" (prop)"1" (lemma "some_weak_induction" )"1" "p!1" "LAMBDA cseq: NOT every(pred_NOT(p!1))(cseq)" )"1" (split)"1" (inst - "cseq!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp)"2" (expand "every" -2)"2" (expand "pred_NOT" )"2" (lift-if) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "every_weak_coinduction" )"2" "pred_NOT(p!1)" "LAMBDA cseq: NOT some(p!1)(cseq)" )"2" (split)"1" (inst - "cseq!1" ) (("1" (assert ) nil nil )) nil )"2" (skosimp)"2" (expand "some" 1)"2" (expand "pred_NOT" )"2" (lift-if) (("2" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )nil defined_types nil )nil defined_types nil )nil csequence_codt nil )NOT const-decl "[bool -> bool]" booleans nil )"boolean" csequence_codt nil )"bool" csequence_props nil )nil csequence_codt nil )nil csequence_props nil )"boolean" csequence_codt nil )nil csequence_codt nil ))nil 3513452124"" (skolem!)"" (lemma "some_every_rew" )"" (inst - "pred_NOT(p!1)" "cseq!1" )"" (expand "pred_NOT" )"" (replace-eta "p!1" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil csequence_props nil )"[T, T -> boolean]" equalities nil )nil csequence_codt nil )"bool" csequence_props nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil csequence_props nil ))nil 3513452167"" (induct "cseq" :name "some_induction" )"" (skosimp)"" (inst - "p!1" "LAMBDA cseq: some(q!1)(cseq)" )"" (split)"1" (inst - "cseq!1" ) (("1" (assert ) nil nil )) nil )"2" (delete -2 2)"2" (skosimp)"2" (expand "some" +)"2" (expand "pred_IMPLIES" )"2" (lift-if)"2" (ground)"2" (inst - "first(a!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" csequence_props nil )"[csequence -> boolean]" nil )"[(nonempty?) -> T]" csequence_codt nil )"boolean" csequence_codt nil )nil csequence_codt nil )nil defined_types nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil csequence_codt nil )nil csequence_props nil ))nil 3513452244"" (induct "cseq" :name "every_coinduction" )"" (skosimp)"" (inst - "q!1" "LAMBDA cseq: every(p!1)(cseq)" )"" (split)"1" (inst - "cseq!1" ) (("1" (assert ) nil nil )) nil )"2" (delete -2 2)"2" (skosimp)"2" (expand "every" -)"2" (expand "pred_IMPLIES" )"2" (lift-if)"2" (ground)"2" (inst - "first(a!1)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" csequence_props nil )"[csequence -> boolean]" nil )"[(nonempty?) -> T]" csequence_codt nil )"boolean" csequence_codt nil )nil csequence_codt nil )nil defined_types nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil csequence_codt nil )nil csequence_props nil ))quality 100%
¤ Dauer der Verarbeitung: 0.3 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
