(powerseriesnil 3507981245"" (skosimp*) (("" (grind) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3507981245 ("" (subtype-tcc) nil nil ) nil nil ))nil 3507981245 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3507981245 ("" (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 3507981245"" (skosimp*)"" (typepred "cxs!1" )"" (expand "cauchys_real?" )"" (typepred "cx!1" )"" (expand "cauchy_real?" )"" (skosimp*)"" "(LAMBDA i: IF i = 0 THEN xs!1(i) ELSE xs!1(i)*x!1^i ENDIF)" )"" (assert )"" (expand "cauchys_prop" )"" (skosimp*)"" (inst - "n!1" )"" (lemma "trichotomy" ("x" "n!1" ))"" (split -1)"1" (assert )"1" "mul_lemma" "x" "xs!1(n!1)" "y" "x!1 ^ n!1" "cx" "cxs!1(n!1)" "cy" "cauchy_power(cx!1, n!1)" ))"1" "power_lemma" "x" "x!1" "pn" "n!1" "cx" "cx!1" ))"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sum nil )"bool" sum nil )nil cauchy nil )"bool" cauchy 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 )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_axioms nil )"(strict_total_order?[real])" real_props nil )nil power nil )"cauchy_real" power nil )nil integers nil )"bool" reals nil )nil integers nil )nil mul nil )"bool" sum nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil number_fields nil )"real" reals nil ))nil ))nil 3507981245"" (skosimp*)"" (expand "cauchys_real?" )"" (inst + "xs!1" )"" (expand "cauchys_prop" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" sum nil )"bool" sum 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 ))nil 3507981245"" (skosimp*)"" (expand "powerseries" )"" (expand "cauchy_powerseries" )"" "sum_lemma" "xs" "(LAMBDA i: IF i = 0 THEN xs!1(i) ELSE xs!1(i) * x!1 ^ i ENDIF)" "m" "m!1" "cxs" "(LAMBDA i: IF i = 0 THEN cxs!1(i) ELSE cauchy_mul(cxs!1(i), cauchy_power(cx!1, i)) ENDIF)" ))"1" (assert )"1" (hide 2)"1" (skosimp*)"1" (lemma "trichotomy" ("x" "n!1" ))"1" (inst - "n!1" )"1" (split -1)"1" (simplify)"1" (assert )"1" "mul_lemma" "x" "xs!1(n!1)" "y" "x!1 ^ n!1" "cx" "cxs!1(n!1)" "cy" "cauchy_power(cx!1, n!1)" ))"1" (assert )"1" "power_lemma" "x" "x!1" "cx" "cx!1" "pn" "n!1" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"real" powerseries nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"cauchy_real" power nil )nil integers nil )"bool" reals nil )nil integers nil )"cauchy_real" mul nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil cauchy nil )"bool" cauchy 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 sum nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil real_axioms nil )nil power nil )nil mul nil )"(strict_total_order?[real])" real_props nil )"cauchy_real" powerseries nil ))nil )))quality 93%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
