Quelle sigma_nat.prf
Sprache: Lisp
(sigma_natnil 3620720752 ("" (assuming-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 )nil integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3352138082"" (skosimp*)"" (inst-cp + 0)"" (inst + "x!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))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 )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3352138082 ("" (judgement-tcc) nil nil ) nil nil ))nil 3403006081"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3308675684"" (skosimp*) (("" (rewrite "sigma_shift_T" ) nil nil )) nil )"nonneg_int" nil )"int" integers nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma 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 ))nil ))nil 3308675684"" (skosimp*) (("" (inst + 0) (("" (assert ) nil nil )) nil )) nil )nil nil ))nil 3352138082 ("" (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 )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3403006081"" (skosimp*) (("" (assert ) nil nil )) nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3308675684"" (skosimp*)"" (lemma "sigma_shift_T2" )"" (inst?)"" (inst - "high!1" "low!1" "0 - m!1" )"" (assert )"" (prop)"1" (replace -1 :hide? t)"1" (rewrite "sigma_eq" )"1" (skosimp*) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (case "high!1<low!1" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))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 sigma nil )"int" integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3308675684"" (skosimp*)"" (lemma "sigma_shift_T2" )"" (inst?)"" (inst - "high!1" "low!1" "0-m!1" )"" (assert )"" (prop)"1" (replace -1 :hide? t)"1" (rewrite "sigma_eq" )"1" (expand "~" )"1" (assert )"1" (skosimp*)"1" (assert )"1" (lift-if) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "high!1<low!1" )"1" (expand "sigma" ) (("1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))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 sigma nil )"int" integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3410183793 ("" (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 )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3410183793 ("" (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 )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3410183793 ("" (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 )"(total_order?[real])" nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3410183811"" (skosimp*)"" (rewrite "sigma_shift_T2" )"1" (rewrite "sigma_restrict_eq" )"1" (hide 2)"1" (expand "restrict" ) (("1" (propax) nil nil )) nil )) nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil )"2" (case "low!1 <= high!1" )"1" (assert ) nil nil ) ("2" (grind) nil nil )) nil ))nil ))nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma 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 )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"[T -> real]" sigma nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"real" sigma nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3594380184 ("" (subtype-tcc) nil nil )nil nil ))nil 3594380184 ("" (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 )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3594380186"" (induct "n" )"1" (skeep)"1" (assert )"1" (rewrite "sigma_restrict_eq" )"1" (decompose-equality 1)"1" (expand "restrict" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" (induct "m" )"1" (assert ) nil nil )"2" (skolem 1 "kk" )"2" (flatten)"2" (assert )"2" (skeep)"2" (assert )"2" (inst - "F" )"2" (case "NOT 1+j <=kk" )"1" (case "NOT kk=j" )"1" (assert ) nil nil )"2" (replace -1)"2" (assert )"2" (expand "sigma" +)"2" expand "sigma" +)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "sigma" 1 1)"2" (replace -2 +)"2" (assert )"2" expand "sigma" 1 2)"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"real" reals nil )"int" integers nil )"odd_int" integersnil )"posint" nil )"nat" sigma_nat nil )"posint" nil )nil sigma nil )"[T -> real]" sigma nil )"(total_order?[real])" nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma nil )nil sigma nil )nil sigma nil )"[T, T -> boolean]" equalities nil )nil defined_types 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 )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"nonneg_int" nil ))nil 3308675684"" (skosimp*) (("" (rewrite "sigma_first" ) nil nil )) nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma 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 ))nil ))nil 3352162210"" (skosimp*) (("" (inst + 0) (("" (assert ) nil nil )) nil )) 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 )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3403006081"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3308675684"" (skosimp*) (("" (rewrite "sigma_split" ) nil nil )) nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma 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 ))nil ))nil 3481027293 ("" (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 )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil ))nil ))nil 3481027293"" case "FORALL (F: [nat -> real], k: nat, low: nat): LAMBDA (n: nat):IF n > k + 2*low THEN 0 ELSE F(2*low+k - n) ENDIF)") "1" (skeep)"1" (case "high < low" )"1" (expand "sigma" +) (("1" (assert ) nil nil )) nil )"2" (inst - "F" "high-low" "low" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (skeep)"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (skeep)"2" (skeep)"2" (inst - "F" "low" )"2" (expand "sigma" 1 1)"2" (lemma "sigma_split" )"2" "LAMBDA (n: nat): IF n > 1 + j + 2 * low THEN 0" " 1+j+low" " low" " low") "1" (assert )"1" (replace -1)"1" (hide -1)"1" (expand "sigma" + 3)"1" (expand "sigma" + 3)"1" "sigma_shift" )"1" "LAMBDA (n: nat): IF n > 1 + j + 2 * low THEN 0" "low+j" "low" "1" )"1" replace -1)"1" "1" assert )"1" replace -1)"1" "1" rewrite "sigma_restrict_eq" )"1" "1" "1" expand "restrict" )"1" nil nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )nil sigma nil )"(total_order?[real])" nil )"real" reals nil )nil sigma nil )"[T -> real]" sigma nil )nil sigma_nat nil )"nat" sigma_nat nil )"nat" sigma_nat nil )"posint" nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"int" sigma_nat nil )"nat" sigma_nat nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"nonneg_int" 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 )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (T_low type-eq-decl nil sigma nil )nil sigma nil )"real" sigma nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil 3541327761 ("" (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 )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3541327761 ("" (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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil ))nil 3541327793"" case "FORALL (F, G: [nat -> real], high1, high2: int, low1, low2,rn: nat): LAMBDA (k: nat):LAMBDA (i: nat):IF (i < k - high2 OR i > k - low2) THEN 0") "1" (skeep)"1" (case "high1 >= low1" )"1" (inst?)"1" (inst - "high1-low1" ) (("1" (assert ) nil nil )) nil ))nil )"2" (hide -)"2" (expand "sigma" + 1)"2" (assert )"2" (assert )"2" (case "FORALL (eg1:real): 0*eg1 = 0" )"1" (rewrite -1)"1" (hide -1)"1" (rewrite "sigma_restrict_eq_0" )"1" (hide 3)"1" (skosimp*)"1" (expand "sigma" )"1" (propax) nil nil )) nil ))nil ))nil )"2" (hide 3) (("2" (grind) nil nil )) nil )"3" (hide 3)"3" (flatten) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "rn" )"1" (skeep)"1" (case "high1 = low1" )"1" (replace -1)"1" (assert )"1" (expand "sigma" + 1)"1" (expand "sigma" + 2)"1" (rewrite "sigma_scal" :dir rl)"1" (expand "sigma" + 3)"1" (expand "sigma" + 3)"1" (assert )"1" (lemma "sigma_shift" )"1" "%1" _ _ _) (! 1 2 3))"1" "high2" "low2" "low1" )"1" replace -1)"1" "1" rewrite "sigma_eq" )nil nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (case "high1 >= low1 AND high2 >= low2" )"1" (flatten)"1" (inst - "F" "G" "high1-1" "high2" "low1" "low2" )"1" (assert )"1" (expand "sigma" + 1)"1" (replace -3)"1" (hide -3)"1" (expand "sigma" + 5)"1" (lemma "sigma_sum" )"1" "LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0" "LAMBDA (k: nat): LAMBDA (i: nat):IF (i < k - high2 OR i > k - low2) THEN 0" "high1+high2" "low1+low2" )"1" replace -1 :dir rl)"1" "1" case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIES a1+a2=b2+b1" )"1" "1" assert )"1" "1" "1" expand "sigma" + 3)"1" "sigma_restrict_eq_0" )"1" "1" assert )nil nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "sigma_split" )"2" "LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0" "high1+high2" "low1+low2" "high1+low2-1" )"1" assert )"1" replace -1)"1" "1" case "NOT sigma(low1 + low2, high1 - 1 + low2, LAMBDA (k: nat):IF (high1 < k - high2 OR high1 > k - low2) THEN 0") "1" "1" rewrite "sigma_restrict_eq_0" )nil nil ))nil )"2" "2" assert )"2" "sigma_shift" )"2" "LAMBDA (k: nat): IF (high1 < k - high2 OR high1 > k - low2) THEN 0" "high2" "low2" "high1" )"1" replace "1" "1" rewrite "sigma_scal" "1" rewrite "sigma_eq" )nil nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" (assert ) nil nil ))nil ))nil )"3" "3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1)"2" (ground)"2" (expand "sigma" + 2)"2" (rewrite "sigma_restrict_eq_0" )"1" (hide 3)"1" (skosimp*)"1" (rewrite "sigma_restrict_eq_0" )"1" (hide 2)"1" "1" assert )"1" "1" (ground) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (skosimp*) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil )"5" (hide 2) (("5" (skosimp*) (("5" (assert ) nil nil )) nil ))nil )"6" (hide 2) (("6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide 2) (("3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil )"4" (hide 2) (("4" (skosimp*) (("4" (assert ) nil nil )) nil )) nil )"5" (hide 2) (("5" (skosimp*) (("5" (assert ) nil nil )) nil )) nil )"6" (hide 2) (("6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil ))nil )nil sigma nil )"real" reals nil )"posint" nil )"(total_order?[real])" nil )nil sigma nil )"nat" sigma_nat nil )"int" sigma_nat nil )"int" sigma_nat nil )"posint" nil )nil integers nil )"odd_int" integers nil )nil sigma nil )nil sigma_nat nil )nil sigma nil )"nat" sigma_nat nil )"int" sigma_nat nil )"nat" sigma_nat nil )nil naturalnumbers nil )nil defined_types nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil sigma nil )"nat" sigma_nat nil )"int" sigma_nat nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"real" reals nil )"nonneg_int" 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 )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (T_low type-eq-decl nil sigma nil )nil sigma nil )"real" sigma nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" reals nil ) (> const-decl "bool" reals nil ))nil 3620720753"" (skeep) (("" (rewrite "sigma_eq" ) nil nil )) nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma nil )nil sigma 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 ))nil 3620667440 ("" (subtype-tcc) nil nil ) nil nil ))nil 3620667440 ("" (subtype-tcc) nil nil ) nil nil ))nil 3620667441"" (skeep)"" (label "ontoz" -2)"" (label "rangez" -1)"" (label "injz" -3)"" (case "NOT low<=high" )"1" (expand "sigma" +) (("1" (assert ) nil nil )) nil )"2" "FF" "LAMBDA (k:nat): (LAMBDA (i:nat): IF low<=i AND i<=low+k THEN F(i) ELSE 0 ENDIF)" )"2" case "FORALL (k:nat): low+k<=high IMPLIES sigma(low,high, FF(k)) = sigma(low,high,FF(k) o sig)" )"1" (inst - "high-low" )"1" (assert )"1" case "sigma(low, high, FF(high - low)) = sigma(low, high,F) AND sigma(low, high, FF(high - low) o sig) = sigma(low, high, F o sig)" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (split 1)"1" (rewrite "sigma_eq" 1)"1" (skosimp*)"1" (typepred "n!1" )"1" expand "FF" 1)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "sigma_eq" 1)"2" (expand "o" )"2" (skosimp*)"2" expand "FF" 1)"2" "2" "n!1" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (assert )"1" (inst -4 "low" )"1" (skosimp*)"1" (lemma "sigma_eq_one_arg" )"1" (inst?)"1" "low" )"1" assert )"1" "1" "1" "sigma_eq_one_arg" )"1" "1" "j!1" )"1" assert )"1" "1" "1" expand "o" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "o" 1)"2" expand "FF" 1)"2" "j!1" "i!1" )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "i!1" "j!1" )"3" expand "o" 1)"3" assert )"3" expand "FF" "3" "3" "i!1" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil )"3" "3" "i!1" "j!1" )"3" expand "FF" 1)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "k" )"2" (flatten)"2" "GG" "LAMBDA (i:nat): IF i=low+k+1 THEN F(i) ELSE 0 ENDIF" )"2" (assert )"2" case "NOT (FF(k+1) = (LAMBDA (d:nat): FF(k)(d) + GG(d)))" )"1" "1" expand "FF" 1)"1" expand "GG" 1)"1" assert )"1" "1" "1" "1" "1" "1" "1" "1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "HH" "LAMBDA (i:nat): IF sig(i)=(low+k+1) THEN F(sig(i)) ELSE 0 ENDIF" )"2" case "NOT ((FF(k+1) o sig) = (LAMBDA (d:nat): (FF(k) o sig)(d) + HH(d)))" )"1" "1" expand "o" 1)"1" expand "FF" 1)"1" expand "HH" 1)"1" "1" assert )"1" "1" assert )"1" "1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" rewrite "sigma_sum" :dir rl)"2" rewrite "sigma_sum" :dir rl)"2" case "sigma(low,high,GG) = sigma(low,high,HH)" )"1" "1" assert )"1" rewrite "sigma_tolambda" "1" "1" rewrite "sigma_tolambda" nil nil ))nil ))nil ))nil ))nil )"2" "2" "sigma_eq_one_arg2" )"2" "GG" "high" "low" "low+k+1" )"2" assert )"2" "1" "1" "sigma_eq_one_arg2" )"1" "ontoz" "low+k+1" )"1" "1" "HH" "high" "low" "j!1" )"1" assert )"1" "1" "1" expand "GG" "1" expand "HH" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "HH" "2" "2" "2" "i!1" "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "GG" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*) (("5" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"nonneg_int" nil )"posint" nil )"real" reals nil )"[nat -> real]" sigma_nat nil )"[nat -> real]" sigma_nat nil )nil sigma nil )nil sigma_nat nil )nil sigma nil )"posint" nil )nil sigma nil )"nat" sigma_nat nil )nil naturalnumbers nil )nil defined_types nil )"(total_order?[real])" nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" sigma_nat nil )"nat" sigma_nat nil )nil sigma nil )nil integers nil )"[nat -> [nat -> real]]" sigma_nat nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )nil sigma nil )"T3" function_props nil )"real" sigma nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props 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 naturalnumbers nil ))nil 3621161667 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3621161667 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3621161667 ("" (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 )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3621161684"" (skeep)"" (label "Gdef" -4)"" (label "ontoz" -3)"" (label "rangez" -1)"" (label "injz" -2)"" (case "NOT low1<=high1" )"1" (expand "sigma" + 1)"1" (assert )"1" (rewrite "sigma_restrict_eq_0" +)"1" (skosimp*)"1" (inst "ontoz" "i!1" )"1" (assert ) (("1" (skosimp*) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (case "NOT low2<=high2" )"1" (assert )"1" (inst - "low1" )"1" (assert ) (("1" (ground) nil nil )) nil )) nil ))nil )"2" "FF" "LAMBDA (k:nat): (LAMBDA (i:nat): IF low1<=i AND i<=low1+k THEN F(i) ELSE 0 ENDIF)" )"2" "GG" "LAMBDA (k:nat): (LAMBDA (i:nat): IF (EXISTS (j:nat): low1<=j AND j<=low1+k AND sig(j)=i) THEN G(i) ELSE 0 ENDIF)" )"2" case "FORALL (k:nat): low1+k<=high1 IMPLIES sigma(low1,high1, FF(k)) = sigma(low2,high2,GG(k))" )"1" (inst - "high1-low1" )"1" (assert )"1" case "sigma(low1, high1, FF(high1 - low1)) = sigma(low1, high1,F) AND sigma(low2, high2, GG(high1 - low1)) = sigma(low2, high2, G)" )"1" (flatten) (("1" (assert ) nil nil ))nil )"2" (split 1)"1" rewrite "sigma_eq" 1)"1" "1" expand "FF" 1)"1" (propax) nil nil ))nil ))nil ))nil )"2" rewrite "sigma_eq" 1)"2" "2" expand "GG" 1)"2" "2" "2" "ontoz" )"2" "n!1" )"2" assert )"2" "2" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2)"2" (induct "k" )"1" (assert )"1" (lemma "sigma_eq_one_arg2" )"1" "1" "low1" )"1" assert )"1" "1" "1" "sigma_eq_one_arg2" )"1" "1" "sig(low1)" )"1" assert )"1" "1" "1" expand "FF" 1)"1" expand "GG" 1)"1" "1" "1" "Gdef" )nil nil )"2" "low1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "rangez" "low1" )"2" assert )nil nil ))nil )"3" "rangez" "low1" )"3" assert )nil nil ))nil )"4" "4" expand "GG" 2)"4" "4" "4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "FF" 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "k" )"2" (assert )"2" "2" assert )"2" case "sigma(low1, high1, FF(1 + k)) = sigma(low1, high1, FF(k))+F(low1+k+1)" )"1" case "sigma(low2, high2, GG(1 + k)) = sigma(low2, high2, GG(k)) + G(sig(low1+k+1))" )"1" "Gdef" )"1" "low1+k+1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" "RD5" "LAMBDA (i:nat): IF i = sig(low1 + k + 1) THEN G(i) ELSE 0 ENDIF" )"2" case "GG(1+k) = (LAMBDA (pz:nat): GG(k)(pz) + RD5(pz))" )"1" "1" rewrite "sigma_sum" "1" "sigma_tolambda" )"1" "GG(k)" "high2" "low2" )"1" "1" "sigma_eq_one_arg2" )"1" "RD5" "high2" "low2" "sig(low1+k+1)" )"1" assert )"1" "1" expand "RD5" "1" nil nil ))nil )"2" "rangez" )"2" assert )nil nil ))nil )"3" "rangez" )"3" assert )nil nil ))nil )"4" "4" expand "RD5" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "GG" 1)"2" expand "RD5" +)"2" "2" "2" "2" "2" "2" "2" "2" assert )"2" "1" "1" "injz" )"1" "j" "1+k+low1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "j" )"2" assert )nil nil ))nil ))nil )"3" "1+k+low1" )"3" assert )nil nil ))nil )"4" "4" "j" )"4" assert )nil nil ))nil ))nil )"5" "1+k+low1" )"5" "1+k+low1" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "R2D2" "LAMBDA (i:nat): IF i = low1+k+1 THEN F(i) ELSE 0 ENDIF" )"2" case "FF(1+k) = (LAMBDA (j:nat): FF(k)(j) + R2D2(j))" )"1" replace -1)"1" "1" rewrite "sigma_sum" "1" "sigma_tolambda" )"1" "FF(k)" "high1" "low1" )"1" "1" assert )"1" "sigma_eq_one_arg2" )"1" "1" "1+k+low1" )"1" assert )"1" "1" "1" expand "R2D2" "1" nil nil ))nil ))nil )"2" "2" expand "R2D2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "FF" 1)"2" expand "R2D2" +)"2" "2" assert )"2" "2" assert )"2" "2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil ))nil )"4" (skosimp*) (("4" (assert ) nil nil ))nil )"5" (skosimp*) (("5" (assert ) nil nil ))nil )"6" (skosimp*) (("6" (assert ) nil nil ))nil )"7" (skosimp*) (("7" (assert ) nil nil ))nil )"8" (skosimp*) (("8" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals 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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )nil sigma nil )nil sigma nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil sigma nil )"real" sigma nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"nonneg_int" nil )"[bool, bool -> bool]" booleans nil )"int" integers nil )"[nat -> [nat -> real]]" sigma_nat nil )nil sigma nil )"[nat -> [nat -> real]]" sigma_nat nil )"nat" sigma_nat nil )"int" sigma_nat nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"int" sigma_nat nil )nil defined_types nil )nil naturalnumbers nil )"nat" sigma_nat nil )"nat" sigma_nat nil )nil sigma nil )"posint" nil )"[nat -> real]" sigma_nat nil )"real" reals nil )"nat" sigma_nat nil )nil sigma_nat nil )"[nat -> real]" sigma_nat nil )nil sigma nil )"posint" nil )"real" reals nil ))nil )nil 3621161674 ("" (postpone) nil nil ) nil shostak))nil 3403521637"" (skosimp*) (("" (inst + "0" ) (("" (assert ) nil nil )) nil )) 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 )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3403521650"" (skosimp*) (("" (expand "sigma" ) (("" (propax) nil nil )) nil ))nil )"real" sigma nil )) shostak))nil 3615631562 ("" (subtype-tcc) nil nil ) nil nil ))nil 3615631562 ("" (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 )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil ))nil 3615631562 ("" (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 )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"{k | abs(k) < abs(j)}" mod nil )"nat" floor_ceil nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_rat" nil ))nil ))nil 3615631614"" (induct "M" )"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (skeep)"3" (skeep)"3" (lemma "sigma_split_ge" )"3" (inst-cp -1 "F" "j" "j-1" "0" )"3" "LAMBDA (k: nat): F((k - mod(k, N)) / N) * G(mod(k, N))" "(j+1)*N-1" "j*N-1" "0" )"1" (split -2)"1" (split -2)"1" (case-replace "j+1-1=j" )"1" (hide -1)"1" (replace -2)"1" (replace -1)"1" (case-replace "j*N-1+1 = j*N" )"1" (simplify 1)"1" "1" "F" "G" "N" )"1" replace -1)"1" "1" "1" "sigma_shift_to_zero" )"1" "LAMBDA (k: nat): F((k - mod(k, N)) / N) * G(mod(k, N))" "N-1 +N*j" "j*N" )"1" "1" replace -1)"1" "N-1+N*j-j*N = N-1" )"1" "1" "sigma_eq" )"1" "LAMBDA (i: nat): " "LAMBDA (i: nat): G(i)*F(j)" "N-1" "0" )"1" "1" replace "1" "sigma_scal_right" )"1" "G" "F(j)" "N-1" "0" )"1" replace "1" "sigma_eq_arg" )"1" "F" "j" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "mod(n+j*N, N) = n" )"1" nil nil )"2" "2" expand "mod" )"2" "(j*N+n)/N = n/N + j" )"1" "floor_plus_int" )"1" "j" "n/N" )"1" replace "1" "1" "floor_0" )"1" "n/N" )"1" "1" "1" "1" replace "1" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace -1)"2" "sigma_eq_arg" )"2" "F" "0" )"2" replace -1)"2" "sigma_eq" )"2" "LAMBDA (k: nat): F((k - mod(k, N)) / N) * G(mod(k, N))" "LAMBDA (k:nat): F(0)*G(k)" "N-1" "0" )"1" "1" replace -1)"1" "sigma_scal_right" )"1" "G" "F(0)" "N-1" "0" )"1" replace -1)"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "mod(n, N) = n" )"1" nil nil )"2" "2" "2" "2" "floor(n/N)=0" )"1" nil nil )"2" "2" "2" "2" "2" "floor_0" )"2" "n/N" )"2" "2" "2" case "n/N<1" )"1" "N" )"1" "1" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil ))nil ))nil ))nil )"2" (ground) nil nil ))nil )"2" (ground) nil nil ) ("3" (ground) nil nil ))nil )"2" (ground) nil nil ) ("3" (ground) nil nil ))nil )"2" (skeep)"2" (hide-all-but 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (skeep)"4" (lemma "mod_pos" )"4" (inst -1 "k" "N" )"4" (flatten) (("4" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"5" (hide 2) (("5" (skosimp*) (("5" (grind) nil nil )) nil )) nil )"6" (skeep 1) (("6" (grind) nil nil )) nil ))nil )nil mod nil )nil sigma_nat nil )"posnat" sigma_nat nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil sigma_nat nil )nil sigma_nat nil )NOT const-decl "[bool -> bool]" booleans nil )"nonneg_int" nil )nil sigma nil )"nonneg_rat" nil )"nat" floor_ceil nil )nil sigma nil )nil sigma nil )nil integers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"(total_order?[real])" nil )nil real_types nil )"even_int" integersnil )"even_int" integersnil )nil floor_ceil nil )nil floor_ceil nil )nil integers nil )"nat" sigma_nat nil )"(total_order?[real])" nil )"posint" nil )"posint" nil )"real" reals nil )"real" reals nil )"int" integers nil )"posint" nil )"even_int" integersnil )"rat" rationals nil )"rat" rationals nil )"odd_int" integers nil )"even_int" integersnil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )nil naturalnumbers nil )"real" sigma nil )nil sigma nil )nil sigma nil )"[T, T -> boolean]" equalities nil )nil defined_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{k | abs(k) < abs(j)}" mod nil )nil integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields 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 )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"int" integers nil )"rat" rationals nil )nil application-judgement "below(m)" mod nil )"real" reals nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil ))nil 3609924876 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3609924876 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3609924876 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3609924876 ("" (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 )"real" reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"boolean" notequal nil ))nil ))nil 3609924878"" case "FORALL (m, n: nat, r: real): LAMBDA (k: nat): r ^ k) =") "1" (skeep)"1" (inst - "m-n" "n" "r" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "m" )"1" (skeep)"1" (assert )"1" (expand "sigma" )"1" (expand "sigma" )"1" (assert )"1" (expand "^" )"1" (expand "expt" + 2) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "m" )"2" (flatten)"2" (assert )"2" (skeep)"2" (inst - "n" "r" )"2" (assert )"2" (expand "sigma" +)"2" (assert )"2" "A" "sigma(n, m + n, LAMBDA (k: nat): r ^ k)" )"2" (replace -1)"2" (hide -1)"2" "+" "r ^ (1 + m + n) - (r ^ (1 + m + n)) * r" "2" replace -1)"2" "2" assert )"2" expand "^" )"2" expand "expt" + 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"real" reals nil )"real" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )"real" reals nil )"(total_order?[real])" nil )"nat" sigma_nat nil )"nat" sigma_nat nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )"nonneg_int" nil )"real" reals nil )"real" reals nil )"posint" 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 )"boolean" notequal nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (T_low type-eq-decl nil sigma nil )nil sigma nil )"real" sigma nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.105Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-06)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
