Quelle rs_integral_def.prf
Sprache: Lisp
(rs_integral_defnil 3494855846"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil rs_integral_def nil )) nil ))nil 3494855846"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil rs_integral_def nil )) nil ))nil 3489830608 ("" (subtype-tcc) nil nil ) nil nil ))nil 3489830608"" (skeep)"" (assert )"" (ground)"1" (expand "o" )"1" (expand "partjoin" )"1" (expand "o" )"1" (expand "delete" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skeep)"2" (ground)"1" (expand "o" )"1" (lift-if)"1" (assert )"1" (ground)"1" (expand "partjoin" )"1" (expand "o" )"1" (typepred "xab" )"1" (inst?) (("1" (ground) nil nil )) nil ))nil ))nil ))nil )"2" (expand "partjoin" )"2" (expand "o" )"2" (lift-if)"2" (assert )"2" (ground)"1" "Pab" )"1" "ii" )"1" "1" "xbc" )"1" "ii-xab`length" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "delete" )"2" assert )"2" "xbc" )"2" "ii-xab`length" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" expand "delete" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (typepred "ii" )"3" (expand "partjoin" -)"3" (expand "o" )"3" (expand "delete" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "o" )"2" (expand "partjoin" )"2" (expand "o" )"2" (expand "delete" )"2" (assert )"2" (lift-if)"2" (lift-if)"2" (assert )"2" (ground)"1" "xab" )"1" "ii" )"1" (ground) nil nil ))nil ))nil )"2" "xbc" )"2" "ii-xab`length" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"bool" reals nil ) (> const-decl "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_integral_def nil )"[real -> boolean]" rs_integral_def nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"posint" nil )"(total_order?[real])" nil )"fseq" fseqs "structures/" )"nonneg_int" nil )"fseq" fseqs_ops "structures/" )"partition(a, c)" rs_partition nil ))nil ))nil 3278409455"" (skosimp*)"" (assert )"" (typepred "xis!1" )"" (assert )"" (flatten) (("" (assert ) (("" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rs_integral_def nil )nil rs_integral_def nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil ))nil 3489771807"" (skeep)"" (typepred "xis" )"" (inst - "ii" )"" (flatten)"" (typepred "P" )"" (inst-cp -5 "ii" )"" (inst -5 "ii+1" ) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_integral_def nil )"[real -> boolean]" rs_integral_def nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )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 )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" nil )"posint" nil ))nil 3278175567"" (skosimp*)"" (assert ) (("" (typepred "xis!1" ) (("" (assert ) nil nil )) nil ))nil ))nil )"(total_order?[real])" nil )"int" integers nil ))nil 3278691242"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"int" integers nil ))nil 3278691242"" (skosimp*)"" (typepred "P!1" )"" (inst -6 "n!1+1" )"1" (flatten)"1" (assert )"1" (lemma "connected_domain" )"1" (expand "connected?" )"1" (inst - "a!1" "b!1" "P!1`seq(1+n!1)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_integral_def nil )"[real -> boolean]" rs_integral_def nil )nil naturalnumbers 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 )"int" integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil 3278154574"" (skosimp*)"" (lemma "connected_domain" )"" (expand "connected?" )"" (inst - "a!1" "b!1" "P!1`seq(n!1)" )"" (assert )"" (typepred "P!1" )"" (inst - "n!1" ) (("" (inst - "n!1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil rs_integral_def nil )"int" integers nil )"(total_order?[real])" nil )"bool" deriv_domain_def nil ))nil 3278154574"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil 3278324172 ("" (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]" rs_integral_def nil )nil rs_integral_def nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil 3278324172 ("" (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]" rs_integral_def nil )nil rs_integral_def nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil ))nil 3278324172 ("" (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]" rs_integral_def nil )nil rs_integral_def nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"posint" nil )nil naturalnumbers nil ))nil 3278324172 ("" (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]" rs_integral_def nil )nil rs_integral_def nil )"bool" reals nil ) (> const-decl "bool" reals nil )nil naturalnumbers nil )nil fseqs "structures/" )nil fseqs "structures/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"R" restrict nil )"bool" reals nil )"bool" sort_fseq "structures/" )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil rs_partition nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_integral_def nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"(total_order?[real])" nil )"posint" nil )nil naturalnumbers nil )nil integers nil ))nil 3280252836"" (skosimp*)"" (expand "Rie_sum" )"" (assert )"" (expand "Rie_sum_alt" )"" (expand "Rie_sec" )"" (assert )"" case "FORALL (NN: below(length(P!1)-1)): sigma[below(length(P!1) - 1)] LAMBDA (n: below(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)):IF n = 0 THEN 0") "1" (inst?)"1" (assert )"1" (replace -1)"1" (replace -1 :dir rl)"1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" "NN" 1 "below_induction[length(P!1)-1]" )"1" (assert )"1" (expand "sigma" )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1) (("2" (assert ) nil nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" rs_integral_def nil )"real" rs_integral_def nil )nil bounded_nat_inductions nil )nil defined_types nil )"partition[T](a!1, b!1)" rs_integral_defnil )"T" rs_integral_def nil )"T" rs_integral_def nil )"int" integers nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"posint" nil )"posint" nil )"real" rs_integral_def nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" reals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_integral_def nil )"[real -> boolean]" rs_integral_def nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil )nil 3280252800"" (skosimp*)"" (expand "Rie_sum" )"" (assert )"" (expand "Rie_sum_alt" )"" (expand "Rie_sec" )"" (assert )"" (assert )"" case "FORALL (NN: below(length(P!1)-1)): sigma[below(length(P!1) - 1)] LAMBDA (n: below(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)):IF n = 0 THEN 0") "1" (inst?) (("1" (assert ) nil )))"2" (hide 2)"2" "NN" 1 "below_induction[length(P!1)-1]" )"1" (assert )"1" (expand "sigma" ) (("1" (propax) nil )))))"2" (skosimp*)"2" (expand "sigma" 1)"2" (assert ) nil )))))"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil )))))"4" (skosimp*) (("4" (assert ) nil )))"5" (skosimp*)"5" (hide 3)"5" (assert )"5" (typepred "xis!1" )"5" expand "xis?" )"5" (propax) nil )))))))))))"6" (assert )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil )))))))"7" (skosimp*)"7" (assert )"7" (hide 2)"7" (typepred "xis!1" )"7" (assert ) nil )))))))))))))"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil )))))"4" (hide 2)"4" (skosimp*) (("4" (assert ) nil )))))"5" (hide 2)"5" (skosimp*)"5" (assert )"5" (typepred "xis!1" )"5" (assert ) nil )))))))))"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil )))))"7" (hide 2)"7" (skosimp*)"7" (assert )"7" (typepred "xis!1" )"7" (assert ) nil ))))))))))))))))))))))))nil )nil nil )nil 3278324183"" (skosimp*)"" (expand "Rie_sum" )"" (assert )"" (expand "Rie_sum_alt" )"" (expand "Rie_sec" )"" (assert )"" (assert )"" case "FORALL (NN: below(length(P!1)-1)): sigma[below(length(P!1) - 1)] LAMBDA (n: below(length(P!1) - 1)):LAMBDA (n: upto(length(P!1) - 1)):IF n = 0 THEN 0") "1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" "NN" 1 "below_induction[length(P!1)-1]" )"1" (assert )"1" (expand "sigma" ) (("1" (propax) nil nil ))nil ))nil )"2" (skosimp*)"2" (expand "sigma" 1)"2" (assert ) nil nil )) nil ))nil )"3" (hide 2)"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*)"5" (hide 3)"5" (assert )"5" (typepred "xis!1" )"5" expand "xis?" )"5" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (assert )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil nil ))nil ))nil ))nil )"7" (skosimp*)"7" (assert )"7" (hide 2)"7" (typepred "xis!1" )"7" (assert ) 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 )"5" (typepred "xis!1" )"5" (assert ) nil nil )) nil ))nil ))nil ))nil )"6" (hide 2)"6" (skosimp*) (("6" (assert ) nil nil )) nil ))nil )"7" (hide 2)"7" (skosimp*)"7" (assert )"7" (typepred "xis!1" )"7" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma "reals/" )) shostak))nil 3492270809"" (lemma "partition_strictly_sort" )"" (assert )"" (skeep)"" (skeep)"" (inst - "a" "b" )"" (assert ) (("" (inst - "P" ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil naturalnumbers nil )nil rs_partition 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]" rs_integral_def nil )nil rs_integral_def nil ))nil ))nil 3495206538"" (auto-rewrite + "member" )"" (skeep)"" (skeep)"" "XISfun" "(LAMBDA (xis:xis?(a,b,P)): (# length := strictly_sort(P)`length-1, seq := (LAMBDA (ii:nat): IF ii < strictly_sort(P)`length-1 THEN xis`seq(strictly_sort_map(P)(ii)) ELSE default[T] ENDIF) #))" )"1" (label "XISfunname" -1)"1" case "FORALL (xis:xis?(a,b,P)): Rie_sum(a,b,g,P,xis,f) = Rie_sum(a,b,g,strictly_sort(P),XISfun(xis),f)" )"1" (ground)"1" (skeep -)"1" (inst - "xis" )"1" (inst + "XISfun(xis)" )"1" (assert ) nil nil )"2" (assert )"2" (expand "XISfun" +)"2" (assert )"2" (typepred "strictly_sort(P)" )"2" "a" )"2" case "member(a,P)" )"1" replace -1)"1" "1" assert )"1" (skosimp*) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep -)"2" (assert )"2" case "FORALL (xiss:xis?(a,b,strictly_sort(P))): EXISTS (xis:xis?(a,b,P)): xiss = XISfun(xis)" )"1" (inst - "xis" )"1" (skolem -1 "xisp" )"1" (inst - "xisp" )"1" (inst + "xisp" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide -1)"2" (hide -1)"2" (hide 2)"2" (skeep)"2" "sig" "partition_union_map(a,b,P,P)" )"2" "signame" -1)"2" "sig" )"2" "sigtp" -1)"2" "yis" "(# length := P`length-1, seq := (LAMBDA (ii:nat): IF ii < P`length-1 THEN IF sig(ii) = strictly_sort(P)`length-1 THEN b ELSIF sig(ii) = sig(ii+1) THEN P`seq(ii) ELSE xiss`seq(sig(ii)) ENDIF ELSE default[T] ENDIF) #)" )"1" "yisname" -1)"1" "partition_union_is_strictly_sort" )"1" "a" "b" )"1" assert )"1" "P" )"1" "unionsort" "1" replace "unionsort" )"1" "xis_lem" )"1" "yis" )"1" expand "XISfun" "1" "1" "1" "1" "1" expand "yis" "1" "1" "1" "ssm" "strictly_sort_map(P)" )"1" replace "1" "ssmname" "1" "partition_union_strictly_sort_map_inv" )"1" "a" "b" )"1" assert )"1" "P" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ssm" "strictly_sort_map(P)" )"2" replace "2" "ssmname" "2" "ssm" )"2" "partition_union_strictly_sort_map_inv" )"2" "a" "b" )"2" assert )"2" "P" "x!1" )"2" assert )"2" replace "ssmname" )"2" replace "signame" )"2" replace "2" "x!1" )"2" "2" assert )"2" "sig" )"2" "1+ssm(x!1)" )"2" assert )"2" "sig" )"2" "ssm(x!1)" )"2" assert )"2" case "NOT P`seq(ssm(x!1)) = P`seq(1+ssm(x!1))" )"1" assert )nil nil )"2" "xiss" )"2" "x!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ssm" "strictly_sort_map(P)" )"3" replace "3" "ssmname" "3" "partition_union_strictly_sort_map_inv" )"3" "a" "b" )"3" assert )"3" "P" "x!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "ssm" "strictly_sort_map(P)" )"4" replace "4" "ssmname" "4" "ssm" )"4" assert )"4" "x!1" )"4" "4" assert )"4" "strictly_sort(P)" )"4" expand "strictly_increasing?" )"4" "x!1" "strictly_sort(P)`length-1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xiss`seq" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "1" "1" assert )"1" expand "yis" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" expand "yis" "1" "1" assert )"1" "1" "1" assert )"1" "xiss" )"1" "sig" )"1" "ii" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "xiss" )"2" "sig(ii)" )"2" "2" "sig" )"2" "ii" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "yis" "2" "2" assert )"2" "1" "sig" )"1" "ii" )"1" "P" )"1" "ii+1" )"1" "1" expand "increasing?" )"1" "ii" "1+ii" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P" )"2" expand "increasing?" )"2" "ii" "1+ii" )"2" assert )nil nil ))nil ))nil ))nil )"3" "xiss" )"3" "sig(ii)" )"3" "3" case "1+sig(ii) <= sig(1+ii)" )"1" assert )"1" "strictly_sort(P)" )"1" expand "strictly_increasing?" )"1" "1+sig(ii)" "sig(1+ii)" )"1" assert )"1" "sig" )"1" "1+ii" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sig" )"2" "ii" )"2" "ii+1" )"2" assert )"2" "strictly_sort(P)" )"2" expand "strictly_increasing?" )"2" "sig(1+ii)" "sig(ii)" )"2" assert )"2" "2" "P" )"2" expand "increasing?" )"2" "ii" "1+ii" )"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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide ("xispred" "XISfunname" ))"2" (hide 2)"2" (skeep)"2" (expand "XISfun" )"2" "yis" "(# length := strictly_sort(P)`length-1, seq := (LAMBDA (ii:nat): IF ii < strictly_sort(P)`length-1 THEN xis`seq(strictly_sort_map(P)(ii)) ELSE default[T] ENDIF) #)" )"1" (replace -1)"1" (hide -1)"1" (expand "Rie_sum" )"1" "ssp" "strictly_sort(P)" )"1" "sspname" -1)"1" replace "sspname" )"1" "sig" "strictly_sort_map(P)" )"1" "signame" -1)"1" case "FORALL (mm:below(ssp`length-1)): sigma[below(strictly_sort(P)`length - 1)] LAMBDA (n: below(strictly_sort(P)`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "ssp`length-2" )"1" replace -1)"1" "1" "sigma_split[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "P`length-2" "0" "sig(ssp`length - 2)" )"1" assert )"1" case "sig(ssp`length-2) <= P`length-2" )"1" assert )"1" replace "1" case "sigma(1 + sig(ssp`length - 2), P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i" )"2" case "g(P`seq(1+i)) = g(P`seq(i))" )"1" assert )nil nil )"2" "2" "sig" )"2" "2" "ssp`length-2" )"1" assert )"1" "1" "jj" "ssp`length-2" )"1" replace "1" case "ssp`length-1 = jj+1" )"1" replace "1" case "P`seq(1+i) = P`seq(i)" )"1" assert )nil nil )"2" "2" "strictly_sort_map_between" )"2" "P" )"2" replace "sspname" )"2" replace "signame" )"2" assert )"2" "jj" )"1" "i" )"1" assert )"1" case "P`seq(sig(1+jj)) = P`seq(1+i)" )"1" assert )"1" case "1+sig(jj) <= sig(jj+1)" )"1" case "sig(jj+1) = P`length-1" )"1" assert )nil nil )"2" replace "2" "sig" )"2" assert )"2" case "NOT P`length = 0" )"1" "fseq_length_zero" )"1" "ssp" )"1" assert )"1" "ssp" )"1" "P`seq(0)" )"1" case "member(P`seq(0),P)" )"1" replace "1" "1" assert )"1" nil nil ))nil ))nil ))nil )"2" expand "member" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "fseq_length_zero" )"3" "ssp" )"3" assert )"3" "ssp" )"3" "P`seq(0)" )"3" case "member(P`seq(0),P)" )"1" replace "1" assert )"1" nil nil ))nil ))nil )"2" expand "member" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "strictly_sort_map_increasing" )"2" "P" )"2" assert )"2" "jj" "1+jj" )"1" assert )nil nil )"2" assert )"2" "fseq_length_zero" )"2" "ssp" )"2" assert )"2" "ssp" )"2" "P`seq(0)" )"2" case "member(P`seq(0),P)" )"1" replace "1" assert )"1" nil nil ))nil ))nil )"2" expand "member" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "partition_strictly_sort" )"4" "a" "b" )"4" assert )"4" "P" )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "strictly_sort_map_between" )"2" "P" )"2" replace "2" assert )"2" replace "2" "sig" )"2" assert )"2" "1" "1" replace "sspname" )"1" replace "1" assert )"1" "jj" )"1" "1+i" )"1" assert )nil nil ))nil )"2" assert )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sig" )"2" assert )"2" case "strictly_sort(P)`length >= 1" )"1" assert )"1" replace "sspname" )"1" "ssp`length-2" )"1" "ssp`length-1" )"1" "1" assert )"1" case "NOT sig(ssp`length-2) = P`length-1" )"1" assert )nil nil )"2" replace "2" "ssp" )"2" expand "strictly_increasing?" )"2" "ssp`length-2" "ssp`length-1" )"1" assert )nil nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"1" "P" )"1" assert )nil nil ))nil )"2" "partition_strictly_sort" )"2" expand "ssp" )"2" "strictly_sort(P)" )"2" "a" )"2" "b" )"2" case "member(b,P) and member(a,P)" )"1" "1" replace "1" replace "1" "1" "1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "P`length-1" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "altb" -3)"2" "mm" )"1" "1" expand "sigma" )"1" expand "sigma" "1" assert )"1" "1" assert )"1" case "sigma(0, sig(0) - 1, LAMBDA (n: below(P`length - 1)):") "1" replace "1" assert )"1" "sig" )"1" "0" )"1" "1" assert )"1" replace "sspname" )"1" replace "1" replace "1" expand "yis" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i" )"2" case "P`seq(1+i) = P`seq(i)" )"1" assert )nil nil )"2" "2" "sig" )"2" "0" )"2" "2" "2" assert )"2" "2" case "P`seq(sig(0)) = a" )"1" "P" )"1" "1" case "P`seq(i) = a AND P`seq(1+i) = a" )"1" "1" assert )nil nil ))nil )"2" "2" "1" expand "increasing?" "1" "0" "i" )"1" "i" "sig(0)" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "increasing?" "2" "0" "1+i" )"2" "1+i" "sig(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"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 )"2" "mm" )"2" assert )"1" "1" expand "sigma" "1" replace -2)"1" "strictly_sort_map_increasing" )"1" expand "sigma" "1" "1" "1" expand "yis" "1" assert )"1" replace "signame" )"1" case "f(xis`seq(sig(1 + mm))) * g(ssp`seq(2 + mm)) )))AND sigma[below(P`length - 1)]LAMBDA (n: below(P`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "1" assert )nil nil ))nil )"2" "2" "1" "sig" )"1" "1+mm" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "sigma_split[below(P`length-1)]" )"2" "(LAMBDA (n: below(P`length - 1)): " "sig(1+mm)-1" "0" "sig(mm)" )"2" assert )"2" "1" replace "1" "1" case "sigma(1 + sig(mm), sig(1 + mm) - 1, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "2" "2" "i" )"2" case "P`seq(i) = P`seq(1+i)" )"1" assert )nil nil )"2" "2" "strictly_sort_map_between" )"2" "P" )"2" assert )"2" replace "signame" )"2" "mm" )"2" "i" )"2" "1+i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P" )"2" assert )"2" "mm" "1+mm" )"2" assert )nil nil ))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" case "ssp`length >= 2" )"1" assert )nil nil )"2" "2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" case "mm < 0" )"1" assert )nil nil )"2" assert )"2" "sig(mm)" )"2" assert )"2" case "NOT sig(mm) = P`length-1" )"1" assert )nil nil )"2" "sig" )"2" "mm" )"2" replace "sspname" )"2" assert )"2" "2" "sig" )"2" "2" "ssp`length-1" )"2" "2" assert )"2" "ssp" )"2" expand "strictly_increasing?" )"2" "mm" "ssp`length-1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "partition_strictly_sort" )"7" "a" "b" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" case "mm < 0" )"1" (assert ) nil nil )"2" assert )"2" "sig(mm)" )"2" assert )"2" case "NOT sig(mm) = P`length-1" )"1" assert )nil nil )"2" "sig" )"2" "mm" )"2" replace "2" assert )"2" "2" "sig" )"2" "2" "ssp`length-1" )"2" "2" assert )"2" "ssp" )"2" expand "strictly_increasing?" )"2" "mm" "ssp`length-1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (hide -2) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1)"3" (skeep)"3" (assert )"3" (hide 2)"3" (split +)"1" (skeep)"1" (expand "XISfun" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (expand "XISfun" )"2" (lemma "partition_strictly_sort" )"2" (inst - "a" "b" )"2" assert )"2" "P" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "XISfun" )"3" (propax) nil nil )) nil )"4" (skeep)"4" (expand "XISfun" )"4" (name "sig" "strictly_sort_map(P)" )"4" replace -1)"4" "ii" )"4" "sig" )"4" "ii" )"4" "4" assert )"4" "xis" )"4" "sig(ii)" )"1" "1" assert )nil nil ))nil )"2" case "sig(ii) = P`length-1" )"1" assert )"1" replace -1)"1" "strictly_sort_map_increasing" )"1" "P" )"1" assert )"1" "ii" "strictly_sort(P)`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (lemma "partition_strictly_sort" )"4" (inst - "a" "b" )"4" (assert ) (("4" (inst - "P" ) nil nil )) nil ))nil ))nil ))nil ))nil )"5" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (lemma "partition_strictly_sort" )"2" (inst - "a" "b" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" fseqs "structures/" )"{sq: [below(strictly_sort(s)`length) -> below(s`length)] | LET sss = strictly_sort(s) INAND sss`length >= 1 IMPLIESAND AND AND ii < sss`length - 1 IMPLIES" sort_fseq "structures/" )"[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"{ss: fseq | AND " sort_fseq "structures/" )"bool" fseqs "structures/" )"[bool, bool -> bool]" booleans nil )"bool" sort_fseq "structures/" )nil rs_integral_def nil )"[numfield, numfield -> numfield]" number_fields nil )nil rs_partition nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" sort_fseq "structures/" )"bool" reals nil )"R" restrict nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil fseqs "structures/" )nil fseqs "structures/" )nil rs_integral_def nil )"[real -> boolean]" rs_integral_def nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"int" integers nil )"(reflexive?[S])" nil )"(antisymmetric?[S])" nil )"(transitive?[S])" nil )"(preorder?[S])" nil )"(partial_order?[S])" nil )"(dichotomous?[S])" nil )"(total_order?[S])" nil )"real" rs_integral_def nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil nil )"posint" nil )"[# length: int, seq: [nat -> T] #]" nil )nil rs_partitionnil )"posint" nil )"{pm: [below(P`length) -> below(partition_union(a, b)(P, Q)`length)] | " nil )"{PQ: partition(a, b) | OR member(x, Q)))AND strictly_increasing?(PQ)}" rs_partition nil) OR const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"T" rs_integral_def nil )"T" rs_integral_def nil )"partition[T](a, b)" rs_integral_def nil )"[xis?(a, b, P) -> [# length: int, seq: [nat -> T] #]]" nil )"xis?(a, b, P)" rs_integral_def nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )nil sigma_below "reals/" )nil sigma "reals/" )"odd_int" integersnil )nil integers nil )nil sort_fseq"structures/" )nil fseqs "structures/" )"fseq[T]" rs_integral_def nil )nil rs_partition nil )nil sort_fseq"structures/" )"int" rs_integral_def nil )"int" integers nil )nil sigma "reals/" )"{ss: fseq[T] | AND " nil )"[# length: int, seq: [nat -> T] #]" nil )"odd_int" integers nil )"real" reals nil )nil bounded_nat_inductions nil )nil defined_types nil )"{sq: [below(strictly_sort(P)`length) -> below(P`length)] | AND AND " nil )"{sq: [below(strictly_sort(P)`length) -> below(P`length)] | AND AND " nil )"below(strictly_sort(P)`length - 1)" nil ))nil )nil 3492270772"" (skeep)"" (skeep)"" "XISfun" "(LAMBDA (xis:xis?(a,b,P)): (# length := strictly_sort(P)`length-1, seq := (LAMBDA (ii:nat): IF ii < strictly_sort(P)`length-1 THEN xis`seq(strictly_sort_map(P)(ii)) ELSE default[T] ENDIF) #))" )"1" (label "XISfunname" -1)"1" case "FORALL (xis:xis?(a,b,P)): Rie_sum(a,b,g,P,xis,f) = Rie_sum(a,b,g,strictly_sort(P),XISfun(xis),f)" )"1" (ground)"1" (skeep -)"1" (inst - "xis" )"1" (inst + "XISfun(xis)" )"1" (assert ) nil nil )"2" (assert )"2" (expand "XISfun" +)"2" (assert )"2" (typepred "strictly_sort(P)" )"2" (inst - "a" )"2" case "member(a,P)" )"1" replace -1)"1" "1" assert )"1" (skosimp*) nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skeep -)"2" (assert )"2" case "FORALL (xiss:xis?(a,b,strictly_sort(P))): EXISTS (xis:xis?(a,b,P)): xiss = XISfun(xis)" )"1" (inst - "xis" )"1" (skolem -1 "xisp" )"1" (inst - "xisp" )"1" (inst + "xisp" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide -1)"2" (hide -1)"2" (hide 2)"2" (skeep)"2" "sig" "partition_union_map(a,b,P,P)" )"2" "signame" -1)"2" "sig" )"2" "sigtp" -1)"2" "yis" "(# length := P`length-1, seq := (LAMBDA (ii:nat): IF ii < P`length-1 THEN IF sig(ii) = strictly_sort(P)`length-1 THEN b ELSIF sig(ii) = sig(ii+1) THEN P`seq(ii) ELSE xiss`seq(sig(ii)) ENDIF ELSE default[T] ENDIF) #)" )"1" "yisname" -1)"1" "partition_union_is_strictly_sort" )"1" "a" "b" )"1" assert )"1" "P" )"1" "unionsort" "1" replace "unionsort" )"1" "xis_lem" )"1" "yis" )"1" expand "XISfun" "1" "1" "1" "1" "1" expand "yis" "1" "1" "1" "ssm" "strictly_sort_map(P)" )"1" replace "1" "ssmname" "1" "partition_union_strictly_sort_map_inv" )"1" "a" "b" )"1" assert )"1" "P" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ssm" "strictly_sort_map(P)" )"2" replace "2" "ssmname" "2" "ssm" )"2" "partition_union_strictly_sort_map_inv" )"2" "a" "b" )"2" assert )"2" "P" "x!1" )"2" assert )"2" replace "ssmname" )"2" replace "signame" )"2" replace "2" "x!1" )"2" "2" assert )"2" "sig" )"2" "1+ssm(x!1)" )"2" assert )"2" "sig" )"2" "ssm(x!1)" )"2" assert )"2" case "NOT P`seq(ssm(x!1)) = P`seq(1+ssm(x!1))" )"1" assert )nil nil )"2" "xiss" )"2" "x!1" )"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 ))nil ))nil ))nil ))nil ))nil ))nil )"3" "ssm" "strictly_sort_map(P)" )"3" replace "3" "ssmname" "3" "partition_union_strictly_sort_map_inv" )"3" "a" "b" )"3" assert )"3" "P" "x!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "ssm" "strictly_sort_map(P)" )"4" replace "4" "ssmname" "4" "ssm" )"4" assert )"4" "x!1" )"4" "4" assert )"4" "strictly_sort(P)" )"4" expand "strictly_increasing?" )"4" "x!1" "strictly_sort(P)`length-1" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "xiss`seq" )"2" "x!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil )"2" "1" "1" assert )"1" expand "yis" "1" nil nil ))nil ))nil ))nil )"2" "2" "1" expand "yis" "1" "1" assert )"1" "1" "1" assert )"1" "xiss" )"1" "sig" )"1" "ii" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "xiss" )"2" "sig(ii)" )"2" "2" "sig" )"2" "ii" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "yis" "2" "2" assert )"2" "1" "sig" )"1" "ii" )"1" "P" )"1" "ii+1" )"1" "1" expand "increasing?" )"1" "ii" "1+ii" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P" )"2" expand "increasing?" )"2" "ii" "1+ii" )"2" assert )nil nil ))nil ))nil ))nil )"3" "xiss" )"3" "sig(ii)" )"3" "3" case "1+sig(ii) <= sig(1+ii)" )"1" assert )"1" "strictly_sort(P)" )"1" expand "strictly_increasing?" )"1" "1+sig(ii)" "sig(1+ii)" )"1" assert )"1" "sig" )"1" "1+ii" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "sig" )"2" "ii" )"2" "ii+1" )"2" assert )"2" "strictly_sort(P)" )"2" expand "strictly_increasing?" )"2" "sig(1+ii)" "sig(ii)" )"2" assert )"2" "2" "P" )"2" expand "increasing?" )"2" "ii" "1+ii" )"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 ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide ("xispred" "XISfunname" ))"2" (hide 2)"2" (skeep)"2" (expand "XISfun" )"2" "yis" "(# length := strictly_sort(P)`length-1, seq := (LAMBDA (ii:nat): IF ii < strictly_sort(P)`length-1 THEN xis`seq(strictly_sort_map(P)(ii)) ELSE default[T] ENDIF) #)" )"1" (replace -1)"1" (hide -1)"1" (expand "Rie_sum" )"1" (name "ssp" "strictly_sort(P)" )"1" "sspname" -1)"1" replace "sspname" )"1" "sig" "strictly_sort_map(P)" )"1" "signame" -1)"1" case "FORALL (mm:below(ssp`length-1)): sigma[below(strictly_sort(P)`length - 1)] LAMBDA (n: below(strictly_sort(P)`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "ssp`length-2" )"1" replace -1)"1" "1" "sigma_split[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "P`length-2" "0" "sig(ssp`length - 2)" )"1" assert )"1" case "sig(ssp`length-2) <= P`length-2" )"1" assert )"1" replace -2)"1" case "sigma(1 + sig(ssp`length - 2), P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i" )"2" case "g(P`seq(1+i)) = g(P`seq(i))" )"1" assert )nil nil )"2" "2" "sig" )"2" "2" "ssp`length-2" )"1" assert )"1" "1" "jj" "ssp`length-2" )"1" replace "1" case "ssp`length-1 = jj+1" )"1" replace "1" case "P`seq(1+i) = P`seq(i)" )"1" assert )nil nil )"2" "2" "strictly_sort_map_between" )"2" "P" )"2" replace "sspname" )"2" replace "signame" )"2" assert )"2" "jj" )"1" "i" )"1" assert )"1" case "P`seq(sig(1+jj)) = P`seq(1+i)" )"1" assert )"1" case "1+sig(jj) <= sig(jj+1)" )"1" case "sig(jj+1) = P`length-1" )"1" assert )nil nil )"2" replace "2" "sig" )"2" assert )"2" case "NOT P`length = 0" )"1" "fseq_length_zero" )"1" "ssp" )"1" assert )"1" "ssp" )"1" "P`seq(0)" )"1" case "member(P`seq(0),P)" )"1" replace "1" "1" assert )"1" nil nil ))nil ))nil ))nil )"2" expand "member" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "fseq_length_zero" )"3" "ssp" )"3" assert )"3" "ssp" )"3" "P`seq(0)" )"3" case "member(P`seq(0),P)" )"1" replace "1" assert )"1" nil nil ))nil ))nil )"2" expand "member" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "strictly_sort_map_increasing" )"2" "P" )"2" assert )"2" "jj" "1+jj" )"1" assert )nil nil )"2" assert )"2" "fseq_length_zero" )"2" "ssp" )"2" assert )"2" "ssp" )"2" "P`seq(0)" )"2" case "member(P`seq(0),P)" )"1" replace "1" assert )"1" nil nil ))nil ))nil )"2" expand "member" )"2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "partition_strictly_sort" )"4" "a" "b" )"4" assert )"4" "P" )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "strictly_sort_map_between" )"2" "P" )"2" replace "2" assert )"2" replace "2" "sig" )"2" assert )"2" "1" "1" replace "sspname" )"1" replace "1" assert )"1" "jj" )"1" "1+i" )"1" assert )nil nil ))nil )"2" assert )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sig" )"2" assert )"2" case "strictly_sort(P)`length >= 1" )"1" assert )"1" replace "sspname" )"1" "ssp`length-2" )"1" "ssp`length-1" )"1" "1" assert )"1" case "NOT sig(ssp`length-2) = P`length-1" )"1" assert )nil nil )"2" replace "2" "ssp" )"2" expand "strictly_increasing?" )"2" "ssp`length-2" "ssp`length-1" )"1" assert )nil nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "partition_strictly_sort" )"3" "a" "b" )"3" assert )"3" "P" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"1" "P" )"1" assert )nil nil ))nil )"2" "partition_strictly_sort" )"2" expand "ssp" )"2" "strictly_sort(P)" )"2" "a" )"2" "b" )"2" case "member(b,P) and member(a,P)" )"1" "1" replace "1" replace "1" "1" "1" expand "member" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "P`length-1" )"1" assert )nil nil ))nil )"2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "altb" -3)"2" "mm" )"1" "1" expand "sigma" )"1" expand "sigma" "1" assert )"1" "1" assert )"1" case "sigma(0, sig(0) - 1, LAMBDA (n: below(P`length - 1)):") "1" replace "1" assert )"1" "sig" )"1" "0" )"1" "1" assert )"1" replace "sspname" )"1" replace "1" replace "1" expand "yis" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i" )"2" case "P`seq(1+i) = P`seq(i)" )"1" assert )nil nil )"2" "2" "sig" )"2" "0" )"2" "2" "2" assert )"2" "2" case "P`seq(sig(0)) = a" )"1" "P" )"1" "1" case "P`seq(i) = a AND P`seq(1+i) = a" )"1" "1" assert )nil nil ))nil )"2" "2" "1" expand "increasing?" "1" "0" "i" )"1" "i" "sig(0)" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "increasing?" "2" "0" "1+i" )"2" "1+i" "sig(0)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )"2" "P" )"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 )"2" "mm" )"2" assert )"1" "1" expand "sigma" "1" replace -2)"1" "strictly_sort_map_increasing" )"1" expand "sigma" "1" "1" "1" expand "yis" "1" assert )"1" replace "signame" )"1" case "f(xis`seq(sig(1 + mm))) * g(ssp`seq(2 + mm)) )))AND sigma[below(P`length - 1)]LAMBDA (n: below(P`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "1" assert )nil nil ))nil )"2" "2" "1" "sig" )"1" "1+mm" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "sigma_split[below(P`length-1)]" )"2" "(LAMBDA (n: below(P`length - 1)): " "sig(1+mm)-1" "0" "sig(mm)" )"2" assert )"2" "1" replace "1" "1" case "sigma(1 + sig(mm), sig(1 + mm) - 1, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "2" "2" "i" )"2" case "P`seq(i) = P`seq(1+i)" )"1" assert )nil nil )"2" "2" "strictly_sort_map_between" )"2" "P" )"2" assert )"2" replace "signame" )"2" "mm" )"2" "i" )"2" "1+i" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "P" )"2" assert )"2" "mm" "1+mm" )"2" assert )nil nil ))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" case "ssp`length >= 2" )"1" assert )nil nil )"2" "2" "partition_strictly_sort" )"2" "a" "b" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" case "mm < 0" )"1" assert )nil nil )"2" assert )"2" "sig(mm)" )"2" assert )"2" case "NOT sig(mm) = P`length-1" )"1" assert )nil nil )"2" "sig" )"2" "mm" )"2" replace "sspname" )"2" assert )"2" "2" "sig" )"2" "2" "ssp`length-1" )"2" "2" assert )"2" "ssp" )"2" expand "strictly_increasing?" )"2" "mm" "ssp`length-1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" assert )nil nil ))nil )"5" "5" assert )nil nil ))nil )"6" "6" assert )nil nil ))nil )"7" "partition_strictly_sort" )"7" "a" "b" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" case "mm < 0" )"1" (assert ) nil nil )"2" assert )"2" "sig(mm)" )"2" assert )"2" case "NOT sig(mm) = P`length-1" )"1" assert )nil nil )"2" "sig" )"2" "mm" )"2" replace "2" assert )"2" "2" "sig" )"2" "2" "ssp`length-1" )"2" "2" assert )"2" "ssp" )"2" expand "strictly_increasing?" )"2" "mm" "ssp`length-1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" (assert ) nil nil ))nil )"5" "5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (skeep)"2" (hide -2) (("2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide -1)"3" (skeep)"3" (assert )"3" (hide 2)"3" (split +)"1" (skeep)"1" (expand "XISfun" )"1" (lift-if) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (assert )"2" (expand "XISfun" )"2" (propax) nil nil )) nil ))nil )"3" (expand "XISfun" ) (("3" (propax) nil nil ))nil )"4" (expand "XISfun" ) (("4" (propax) nil nil ))nil )"5" (expand "XISfun" )"5" (lemma "partition_strictly_sort" )"5" (inst - "a" "b" )"5" (assert )"5" "P" )"5" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"6" (expand "XISfun" ) (("6" (propax) nil nil ))nil )"7" (skeep)"7" (expand "XISfun" )"7" (name "sig" "strictly_sort_map(P)" )"7" (replace -1)"7" "ii" )"7" "sig" )"7" "ii" )"7" "7" assert )"7" "xis" )"7" "sig(ii)" )"1" "1" (assert ) nil nil ))nil )"2" case "sig(ii) = P`length-1" )"1" assert )"1" replace -1)"1" "strictly_sort_map_increasing" )"1" "P" )"1" assert )"1" "ii" "strictly_sort(P)`length-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (lemma "partition_strictly_sort" )"4" (inst - "a" "b" )"4" (assert ) (("4" (inst - "P" ) nil nil )) nil ))nil ))nil ))nil ))nil )"5" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (skeep)"2" (lemma "partition_strictly_sort" )"2" (inst - "a" "b" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma "reals/" )nil sort_fseq"structures/" )nil fseqs "structures/" )nil sort_fseq"structures/" )nil sigma "reals/" )nil sigma_below "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil fseqs "structures/" )nil fseqs "structures/" )"bool" sort_fseq "structures/" )"bool" sort_fseq "structures/" )"bool" fseqs "structures/" )"{ss: fseq | AND " sort_fseq "structures/" )"{sq: [below(strictly_sort(s)`length) -> below(s`length)] | LET sss = strictly_sort(s) INAND sss`length >= 1 IMPLIESAND AND AND ii < sss`length - 1 IMPLIES" sort_fseq "structures/" )"T" fseqs "structures/" ))nil )nil 3491668925"" (skeep)"" (skeep)"" (typepred "RS" )"" (label "altb" -2)"" (expand "Riemann_sum?" )"" (skeep -1)"" "yis" "(# length := strictly_sort(P)`length-1, seq := (LAMBDA (ii:nat): IF ii < strictly_sort(P)`length-1 THEN xis`seq(strictly_sort_map(P)(ii)) ELSE default[real] ENDIF) #)" )"1" (inst + "yis" )"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" (expand "Rie_sum" )"1" (name "ssp" "strictly_sort(P)" )"1" (label "sspname" -1)"1" replace "sspname" )"1" "sig" "strictly_sort_map(P)" )"1" "signame" -1)"1" case "FORALL (mm:below(ssp`length-1)): sigma[below(strictly_sort(P)`length - 1)] LAMBDA (n: below(strictly_sort(P)`length - 1)):LAMBDA (n: below(P`length - 1)):") "1" "ssp`length-2" )"1" replace -1)"1" "1" "sigma_split[below(P`length-1)]" )"1" "LAMBDA (n: below(P`length - 1)): " "P`length-2" "0" "sig(ssp`length - 2)" )"1" assert )"1" case "sig(ssp`length-2) <= P`length-2" )"1" assert )"1" replace -2)"1" case "sigma(1 + sig(ssp`length - 2), P`length - 2, LAMBDA (n: below(P`length - 1)):") "1" assert )nil nil )"2" "2" "2" rewrite "sigma_restrict_eq_0" )"2" "2" "2" "i" )"2" case "g(P`seq(1+i)) = g(P`seq(i))" )"1" assert )nil nil )"2" "2" "sig" )"2" "2" "ssp`length-2" )"1" assert )"1" "1" "jj" "ssp`length-2" )"1" replace "1" case "ssp`length-1 = jj+1" )"1" replace "1" case "P`seq(1+i) = P`seq(i)" )"1" assert )nil nil )"2" "2" "strictly_sort_map_between" )"2" "P" )"2" replace "sspname" )"2" replace "signame" )"2" assert )"2" "jj" )"1" "i" )"1" assert )"1" case "P`seq(sig(1+jj)) = P`seq(1+i)" )"1" assert )"1" case "1+sig(jj) <= sig(jj+1)" )"1" case "sig(jj+1) = P`length-1" )"1" assert )nil nil )"2" replace "2" "sig" )"2" assert )"2" case "NOT P`length = 0" )"1" "fseq_length_zero" )"1"
Messung V0.5 in Prozent C=100 H=99 G=99
¤ Dauer der Verarbeitung: 0.660 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
