(harmonic_polynomialsnil 3261618989 3276290504"" (skosimp*)"" (lemma "even_div2" ("i" "i!1" ))"" (rewrite "even_or_odd" ) (("" (assert ) nil nil )) nil )) nil ))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 prelude_aux "../reals/" )nil naturalnumbers nil ))nil 3261619116 3261619125"" (grind) nil nil ) proved-completenil 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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" integers nil )"boolean" notequal nil ))nil 3261619130 3261619134"" (grind) nil nil ) proved-complete"bool" integers nil )"boolean" notequal nil ))nil 3261619140 3261619145"" (grind) nil nil ) proved-completenil 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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" integers nil )"boolean" notequal nil ))nil 3261619149 3261619153"" (grind) nil nil ) proved-completenil 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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" integers nil )"boolean" notequal nil ))nil 3261619159 3261619167"" (grind) nil nil ) proved-complete"bool" integers nil )"boolean" notequal 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 )nil integers nil ))nil 3261620027 3261620031"" (grind) nil nil ) proved-completenil 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 )nil integers nil ))nil 3261619175 3276290540"" (skosimp*)"" (lemma "odd_div2" ("i" "i!1" ))"" (rewrite "even_or_odd" ) (("" (assert ) nil nil )) nil )) nil ))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 prelude_aux "../reals/" )nil naturalnumbers nil ))nil 3261619184 3261619188"" (grind) nil nil ) proved-completenil 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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" integers nil )"boolean" notequal nil ))nil 3261619194 3261619199"" (grind) nil nil ) proved-completenil 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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" integers nil )"boolean" notequal nil ))nil 3261619204 3261619209"" (grind) nil nil ) proved-completenil 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 )"bool" reals nil )nil integers nil )nil integers nil )"bool" integers nil )"boolean" notequal nil ))nil 3261620046 3261620052"" (grind) nil nil ) proved-complete"bool" integers nil )"boolean" notequal nil ))nil 3261619224 3261625898"" (skolem 1 ("x" "y" ))"" (expand "harmonic_poly_real" )"" (expand "sigma" )"" (expand "sigma" )"" (rewrite "expt_x0" )"" (rewrite "expt_x1" )"" (rewrite "C_0" )"" (case "odd?(0)" )"1" (expand "odd?" ) (("1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" harmonic_polynomials nil )nil exponentiation nil )"bool" integers 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 binomial nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exponentiation nil )"real" sigma "../reals/" ))nil 3261619351 3261625899"" (skolem 1 ("x" "y" ))"" (expand "harmonic_poly_imag" )"" (expand "sigma" )"" (expand "sigma" )"" (rewrite "expt_x1" )"" (rewrite "expt_x0" )"" (rewrite "C_n" )"" (case "even?(1)" )"1" (expand "even?" ) (("1" (propax) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" harmonic_polynomials nil )nil exponentiation nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"bool" integers 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 binomial nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exponentiation nil )"real" sigma "../reals/" ))nil 3261620367 3261625909"" (skolem 1 ("n" "x" "y" ))"" (expand "harmonic_poly_real" )"" (expand "harmonic_poly_imag" )"" "F1" "LAMBDA (i: nat): IF i > 1 + n OR odd?(i) THEN 0IF i = 0 THEN x ^ (1 + n)") "1" (replace -1)"1" "sigma_scal[nat]" "low" "0" "high" "n" "a" "x" "F" " LAMBDA (i: nat): IF i > n OR odd?(i) THEN 0IF i = 0 THEN x ^ n")) "1" (replace -1 1 rl)"1" (hide -1)"1" "F2" "LAMBDA (i_1: nat): LAMBDA (i: nat):IF i > n OR odd?(i) THEN 0IF i = 0 THEN x ^ n") "1" (replace -1)"1" "F3" "LAMBDA (i: nat): IF i > n OR even?(i) THEN 0IF i = n THEN y ^ n ELSE x ^ (n - i) * y ^ i ENDIF)") "1" (replace -1)"1" "sigma_scal[nat]" "low" "0" "high" "n" "F" "F3" "a" "y" ))"1" (replace -1 1 rl)"1" case "sigma(0, n, F2) = sigma(0, n+1, F2)" )"1" replace -1 1)"1" case "FORALL (n:nat): sigma(0, n, LAMBDA (i: nat): y * F3(i)) = sigma(0,n+1, LAMBDA (i:nat): IF i = 0 THEN 0 ELSE y*F3(i-1) ENDIF)" )"1" "n" )"1" replace -1 1)"1" "sigma_minus[nat]" "low" "0" "high" "n+1" "F" "F2" "G" "LAMBDA (i: nat): IF i = 0 THEN 0 ELSE y * F3(i - 1) ENDIF" ))"1" replace -1 1)"1" "1" "sigma_eq[nat]" "low" "0" "high" "n+1" "F" "F1" "G" "LAMBDA (i_1: nat): LAMBDA (i: nat): IF i = 0 THEN 0 ELSE y * F3(i - 1) ENDIF)")) "1" "1" assert )nil nil )"2" "2" "2" "n!1" )"2" expand "F1" )"2" "2" expand "F2" )"2" expand "F3" )"2" case "n!1=0" )"1" replace "1" rewrite "C_0" )"1" rewrite "C_0" )"1" rewrite "expt_x0" )"1" case "odd?(0)" )"1" expand "odd?" )"1" nil nil ))nil )"2" assert )"2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "n!1= 1+n" )"1" assert )"1" replace "1" rewrite "C_n" )"1" rewrite "C_n" )"1" case "even?(n)" )"1" case "odd?(n+1)" )"1" assert )nil nil )"2" "2" expand "even?" )"2" "2" replace "2" expand "odd?" )"2" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "NOT (odd?(1+n))" )"1" assert )"1" rewrite "even_or_odd" )"1" "1" expand "odd?" )"1" "1" replace "1" "div_cancel1" "x" "j!1" "n0z" "2" ))"1" replace "1" "div_cancel1" "x" "j!1+1" "n0z" "2" ))"1" replace "1" replace "1" replace "1" "n" )"1" expand "^" "1" assert )"1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "odd?" )"2" "2" replace "2" expand "even?" )"2" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "odd?(n!1)" )"1" case "even?(n!1-1)" )"1" assert )nil nil )"2" "2" expand "odd?" )"2" "2" replace "2" expand "even?" )"2" "j!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "NOT (even?(n!1-1))" )"1" assert )"1" rewrite "even_or_odd" )"1" "1" expand "odd?" )"1" "1" "div_cancel1" "x" "1+j!1" "n0z" "2" ))"1" "div_cancel1" "x" "j!1" "n0z" "2" ))"1" case "(n!1 - 2) / 2 = j!1" )"1" replace "1" case "(n!1) / 2 = j!1+1" )"1" replace "1" case "n!1=n" )"1" replace "1" rewrite "C_n" )"1" rewrite "C_n_1" )"1" rewrite "C_n_1" )"1" "expt_plus" "n0x" "-1" "i" "1" "j" "j!1" ))"1" rewrite "expt_x1" "1" replace "1" "K1" "(-1)^j!1" )"1" rewrite "expt_x1" "1" expand "^" "1" expand "expt" "1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "C_n_plus_1" "n" "n" "k" "n!1" ))"2" replace "2" "expt_plus" "n0x" "-1" "i" "1" "j" "j!1" ))"2" rewrite "expt_x1" "2" replace "2" "K10" "(-1)^j!1" )"2" "K11" "C(n,n!1-1)" )"2" "K12" "C(n,n!1)" )"2" expand "^" "2" expand "expt" quality 100%
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.37Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤ *Eine klare Vorstellung vom Zielzustand
