(weierstrass_approximationnil 3479658253"" (lemma "real_metric_space" ) (("" (inst?) nil nil )) nil )"set" sets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_metric_space nil ))nil ))nil 3479744181"" (subtype-tcc) nil nil ) nil nil ))nil 3479744181"" (subtype-tcc) nil nil ) ((/= const-decl "boolean" notequal nil ))nil ))nil 3479744181"" (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 )"bool" reals nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3479744182"" (skeep)"" case "FORALL (pp: nat): FORALL (kz: nat): pp<=2 AND kz+1 > pp IMPLIES LAMBDA (i:nat): IF i > kz+1 THEN 0 ELSE i^pp*C(kz+1,i)*(-1)^(kz+1-i) ENDIF) = 0") "1" (inst - "p" )"1" (inst - "k-1" ) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2)"2" (hide -1)"2" (hide -1)"2" (induct "pp" )"1" (skosimp*)"1" (assert )"1" (lemma "binomial_theorem" )"1" (inst - "kz!1+1" "1" "-1" )"1" (assert )"1" (expand "^" -1 1)"1" (expand "expt" -1 1)"1" (lemma "sigma_restrict_eq" )"1" "LAMBDA (i: nat): IF i > kz!1+1 THEN 0 ELSE C(kz!1+1, i) * 1 ^ i * (-1) ^ (kz!1+1 - i) ENDIF" "LAMBDA (i: nat): IF i > kz!1+1 THEN 0 ELSE C(kz!1+1, i) * i ^ 0 * (-1) ^ (kz!1+1 - i) ENDIF" "kz!1+1" "0" )"1" assert )"1" "1" "1" expand "restrict" )"1" "1" "1" rewrite "expt_1i" )"1" expand "^" +)"1" expand "expt" +)"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "sigma_split" )"2" "LAMBDA (i: nat): IF i > kz!1 + 1 THEN 0" " kz!1 + 1" " 0" " 0") "1" (assert )"1" (replace -1)"1" (hide -1)"1" (expand "sigma" 1 1)"1" (expand "sigma" 1 1)"1" case "0^(1+j!1) = 0" )"1" replace -1)"1" "1" assert )"1" case "NOT (LAMBDA (i: nat): IF i > 1 + kz!1 THEN 0LAMBDA (i: nat):IF i > 1 + kz!1 or i = 0 THEN 0") "1" "1" "1" "1" "1" "1" "1" assert )"1" "1" replace -1)"1" case "0^(1+j!1) = 0" )"1" assert )nil nil )"2" expand "^" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" expand "C" )"2" case "(-1) ^ (1 - x!1 + kz!1) = -(-1)^(kz!1-x!1)" )"1" replace "1" "1" expand "factorial" "1" expand "factorial" "1" case "x!1^(1+j!1) = x!1*x!1^j!1" )"1" replace "1" "1" assert )nil nil ))nil ))nil )"2" expand "^" "2" expand "expt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "kz!1 = x!1" )"1" replace "1" assert )"1" expand "^" "1" expand "expt" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "kz!1 = x!1 -1" )"1" replace "1" assert )"1" expand "^" "1" expand "expt" "1" expand "expt" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" "2" assert )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "sigma_shift_T2" )"2" "(LAMBDA (i: nat): IF i > 1 + kz!1 OR i = 0 THEN 0" "kz!1" "0" "1" )"1" assert )"1" replace -1)"1" "1" "sigma_scal" )"1" "LAMBDA (i_1: nat): IF 1 + i_1 > 1 + kz!1 THEN 0" "(1+kz!1)" "kz!1" "0" )"1" "sigma_restrict_eq" )"1" "LAMBDA (i: nat): IF 1 + i > 1 + kz!1 THEN 0" "LAMBDA (i_1: nat): IF 1 + i_1 > 1 + kz!1 THEN 0" "kz!1" "0" )"1" "1" replace "1" "1" replace "1" "1" "kz!1-1" )"1" "AA" "LAMBDA (i_1: nat): IF 1 + i_1 > 1 + kz!1 THEN 0") "1" replace "1" case "sigma(0,kz!1,AA) = 0" )"1" assert )nil nil )"2" "2" assert )"2" "BB" "LAMBDA (i: nat): IF i > kz!1 THEN 0") "1" replace "1" case "j!1 = 0" )"1" replace "1" assert )"1" case "AA = BB" )"1" assert )nil nil )"2" "2" "2" expand "AA" "2" expand "BB" "2" "2" "2" assert )"2" "2" replace "2" expand "^" "2" expand "expt" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "j!1 = 1" )"1" replace "1" "1" "1" expand "^" "1" expand "expt" "1" expand "expt" "1" expand " ^" "1" expand "expt" "1" expand "expt" "1" "CC" "(LAMBDA (i_1: nat): IF 1 + i_1 > 1 + kz!1 THEN 0") "1" case "AA = BB + CC" )"1" replace "1" "1" "sigma_sum" )"1" "BB" "CC" "kz!1" "0" )"1" expand "+" "1" replace "1" "1" case "sigma(0,kz!1,CC) = 0" )"1" assert )nil nil )"2" "2" replace "2" "2" "2" "2" "binomial_theorem" )"2" "kz!1" "1" "-1" )"2" assert )"2" expand "^" "2" expand "expt" "2" case "(LAMBDA (i: nat): IF i > kz!1 THEN 0LAMBDA (i_1: nat):IF 1 + i_1 > 1 + kz!1 THEN 0") "1" assert )nil nil )"2" "2" "1" "1" "1" "1" assert )"1" "1" case "1^x!1 = 1" )"1" assert )nil nil )"2" rewrite "expt_1i" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace quality 93%
¤ Dauer der Verarbeitung: 0.33 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
