Quelle primes_sum_squares.prf
Sprache: Lisp
(primes_sum_squaresnil 3501936852 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3501939999 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3501939999"" (skeep)"" (expand "sum_of_two_squares?" )"" (expand "sots_int?" )"" (skosimp*)"" (inst + "abs(ai!1)" "abs(bi!1)" )"" (replace -1)"" (hide -) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"nat" exponentiation nil )"bool" primes_sum_squares nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nonneg_int" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"(total_order?[real])" nil )"nzrat" rationalsnil )"int" exponentiation nil )"int" integers nil )"real" exponentiation nil )"real" exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_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 )"{j: nonneg_int | j >= i}" nil )"bool" primes_sum_squares nil )"int" exponentiation nil ))nil 3501936852"" (skeep)"" (typepred "ns" )"" (typepred "ms" )"" (expand "sum_of_two_squares?" )"" (skosimp*)"" (name "vv" "(a!1*b!2-b!1*a!2)" )"" (case "vv>=0" )"1" (inst + "(a!1*a!2 + b!1*b!2)" "vv" )"1" (replace -3)"1" (replace -4)"1" (hide -)"1" (expand "vv" ) (("1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "(a!1*a!2 + b!1*b!2)" "-vv" )"1" (replace -2)"1" (replace -3)"1" (expand "vv" +)"1" (hide-all-but 2) (("1" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" primes_sum_squares 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 )"nat" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"int" integers nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nonneg_int" nil )"int" primes_sum_squares nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" exponentiation nil )"nzrat" rationalsnil )"int" integers nil )"int" exponentiation nil )"real" exponentiation nil )"real" exponentiation nil )"int" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil ))nil 3501939374"" (case "FORALL (k,r:int): divides(k,r) IFF divides(k,-r)" )"1" (label "intlem" -1)"1" (hide "intlem" )"1" case "FORALL (nn, mm: posnat, p: (prime?)): OR divides(p, mm))") "1" (skeep)"1" (case "ai = 0 OR bi=0" )"1" (split -)"1" (replace -1) (("1" (assert ) nil nil )) nil )"2" (replace -1) (("2" (assert ) nil nil )) nil ))nil )"2" (flatten)"2" case "FORALL (nn, mm: posnat, p: (prime?)): OR divides(p, mm))") "1" case "FORALL (nn, mm: posnat, p: (prime?)): OR divides(p, (-mm)))") "1" (case "ai<0" )"1" (case "bi<0" )"1" (assert )"1" (inst -3 "-ai" "-bi" "p" )"1" (assert ) nil nil )) nil ))nil )"2" (inst -3 "-ai" "bi" "p" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil )"2" (case "bi<0" )"1" (inst -3 "-bi" "ai" "p" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil )"2" (inst -3 "ai" "bi" "p" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (hide (2 3 4 5 6))"2" (skosimp*)"2" (inst - "nn!1" "mm!1" "p!1" )"2" (assert )"2" (split -)"1" "intlem" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "intlem" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (2 3 4 5 6))"2" (skosimp*)"2" (inst - "nn!1" "mm!1" "p!1" )"2" (assert )"2" (split -)"1" (reveal "intlem" )"1" "1" (assert ) nil nil ))nil ))nil )"2" (reveal "intlem" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "divides" -)"2" (skolem -1 "r" )"2" case "FORALL (kr:posnat): (NOT divides(p,kr)) IMPLIES gcd(p,kr) = 1" )"1" (inst - "mm" )"1" (assert )"1" (lemma "gcd_factors" )"1" (inst?)"1" (assert )"1" "1" replace -2)"1" "nn" )"1" assert )"1" expand "divides" 1)"1" "vv" "ip!1*nn + jp!1*r" )"1" case "nn=p*vv" )"1" case "vv > 0" )"1" "vv" )nil nil )"2" "posreal_times_posreal_is_posreal" )"2" "p" "-vv" )"1" assert )nil nil )"2" assert )nil nil )"3" "p" )"3" expand "prime?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skeep)"2" (typepred "gcd(p,kr)" )"2" (typepred "p" )"2" (expand "prime?" )"2" "2" "gcd(p,kr)" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (k, r: int): divides(k, r) IMPLIES divides(k, -r)" )"1" (skeep)"1" (ground)"1" (inst - "k" "r" ) (("1" (assert ) nil nil )) nil )"2" (inst - "k" "-r" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "divides" )"2" (skosimp*)"2" (inst + "-x!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"bool" primes "ints/" )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"[T, T -> boolean]" equalities nil )"even_int" integersnil )"even_int" integersnil )"nzint" integersnil )"nzint" integers nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" primes_sum_squares nil )"int" primes_sum_squares nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil gcd "ints/" )"(prime?)" primes_sum_squares nil )"int" primes_sum_squares nil )nil real_types nil )nil real_types nil )nil real_types nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_props nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"boolean" notequal nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers 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, bool -> bool]" booleans nil )"bool" divides nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil ))nil 3501939374"" (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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" primes_sum_squares nil )"bool" primes_sum_squaresnil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"bool" primes "ints/" )"real" exponentiation nil )"bool" divides nil )"boolean" notequal nil ))nil ))nil 3501939374"" (skeep)"" (expand "divides" )"" (skosimp*)"" (case "ns/ps = x!1" )"1" (assert )"1" (cross-mult 1) (("1" (assert ) nil nil )) nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" divides nil )"bool" primes_sum_squaresnil )"bool" primes_sum_squares 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 )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"rat" rationals nil )nil real_props nil )"(total_order?[real])" nil )"nonneg_int" nil )"even_int" integersnil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil reals nil )nil real_props nil ))nil ))nil 3501939558"" case "FORALL (rr:nzint,rs:int): divides(rr,rs) IMPLIES integer_pred(rs/rr)" )"1" (label "integerpredlem" -1)"1" (hide "integerpredlem" )"1" case "FORALL (rr,rs:int): divides(rr,rs) IFF divides(rr,-rs)" )"1" (label "intlem" -1)"1" (hide "intlem" )"1" (skeep)"1" (typepred "ns" )"1" (typepred "ps" )"1" case "EXISTS (a,b,pp,qq:nat): ns = a^2+b^2 AND ps = pp^2+qq^2" )"1" (skeep -1)"1" (hide -3)"1" (hide -3)"1" case "divides(ps,(pp*b-a*qq)*(pp*b+a*qq))" )"1" "prime_divides" )"1" "1" assert )"1" "1" "1" case "divides(ps,(a*pp+b*qq)^2)" )"1" case "divides(ps^2,(a*pp+b*qq)^2)" )"1" "f1" "(a*pp+b*qq)/ps" )"1" "f2" "(a*qq-b*pp)/ps" )"1" "sots_int_def" )"1" "1" assert )"1" "1" case "integer_pred(f1) and integer_pred(f2)" )"1" "1" expand "sots_int?" )"1" "f1" "f2" )"1" replace "1" replace "1" expand "f1" "1" expand "f2" "1" replace "1" case "ps*(a^2+b^2) = (a * qq - b * pp)^2+(a * pp + b * qq)^2" )"1" "1" "pz" "a^2+b^2" )"1" replace "1" "1" "zz" "(a * qq - b * pp)" )"1" replace "1" "sz" "(a * pp + b * qq)" )"1" replace "1" "1" "1" "1" "ps^2" )"1" "1" nil nil ))nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" expand "prime?" )"2" "2" "posreal_times_posreal_is_posreal" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integerpredlem" )"2" "1" expand "f1" "1" "1" assert )"1" "prime_divides" )"1" "a*pp+b*qq" "a*pp+b*qq" "ps" )"1" assert )"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "f2" "2" "2" assert )"2" "intlem" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integerpredlem" )"2" "2" assert )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" expand "prime?" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "prime_divides" )"2" "a*pp+b*qq" "a*pp+b*qq" "ps" )"1" assert )"1" case "divides(ps, a * pp + b * qq)" )"1" "1" expand "divides" "1" "1" "x!1^2" )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "^" )"2" expand "expt" "2" expand "expt" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "divides_sum" )"2" "ns*ps" "-(a*qq-b*pp)^2" "ps" )"2" "1" replace -3 -1)"1" replace -4 -1)"1" "divides" "sum_of_two_squares?" ))nil nil ))nil ))nil )"2" "2" expand "divides" )"2" "2" "x!1*(-pp*b+a*qq)" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "divides" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "divides(ps,(a*pp-b*qq)^2)" )"1" case "divides(ps^2,(a*pp-b*qq)^2)" )"1" "f1" "(a*pp-b*qq)/ps" )"1" "f2" "(a*qq+b*pp)/ps" )"1" "sots_int_def" )"1" "1" assert )"1" "1" case "integer_pred(f1) and integer_pred(f2)" )"1" "1" expand "sots_int?" )"1" "f1" "f2" )"1" replace "1" replace "1" expand "f1" "1" expand "f2" "1" replace "1" case "ps*(a ^ 2 + b ^ 2) = ") "1" "1" "pz" "a^2+b^2" )"1" replace "1" "1" "zz" "(a * pp - b * qq)" )"1" replace "1" "sz" "(a * qq + b * pp)" )"1" replace "1" "1" "1" "1" "ps^2" )"1" "1" nil nil ))nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" expand "prime?" )"2" "2" "posreal_times_posreal_is_posreal" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "1" expand "f1" "1" assert )"1" "prime_divides" )"1" case "FORALL (i:int,p:(prime?)): divides(p,i^2) IMPLIES divides(p,i)" )"1" "integerpredlem" )"1" "1" assert )"1" "a*pp-b*qq" "ps" )"1" assert )nil nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "i!1>=0" )"1" "i!1" "i!1" "p!1" )"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "-i!1" "-i!1" "p!1" )"2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" assert )"2" "intlem" )"2" "p!1" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "f2" "2" "integerpredlem" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "integerpredlem" )"2" "2" assert )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" expand "prime?" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "prime_divides" )"2" case "FORALL (i:int,p:(prime?)): divides(p,i^2) IMPLIES divides(p,i)" )"1" "a*pp-b*qq" "ps" )"1" assert )"1" "1" "1" expand "divides" "1" "1" "x!1^2" )"1" replace "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" nil nil ))nil ))nil ))nil )"2" "2" "2" case "i!1>=0" )"1" "i!1" "i!1" "p!1" )"1" assert )"1" "divides" ))nil nil ))nil ))nil )"2" "-i!1" "-i!1" "p!1" )"2" "intlem" )"2" "p!1" "i!1" )"2" "divides" ))nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "divides_sum" )"2" "ns*ps" "-(a*qq+b*pp)^2" "ps" )"2" "1" replace -3 -1)"1" replace -4 -1)"1" "divides" "sum_of_two_squares?" ))nil nil ))nil ))nil )"2" "2" expand "divides" )"2" "2" "-x!1*(pp*b+a*qq)" )"2" nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "divides" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ps" )"2" expand "prime_sum_of_two_squares?" )"2" (ground) nil nil ))nil ))nil ))nil ))nil )"2" expand "divides" )"2" "2" "pp^2*x!1-a^2" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "prime_sum_of_two_squares?" )"2" (expand "sum_of_two_squares?" )"2" (flatten)"2" (skosimp*)"2" "a!2" "b!2" "a!1" "b!1" )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (rr, rs: int): divides(rr, rs) IMPLIES divides(rr, -rs)" )"1" (skeep)"1" (ground)"1" (inst?) (("1" (assert ) nil nil )) nil )"2" (inst - "rr" "-rs" ) (("2" (assert ) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "divides" )"2" (skosimp*)"2" (inst + "-x!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (expand "divides" )"2" (skosimp*)"2" (case "rs/rr=x!1" )"1" (assert )"1" (replace -1) (("1" (assert ) nil nil )) nil )) nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" primes_sum_squares nil )"nonneg_int" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"nat" exponentiation nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"bool" primes "ints/" )"(prime_sum_of_two_squares?)" nil )"rat" primes_sum_squares nil )"rat" primes_sum_squares nil )"(total_order?[real])" nil )nil rationals nil )nil primes_sum_squares nil )nil real_props nil )"int" exponentiation nil )"bool" primes_sum_squares nil )"rat" exponentiation nil )"real" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"nat" exponentiation nil )"rat" rationals nil )"rat" exponentiation nil )"rat" rationals nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil reals nil )nil real_props nil )nil integers nil )"int" integers nil )"rat" primes_sum_squares nil )"rat" primes_sum_squares nil )"even_int" integersnil )"(sum_of_two_squares?)" primes_sum_squaresnil )nil divides nil )nil primes_sum_squares nil )"bool" primes_sum_squaresnil )"rat" rationals 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 )"boolean" notequal nil )nil integers nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )"bool" divides nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))nil 3502100866"" (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 )"(total_order?[real])" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exponentiation nil )"bool" primes_sum_squares nil )"bool" divides nil )"boolean" notequal nil )"nat" exponentiation nil ))nil ))nil 3502100866"" (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 )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exponentiation nil )"bool" primes_sum_squares nil )"bool" divides nil )"nat" exponentiation nil )"rat" rationals nil ))nil ))nil 3502100866"" case "FORALL (iii,jjj:int): integer_pred(iii*jjj) and rational_pred(iii*jjj) and rational_pred(iii)" )"1" (label "intlem" -1)"1" (hide "intlem" )"1" (skeep)"1" (case "ns /= 0" )"1" (label "nsnz" -1)"1" (hide "nsnz" )"1" (expand "divides" -)"1" (skolem -2 "rr" )"1" (lemma "prime_factors" )"1" (inst - "rr" )"1" (skosimp*)"1" (replace -1)"1" (expand "product " -4)"1" "1" "1" expand "ordered_list_of_primes?" )"1" "1" expand "list_of_primes?" )"1" case "FORALL (jj:nat,zz:nat): jj+zz<=length(fs!1)-1 IMPLIES m*product[nat](jj,jj+zz,fs!1`seq)>0" )"1" "prodposm" -1)"1" "prodposm" )"1" case "FORALL (ii:nat): ii<=length(fs!1) IMPLIES sum_of_two_squares?(m * product(0, length(fs!1) - 1-ii, fs!1`seq))" )"1" "length(fs!1)" )"1" assert )nil nil ))nil )"2" "ii" )"1" assert )nil nil )"2" "2" assert )"2" expand "product" "2" "sots_div_prime_closed" )"2" "m * " "fs!1`seq(length(fs!1) - 1 - j)" )"1" assert )"1" expand "divides" "1" "m * ") "1" assert )nil nil ))nil ))nil ))nil )"2" expand "prime_sum_of_two_squares?" )"2" case "prime?(fs!1`seq(length(fs!1) - 1 - j))" )"1" assert )"1" "fs!1`seq(length(fs!1) - 1 - j)" )"1" assert )"1" expand "divides" "1" "product[nat](0,length(fs!1) - 2 - j,fs!1`seq)*product(length(fs!1)-j,length(fs!1)-1,fs!1`seq)" )"1" case "fs!1`seq(length(fs!1) - 1 - j) * eq)") "1" assert )nil nil )"2" "2" "product_split" )"2" "fs!1`seq" "length(fs!1)-1" "0" "length(fs!1)-1-j" )"2" assert )"2" expand "product" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "intlem" )"2" "2" assert )"2" "2" "2" "length(fs!1)-1-j" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" "2" )"3" assert )nil nil ))nil ))nil ))nil )"4" assert )"4" "4" assert )nil nil ))nil ))nil ))nil )"3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "zz" )"1" assert )"1" "1" expand "product" +)"1" expand "product" "1" assert )"1" "fs!1`seq(jj)" )"1" "m" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "zz" )"2" "2" "2" "jj" )"2" assert )"2" expand "product" "2" "fs!1`seq(1+jj+zz)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "rr>0" )"1" (assert ) nil nil )"2" (hide 2)"2" case "rr = ns/m" )"1" replace -1 +)"1" "1" "1" "nsnz" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (cross-mult 1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1)"2" (inst + "m" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (skeep) (("2" (assert ) nil nil )) nil )) nil ))nil )"bool" divides nil )nil prime_factorization nil )nil real_props nil )nil reals nil )nil extra_real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"posnat" product_fseq_posnat "reals/" )"nonneg_int" nil )"nnreal" product_nat "reals/" )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil fseqs "structures/" )nil fseqs "structures/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil product "reals/" )nil product "reals/" )"real" product "reals/" )"fseq[posnat]" primes_sum_squares nil )nil defined_types nil )nil naturalnumbers nil )nil naturalnumbers nil )"nat" primes_sum_squares nil )"bool" reals nil )"posnat" product_nat "reals/" )"posreal" product_nat "reals/" )"nat" product_nat "reals/" )"posint" nil )nil primes_sum_squares nil )"rat" rationals nil )"odd_int" integersnil )nil product "reals/" )"[T, T -> boolean]" equalities nil )"bool" primes "ints/" )"posint" nil )"bool" primes_sum_squaresnil )"nat" primes_sum_squares nil )"nat" primes_sum_squares nil )"posint" nil )nil product_nat "reals/" )"posnat" product_fseq_posnat"reals/" )nil real_props nil )nil real_types nil )nil real_types nil )"even_int" integersnil )NOT const-decl "[bool -> bool]" booleans nil )"bool" prime_factorization nil )"bool" prime_factorization nil )nil integers nil )nil integers nil )"bool" reals nil )"int" primes_sum_squares nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" primes_sum_squares nil )nil naturalnumbers nil )"bool" reals nil )"boolean" notequal nil )"(divides(n))" divides nil )"(divides(m))" divides 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 )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3502105281"" (subtype-tcc) nil nil ) nil nil ))nil 3502105281"" (subtype-tcc) nil nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"bool" gcd "ints/" ))nil ))nil 3502105281"" (subtype-tcc) nil nil )"bool" divides nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"bool" gcd "ints/" ))nil ))"" 3539699252"" case "FORALL (m:nat, n: nat, pa, pb: int): n<=m AND NOT (pa=0 AND pb=0)) AND rel_prime(pa, pb) AND divides(n, pa ^ 2 + pb ^ 2) IMPLIES") "1" (skeep)"1" (inst - "n" "n" "pa" "pb" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "m" )"1" (skeep)"1" (case "n = 0" )"1" (replace -1)"1" (hide -)"1" (expand "sum_of_two_squares?" )"1" (inst + "0" "0" ) (("1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (label "papbnz" 1)"2" (case "NOT j = n-1" )"1" (inst - "n" "pa" "pb" ) (("1" (assert ) nil nil ))nil )"2" (hide "papbnz" )"2" (replace -1)"2" (hide -3)"2" (name "xx" "n" )"2" (replace -1)"2" (case "xx > 0" )"1" (label "xxpos" -1)"1" "xxpos" )"1" "hyp" -3)"1" "1" "hyp" )"1" case "divides(xx,pa) AND divides(xx,pb)" )"1" "1" "divides_gcd" )"1" "pa" "pb" "xx" )"1" assert )"1" expand "rel_prime" )"1" replace -4)"1" case "xx = 1" )"1" replace -1)"1" "1" expand "sum_of_two_squares?" )"1" "0" "1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "papbnz" )"2" "1" expand "divides" )"1" "1" case "x!1 > 1" )"1" "xx" )"1" assert )nil nil ))nil )"2" case "x!1 = 1" )"1" assert )nil nil )"2" "posreal_times_posreal_is_posreal" )"2" "-x!1" "xx" )"1" assert )nil nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -1)"2" "2" expand "sum_of_two_squares?" )"2" "0" "0" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xxdivpapb" 1)"2" "xxdivpapb" )"2" "divxx" -2)"2" "papbrp" -1)"2" case "EXISTS (cc,dd:int,mm,nn:int): abs(cc)<=xx/2 AND abs(dd)<=xx/2 AND pa = mm*xx+cc AND pb = nn*xx+dd" )"1" "1" "ccabs" "1" "ddabs" "1" "ccdef" "1" "dddef" "1" case "(cc = 0 AND dd = 0)" )"1" "1" replace "1" replace "1" "xxdivpapb" )"1" expand "divides" "1" "1" "mm" )"1" assert )nil nil ))nil )"2" "nn" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ccddnz" "2" "ccddnz" )"2" case "EXISTS (AA:int): pa^2 + pb^2 = AA*xx + (cc^2 + dd^2)" )"1" "AAdef" "1" "1" case "NOT rel_prime(gcd(cc,dd),xx)" )"1" expand "rel_prime" "1" case "divides(gcd(cc,dd),pa) AND divides(gcd(cc,dd),pb)" )"1" "1" "divides_gcd" )"1" "pa" "pb" "gcd(cc,dd)" )"1" assert )"1" "1" expand "rel_prime" )"1" replace "papbrp" )"1" assert )"1" expand "divides" "1" "1" case "x!1 > 1" )"1" "gcd(cc,dd)" )"1" assert )nil nil ))nil )"2" case "x!1 = 1" )"1" replace "1" assert )"1" replace "1" assert )"1" "1" "gcd(1,xx)" )"1" "1" expand "divides" )"1" "1" case "x!2 > 1" )"1" "gcd(1,xx)" )"1" assert )nil nil ))nil )"2" case "x!2 = 1" )"1" assert )nil nil )"2" assert )"2" case "x!2 < 0" )"1" "posreal_times_posreal_is_posreal" )"1" "-x!2" "gcd(1,xx)" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "posreal_times_posreal_is_posreal" )"2" "-x!1" "gcd(cc,dd)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "papbnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (ab1,mn1,cd1,dg1:int): divides(dg1,cd1) AND divides(dg1,xx) AND ab1 = mn1*xx + cd1 IMPLIES divides(dg1,ab1)" )"1" "pa" "mm" "cc" "gcd(gcd(cc,dd),xx)" )"1" "pb" "nn" "dd" "gcd(gcd(cc,dd),xx)" )"1" assert )"1" case "FORALL (rrz,xxz,ccz:int): divides(rrz,xxz) AND divides(xxz,ccz) IMPLIES divides(rrz,ccz)" )"1" "1" "1" "1" assert )"1" "papbrp" )"1" expand "rel_prime" "1" "divides_gcd" )"1" "pa" "pb" "gcd(gcd(cc,dd),xx)" )"1" assert )"1" "1" replace "1" "1" expand "divides" )"1" "1" case "x!1 > 1" )"1" "gcd(gcd(cc,dd),xx)" )"1" assert )nil nil ))nil )"2" case "x!1 = 1" )"1" replace "1" assert )nil nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "-x!1" "gcd(gcd(cc,dd),xx)" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "papbnz" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "gcd(gcd(cc,dd),xx)" "gcd(cc,dd)" "cc" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "gcd(gcd(cc,dd),xx)" "gcd(cc,dd)" "dd" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "divides" )"2" "2" replace "2" "x!1*x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "divides" )"2" "2" replace "2" replace "2" "mn1*x!2 + x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "divides(xx,cc^2 + dd^2)" )"1" "ccddxxrp" "1" "xxccdddiv" "1" expand "divides" "1" "yy" )"1" case "divides(gcd(cc,dd)^2,yy)" )"1" "ccddsqyydiv" "1" expand "divides" "1" "1" case "EXISTS (ee,ff:int): ee = cc/gcd(cc,dd) AND ff = dd/gcd(cc,dd)" )"1" "1" "eedef" "1" "ffdef" "1" case "(ee = 0 AND ff = 0)" )"1" "ccddnz" )"1" "1" "1" replace "1" replace "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "eeffnz" "2" case "ee^2 + ff^2 > 0" )"1" "eeffnz" )"1" "eeffsqpos" "1" case "divides(xx,ee^2 + ff^2)" )"1" "1" expand "divides" "1" "zz" )"1" case "zz > 0" )"1" "zzpos" "1" "zzdef" "1" case "abs(zz) <= xx/2" )"1" "abszz" "1" case "rel_prime(ee,ff)" )"1" "sots_div_quot_factor" )"1" "xx" "ee^2 + ff^2" )"1" assert )"1" "1" "1" "hyp" )"1" "b" "ee" "ff" )"1" assert )"1" case "b <=zz" )"1" assert )"1" "eeffnz" )"1" replace "1" "eeffnz" )"1" "1" expand "divides" )"1" "1" "1" "x!2*xx" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace "zzdef" )"2" assert )"2" expand "divides" "2" "2" "2" "xx" )"2" case "x!2 > 1" )"1" "b*xx" )"1" assert )nil nil ))nil )"2" case "x!2 = 1" )"1" replace "1" assert )nil nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "b*xx" "-x!2" )"1" assert )nil nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "sum_of_two_squares?" )"2" "abs(ee)" "abs(ff)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "sum_of_two_squares?" )"2" "abs(ee)" "abs(ff)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "eedef" "ffdef" "2" "gcd_factors" )"2" "cc" "dd" )"2" assert )"2" "ccddnz" )"2" "1" "ccddnz" )"1" "1" rewrite "rel_prime_lem" )"1" "jp!1" "ip!1" )"1" "gcd(cc,dd)" )"1" assert )nil nil ))nil ))nil )"2" "eeffnz" )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "eeffnz" )"3" nil nil ))nil ))nil ))nil )"2" case "xx*zz <= xx^2/2" )"1" case "zz <= xx/2" )"1" case "zz>=0" )"1" "1" nil nil ))nil )"2" assert )nil nil ))nil )"2" "xxpos" )"2" "2" "xx" )"2" nil nil ))nil ))nil ))nil ))nil )"2" case "ee^2 <= cc^2 AND ff^2 <= dd^2 AND cc^2<=xx^2/4 AND dd^2 <= xx^2/4" )"1" "1" assert )nil nil ))nil )"2" case "gcd(cc,dd)^2 >=1" )"1" "1" replace "eedef" "1" rewrite "div_expt" )"1" "1" "cc^2" )"1" assert )nil nil )"2" "2" "nnreal_times_nnreal_is_nnreal" )"2" "abs(cc)" "abs(cc)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "ffdef" "2" rewrite "div_expt" )"2" "2" "dd^2" )"1" assert )nil nil )"2" "2" "nnreal_times_nnreal_is_nnreal" )"2" "abs(dd)" "abs(dd)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ccabs" )"3" "3" "1" expand "^" "1" expand "expt" "1" expand "expt" "1" expand "expt" "1" "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"4" "ddabs" )"4" "4" "1" "1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "gcd(cc,dd) >= 1" )"1" "1" "1" expand "^" "1" expand "expt" "1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xxpos" )"2" "posreal_times_posreal_is_posreal" )"2" "-zz" "xx" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xxccdddiv" )"2" "eedef" )"2" "2" replace "2" "2" "ffdef" )"2" "2" case "dd^2 = (ff*gcd(cc,dd))^2" )"1" replace "1" "1" "rel_prime_div_prod" )"1" "xx" "gcd(cc,dd)" "gcd(cc,dd)*(ee^2 + ff^2)" )"1" assert )"1" "1" "rel_prime_div_prod" )"1" "xx" "gcd(cc,dd)" "ee^2 + ff^2" )"1" assert )"1" rewrite "rel_prime_sym" nil nil ))nil ))nil ))nil )"2" rewrite "rel_prime_sym" nil nil )"3" "3" expand "divides" )"3" "yy" )"3" "gcd" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nnreal_times_nnreal_is_nnreal" )"2" "abs(ee)" "abs(ee)" )"2" "abs(ff)" "abs(ff)" )"2" case "ee^2 = 0 IMPLIES ee = 0" )"1" case "ff^2 = 0 IMPLIES ff = 0" )"1" nil nil )"2" "nzreal_times_nzreal_is_nzreal" )"2" "2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nzreal_times_nzreal_is_nzreal" )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" "1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "gcd(cc,dd)" )"2" expand "divides" )"2" "2" "x!2" "x!3" )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "rel_prime(gcd(cc,dd)^2,xx)" )"1" "rel_prime_div_prod" )"1" "gcd(cc,dd)^2" "xx" "yy" )"1" assert )"1" replace "xxccdddiv" "1" "1" "gcd(cc,dd)" )"1" expand "divides" )"1" "1" "1" "1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" replace "1" replace "1" "x!1^2 + x!2^2" )"1" "1" "gcd" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "^" "2" expand "expt" "2" expand "expt" "2" expand "expt" "2" rewrite "rel_prime_mult_left" )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "AAdef" "divxx" "2" expand "divides" )"2" "2" replace "divxx" )"2" "x!1-AA" )"2" "^" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" assert )nil nil ))nil )"4" assert )"4" "4" assert )"4" "ccddnz" )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "ccdef" "2" replace "dddef" "2" expand "^" "2" expand "expt" "2" expand "expt" "2" expand "expt" "2" assert )"2" "mm*mm*xx + nn*nn*xx +2*cc*mm+2*dd*nn" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "xxpos" )"2" case "FORALL (aa:int): EXISTS (nn,kk:int): abs(kk)<=xx/2 AND aa = nn*xx+kk" )"1" "pa" )"1" "pb" )"1" "1" "kk!2" "kk!1" "nn!2" "nn!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "EXISTS (nn:int): nn*xx <= aa AND (nn+1)*xx > aa" )"1" "1" "1" "nn" "aa-nn*xx" )"1" "nn+1" "aa-(nn+1)*xx" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (a:nat): EXISTS (nn: int): nn * xx <= a AND (nn + 1) * xx > a" )"1" case "NOT aa < 0" )"1" "aa" )"1" assert )nil nil ))nil )"2" "-aa" )"1" "1" case "nn!1*xx = -aa" )"1" "-nn!1" )"1" assert )nil nil ))nil )"2" "-nn!1-1" )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" "axiom_of_archimedes" )"2" "2" case "FORALL (ii:nat): ii*xx <= a" )"1" "a/xx" )"1" case "EXISTS (i:nat): a/xx < i" )"1" "1" "1" "1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "nnreal_div_posreal_is_nnreal" )"2" "a" "xx" )"2" assert )"2" "i!1" )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" "ii" )"1" assert )nil nil )"2" "2" "j!1" )"2" 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 ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (ground) nil nil )) nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (ground) nil nil )) nil ))nil ))nil )"nonneg_rat" nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil abs_rews "ints/" )"{j: nonneg_int | j >= i}" nil )"{k: posnat | divides(k, i) AND divides(k, j)}" gcd"ints/" )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"int" primes_sum_squares nil )"rat" rationals nil )nil real_props nil )nil reals nil )nil gcd "ints/" )nil gcd "ints/" )"int" primes_sum_squares nil )"int" primes_sum_squares nil )"int" primes_sum_squares nil )nil abs_rews "ints/" )nil real_props nil )"int" primes_sum_squares nil )"nat" primes_sum_squares nil )nil real_props nil )"int" exponentiation nil )nil primes_sum_squares nil )nil gcd "ints/" )nil real_props nil )nil gcd "ints/" )"odd_int" integers nil )nil extra_real_props nil )nil reals nil )nil exponentiation nil )"rat" exponentiation nil )nil extra_real_propsnil )"int" primes_sum_squares nil )nil real_types nil )nil real_props nil )"int" primes_sum_squares nil )"{r: nonneg_rat | r >= q}" nil )nil extra_real_props nil )"nonneg_rat" nil )nil real_types nil )nil gcd "ints/" )"int" primes_sum_squares nil )nil real_props nil )nil real_props nil )nil real_types nil )"nat" primes_sum_squares nil )nil integers nil )"posnat" exponentiation nil )"posrat" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )nil real_props nil )nil real_types nil )"int" primes_sum_squares nil )"[numfield -> numfield]" number_fields nil )"int" integers nil )nil gcd "ints/" )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"int" exponentiation nil )"nat" exponentiation nil )"nonneg_int" nil )"nat" exponentiation nil )"nzrat" rationalsnil )"(total_order?[real])" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"posint" exponentiation nil )"posint" nil )nil integers nil )"bool" reals nil )nil integers nil )"int" integers 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 )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"bool" gcd "ints/" )"bool" divides nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"bool" primes_sum_squares nil ))nil )"" 3539694599"" case "FORALL (m:nat, n: nat, pa, pb: posnat): n<=m AND AND divides(n, pa ^ 2 + pb ^ 2) IMPLIES") "1" (skeep)"1" (inst - "n" "n" "pa" "pb" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "m" )"1" (skeep)"1" (case "n = 0" )"1" (replace -1)"1" (hide -)"1" (expand "sum_of_two_squares?" )"1" (inst + "0" "0" ) (("1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (case "NOT j = n-1" )"1" (inst - "n" "pa" "pb" ) (("1" (assert ) nil nil ))nil )"2" (replace -1)"2" (hide -3)"2" (name "xx" "n" )"2" (replace -1)"2" (label "hyp" -3)"2" (hide (-1 -2))"2" (hide "hyp" )"2" case "divides(xx,pa) AND divides(xx,pb)" )"1" "1" "divides_gcd" )"1" "pa" "pb" "xx" )"1" assert )"1" expand "rel_prime" )"1" replace -4)"1" case "xx = 1" )"1" replace -1)"1" "1" expand "sum_of_two_squares?" )"1" "0" "1" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "divides" )"2" "2" case "x!1 > 1" )"1" "xx" )"1" assert )nil nil ))nil )"2" case "x!1 = 1" )"1" assert )nil nil )"2" "posreal_times_posreal_is_posreal" )"2" "-x!1" "xx" )"1" assert )nil nil )"2" assert )nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -1)"2" "2" expand "sum_of_two_squares?" )"2" "0" "0" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xxdivpapb" 1)"2" "xxdivpapb" )"2" "divxx" -2)"2" "papbrp" -1)"2" case "EXISTS (cc,dd,mm,nn:nat): abs(cc)<=xx/2 AND abs(dd)<=xx/2 AND pa = mm*xx+cc AND pb = nn*xx+dd" )"1" "1" case "(cc = 0 AND dd = 0)" )"1" "1" replace -1)"1" replace -2)"1" "xxdivpapb" )"1" expand "divides" "1" "1" "mm" )"1" assert )nil nil ))nil )"2" "nn" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ccddnz" 1)"2" "ccddnz" )"2" case "EXISTS (AA:int): pa^2 + pb^2 = AA*xx + (cc^2 + dd^2)" )"1" "1" case "NOT rel_prime(gcd(cc,dd),xx)" )"1" expand "rel_prime" "1" case "divides(gcd(cc,dd),pa) AND divides(gcd(cc,dd),pb)" )"1" "1" "divides_gcd" )"1" "pa" "pb" "gcd(cc,dd)" )"1" assert )"1" expand "rel_prime" )"1" replace "papbrp" )"1" assert )"1" expand "divides" "1" "1" case "x!1 > 1" )"1" "gcd(cc,dd)" )"1" assert )nil nil ))nil )"2" case "x!1 = 1" )"1" replace "1" assert )"1" replace "1" assert )"1" "1" "gcd(1,xx)" )"1" "1" expand "divides" )"1" "1" case "x!2 > 1" )"1" "gcd(1,xx)" )"1" assert )nil nil ))nil )"2" case "x!2 = 1" )"1" assert )nil nil )"2" assert )"2" case "x!2 < 0" )"1" "posreal_times_posreal_is_posreal" )"1" "-x!2" "gcd(1,xx)" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "posreal_times_posreal_is_posreal" )"2" "-x!1" "gcd(cc,dd)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (ab1,mn1,cd1,dg1:nat): divides(dg1,cd1) AND divides(dg1,xx) AND ab1 = mn1*xx + cd1 IMPLIES divides(dg1,ab1)" )"1" "pa" "mm" "cc" "gcd(gcd(cc,dd),xx)" )"1" "pb" "nn" "dd" "gcd(gcd(cc,dd),xx)" )"1" assert )"1" case "FORALL (rrz,xxz,ccz:int): divides(rrz,xxz) AND divides(xxz,ccz) IMPLIES divides(rrz,ccz)" )"1" "1" "1" "1" assert )"1" "papbrp" )"1" expand "rel_prime" "1" "divides_gcd" )"1" "pa" "pb" "gcd(gcd(cc,dd),xx)" )"1" assert )"1" replace "1" "1" expand "divides" )"1" "1" case "x!1 > 1" )"1" "gcd(gcd(cc,dd),xx)" )"1" assert )nil nil ))nil )"2" case "x!1 = 1" )"1" replace "1" assert )nil nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "-x!1" "gcd(gcd(cc,dd),xx)" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "gcd(gcd(cc,dd),xx)" "gcd(cc,dd)" "cc" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "gcd(gcd(cc,dd),xx)" "gcd(cc,dd)" "dd" )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "divides" )"2" "2" replace "2" "x!1*x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "divides" )"2" "2" replace "2" replace "2" "mn1*x!2 + x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "divides(xx,cc^2 + dd^2)" )"1" expand "divides" "1" "yy" )"1" case "divides(gcd(cc,dd)^2,yy)" )"1" expand "divides" "1" "1" case "EXISTS (ee,ff:nat): ee = cc/gcd(cc,dd) AND ff = dd/gcd(cc,dd)" )"1" "1" case "(ee = 0 AND ff = 0)" )"1" "ccddnz" )"1" "1" "1" replace "1" replace "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "eeffnz" "2" "eeffnz" )"2" case "ee <= cc AND ff <= dd" )"1" "1" case "divides(xx,ee^2 + ff^2)" )"1" "1" expand "divides" "1" "zz" )"1" case "abs(zz) <= xx/2" )"1" case "rel_prime(ee,ff)" )"1" "sots_div_quot_factor" )"1" "xx" "ee^2 + ff^2" )"1" assert )"1" "1" "1" "hyp" )"1" "b" "ee" "ff" )"1" assert )"1" case "zz>=0" )"1" expand "abs" )"1" assert )"1" case "b <=zz" )"1" assert )"1" "1" expand "divides" )"1" "1" "1" "x!2*xx" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace "2" assert )"2" case "zz = 0" )"1" replace "1" "1" "eeffnz" )"1" case "FORALL (ee1:real): ee1^2 >= 0" )"1" "ee" )"1" "ff" )"1" case "FORALL (xr:real): xr^2 =0 IMPLIES xr = 0" )"1" "ee" )"1" "ff" )"1" assert )nil nil ))nil ))nil )"2" "2" "2" "nzreal_times_nzreal_is_nzreal" )"2" "xr" "xr" )"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "zzero" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"3" nil nil )"4" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)nil 3502105281"" case "FORALL (m: nat): FORALL (n:nat, pa, pb: posnat): n<=m AND AND divides(n, pa ^ 2 + pb ^ 2) IMPLIES") "1" (skeep)"1" (inst - "n" )"1" (inst - "n" "pa" "pb" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "m" )"1" (skeep)"1" (case "n = 0" )"1" (replace -1)"1" (hide -)"1" (expand "sum_of_two_squares?" )"1" (inst + "0" "0" ) (("1" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (assert )"2" (label "oldlem" -1)"2" (skeep)"2" (name "xx" "n" )"2" (replace -1)"2" (hide -1)"2" (case "xx > 0" )"1" (label "xxpos" -1)"1" case "NOT (FORALL (kk:posnat): kk >= 2 IMPLIES NOT divides(kk^2,xx))" )"1" "1" case "kk^2 >= 4" )"1" case "kk^2 < xx" )"1" "divideskkx" -4)"1" "kge2" -3)"1" "kkge4" -2)"1" "kkltx" -1)"1" case "EXISTS (nn:posnat): nn = xx/kk^2" )"1" "1" case "nn < xx" )"1" "nndef" -2)"1" "nnltx" "1" case "divides(nn,pa^2 + pb^2)" )"1" "nn" "pa" "pb" )"1" assert )"1" "oldlem" "1" expand "sum_of_two_squares?" )"1" "1" replace "1" "oldlem" )"1" "1" "a!1*kk" "b!1*kk" )"1" replace "1" "1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (a1,b1,c1:nat): divides(a1,b1) AND divides(b1,c1) IMPLIES divides(a1,c1)" )"1" "nn" "xx" "pa^2 + pb^2" )"1" assert )"1" expand "divides" "1" "kk^2" )"1" "kk^2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "divides" )"2" "2" replace "2" "2" "x*x_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "2" "kkge4" )"2" "xx" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "divideskkx" )"2" expand "divides" -1)"2" "2" "x" )"1" "1" assert )nil nil ))nil )"2" assert )"2" "posreal_times_posreal_is_posreal" )"2" "-x" "kk^2" )"1" assert )nil nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "kk^2 = xx" )"1" replace -1 + :dir rl)"1" "1" expand "sum_of_two_squares?" )"1" "0" "kk" )"1" assert )"1" expand "^" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "divides" -3)"2" "2" replace -3 +)"2" case "x > 1" )"1" "kk^2" )"1" assert )nil nil ))nil )"2" assert )"2" case "x = 1" )"1" replace -1)"1" assert )nil nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "-x" "kk^2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "kk" )"2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xdivsq" -1)"2" "xxlt" -4)"2" "xdivsq" "xxpos" "oldlem" "xxlt" ))"2" case "EXISTS (cc,dd,mm,nn:nat): abs(cc)<=xx/2 AND abs(dd)<=xx/2 AND pa = mm*xx+cc AND pb = nn*xx+dd" )"1" "1" case "NOT divides(xx,cc^2+dd^2)" )"1" "ccdef" -1)"1" "dddef" -2)"1" "relprime" -5)"1" "dividesab" "1" "divides_sum" )"1" "(mm * xx + cc) ^ 2 + (nn * xx + dd) ^ 2" "-(mm * xx + cc) ^ 2 - (nn * xx + dd) ^ 2+cc^2+dd^2" "xx" )"1" assert )"1" "1" "divides" )"1" expand "divides" )"1" "-(mm * mm * xx + cc * mm + (cc * mm)) - ") "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "divides" -1)"2" "yy" )"2" case "NOT rel_prime(cc,dd)" )"1" case "divides(gcd(cc,dd),xx)" )"1" expand "rel_prime" "1" case "divides(gcd(cc,dd),pa) AND divides(gcd(cc,dd),pb)" )"1" "1" "divides_gcd" )"1" "pa" "pb" "gcd(cc,dd)" )"1" assert )"1" expand "rel_prime" )"1" replace "1" expand "divides" "1" "1" assert )"1" case "x!1>1" )"1" "gcd(cc,dd)" )"1" assert )nil nil ))nil )"2" case "x!1 <=0" )"1" "nnreal_times_nnreal_is_nnreal" )"1" "-x!1" "gcd(cc,dd)" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (nnz,xxz,ccz,rrz:int): divides(rrz,xxz) AND divides(rrz,ccz) IMPLIES divides(rrz,nnz*xxz+ccz)" )"1" "nn" "xx" "dd" "gcd(cc,dd)" )"1" assert )"1" "mm" "xx" "cc" "gcd(cc,dd)" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" expand "divides" )"2" "2" replace "2" replace "2" "nnz*x!1+x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3539964928"" case "FORALL (ig:nat,ez1,pr2:int): abs(ez1)<ig AND pr2/=0 IMPLIES ez1/=ig*pr2" )"1" (label "lem1" -1)"1" (hide "lem1" )"1" (skeep)"1" "CC" "LAMBDA (x,y,z:nat): x<=p AND y<=p AND z<=p" )"1" (case "finite_sets[[nat, nat, nat]].is_finite(CC)" )"1" case "EXISTS (FF:[(fermat_prime_sos_set(p)) -> (CC)]): injective?(FF)" )"1" (skeep -1)"1" (expand "is_finite" )"1" (skosimp*)"1" (inst + "N!1" "f!1 o FF" )"1" "composition_injective[(fermat_prime_sos_set(p)),(CC),below(N!1)]" )"1" (inst - "FF" "f!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "LAMBDA (xyz:(fermat_prime_sos_set(p))): xyz" )"1" (expand "injective?" )"1" (skosimp*) nil nil )) nil )"2" (skosimp*)"2" (expand "CC" )"2" (typepred "xyz!1" )"2" (expand "fermat_prime_sos_set" )"2" case "xyz!1`1 >= 1 AND xyz!1`2 >= 1 AND xyz!1`3 >= 1" )"1" "1" "1" "xyz!1`1" )"1" "1" "xyz!1`3" )"1" "1" "xyz!1`2" )"1" assert )"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 )"2" "2" case "xyz!1`1 = 0" )"1" assert )"1" "1" "1" "p" )"1" expand "prime?" )"1" "1" "2" )"1" assert )"1" "2*xyz!1`2*xyz!1`3" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "xyz!1`2 = 0 OR xyz!1`3 = 0" )"1" case "xyz!1`2 * xyz!1`3 = 0" )"1" replace -1)"1" "1" assert )"1" "p" )"1" expand "prime?" )"1" "1" "xyz!1`1" )"1" assert )"1" "1" expand "divides" )"1" "xyz!1`1" )"1" nil nil ))nil ))nil )"2" "2" replace "2" nil nil ))nil ))nil )"3" "3" assert )"3" replace "3" case "p > 1" )"1" "p" )"1" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "is_finite" )"2" "(p+1)^3" "LAMBDA (xyz:(CC)): LET x = xyz`1, y = xyz`2, z = xyz`3 IN x*(p+1)^2 + y*(p+1) + z" )"1" (expand "injective?" )"1" (skeep)"1" (label "hyp" -1)"1" (typepred "x1" )"1" (typepred "x2" )"1" expand "CC" )"1" "1" case "x1`3=x2`3" )"1" replace -1)"1" assert )"1" case "x1`2 = x2`2" )"1" replace -1)"1" assert )"1" case "(1+p)^2 > 0" )"1" "hyp" )"1" case "x1`1 = x2`1" )"1" nil nil )"2" "2" "1/(1+p)^2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "posreal_times_posreal_is_posreal" )"2" "2" "1+p" "1+p" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "(x1`1-x2`1)*(1+p) = x2`2 - x1`2" )"1" "lem1" )"1" "1+p" "x2`2-x1`2" "x1`1-x2`1" )"1" assert )"1" expand "abs" )"1" "1"
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.740 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
