SSL multi_bernstein.prf
Interaktion und
(multi_bernstein0 1 nil 3618684915 "" (assuming-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )nil integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))0 1 nil 3498406967 ("" (subtype-tcc) nil nil ) nil nil ))0 1 nil 3498406967 ("" (subtype-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))0 1 nil 3509275056 ("" (subtype-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))0 1 nil 3498990086 ("" (subtype-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))0 1 nil 3498990086 ("" (subtype-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))0 1 nil 3498990086 ("" (subtype-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))0 1 nil 3498990086 "" (termination-tcc) nil nil ) nil nil ))0 1 nil 3499083500 "" (expand "multibs_eval" )"" (expand "sigma" )"" (expand "sigma" )"" case "FORALL (X: Vars, bsdegmono: DegreeMono, bspoly: MultiBernstein, 0 ) * bsproduct_eval(bspoly(0 ), bsdegmono, mvars+1 )(X) =1 , 1 , mvars+1 )LAMBDA (i: nat): 0 )(X)") "1" (skeep) (("1" (inst?) (("1" (assert ) nil nil )) nil ))nil )"2" (hide 2 )"2" (induct "mvars" )"1" (skeep)"1" (assert )"1" (expand "bsproduct_eval" )"1" (expand "product" )"1" (expand "product" )"1" (expand "multibs_eval_rec" )"1" (rewrite "sigma_scal" :dir rl)"1" (rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" if )"1" "1" 3 )"1" expand "multibs_eval_rec" )"1" expand "product" )"1" expand "product" )"1" expand "multibs_eval_mono" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "product" )"1" expand "product" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "vv" )"2" (flatten)"2" (skeep)"2" (assert )"2" (expand "bsproduct_eval" +)"2" (expand "product" + 1 )"2" (lemma "sigma_scal" )"2" "LAMBDA (j: nat): IF j > bsdegmono(1 + vv) THEN 0 0 )(1 + vv)(j) *1 + vv))(X(1 + vv))" " cf(0 ) *0 , vv,LAMBDA (i: nat):0 , bsdegmono(i),LAMBDA (j: nat):IF j > bsdegmono(i) THEN 0 0 )(i)(j) *" "bsdegmono(1+vv)" "0" )"1" assert )"1" replace -1 :dir rl)"1" 1 )"1" expand "multibs_eval_rec" +)"1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" if )"1" "1" 3 )"1" expand "bsproduct_eval" )"1" "1" "cf" )"1" 1 "bspoly(0)(1 + vv)(x!1) * Bern(x!1, bsdegmono(1 + vv))(X(1 + vv))" )"1" replace 1 )"1" 1 )"1" case "FORALL (rr:nat,cgm:CoeffMono): rr<=vv IMPLIES multibs_eval_rec(bspoly, bsdegmono, cf, 1 + vv, 1, 1 + rr) 0 )(1 + vv)(x!1 ) * Bern(x!1 , bsdegmono(1 + vv))(X(1 + vv)))2 + vv, 1 , 1 + rr)1 + vv) := x!1 ])(X)") "1" "1" assert )nil nil ))nil )"2" 3 )"2" "rr" )"1" "1" expand "multibs_eval_rec" )"1" 1 )"1" "sigma_scal" )"1" "(LAMBDA (d: nat): 1 + vv, 1 , 0 )0 ) := d])(X))" "(bspoly(0)(1 + vv)(x!1) * Bern(x!1, bsdegmono(1 + vv))(X(1 + vv)))" "bsdegmono(0)" "0" )"1" replace 1 "1" 1 )"1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" if )"1" "1" 3 )"1" expand "multibs_eval_rec" )"1" expand "multibs_eval_mono" )"1" expand "sigma" )"1" expand "sigma" )"1" expand "product" 3 )"1" expand "product" 3 )"1" case "NOT product(0, vv, LAMBDA (k: nat):IF cgm WITH [(0 ) := x!2 ](k) <= bsdegmono(k)0 ) := x!2 ](k), bsdegmono(k))(X(k))1 0 , vv,LAMBDA (k: nat):IF cgm WITH [(1 + vv) := x!1 , (0 ) := x!2 ](k) <=1 + vv) := x!1 , (0 ) := x!2 ](k),1 ") "1" 3 )"1" rewrite "product_restrict_eq" )"1" 2 )"1" "1" expand "restrict" )"1" if )"1" nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1 "2" 1 )"2" case "product(0, vv, LAMBDA (j: nat): bspoly(0 )(j)(cgm WITH [(0 ) := x!2 ](j)))=product(0 , vv,LAMBDA (j: nat):0 )(j)(cgm WITH [(1 + vv) := x!1 , (0 ) := x!2 ](j)))") "1" assert )nil nil )"2" 3 )"2" rewrite "product_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 "rr" )"2" "2" "2" assert )"2" expand "multibs_eval_rec" "2" "sigma_scal" )"2" "2" "(bspoly(0)(1 + vv)(x!1) * Bern(x!1, bsdegmono(1 + vv))(X(1 + vv)))" )"2" replace 1 "2" 1 )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" "cgm WITH [(1 + rr) := x!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 )"2" "2" assert )nil nil ))nil )"3" "3" assert )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 ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) 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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" sigma "reals/" )"real" multi_bernstein nil )eq -decl nil util nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_bernstein nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )"[T, T -> boolean]" equalities nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 )"posint" nil )"(total_order?[real])" nil )"RealOrder" util nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )eq -decl nil defined_types nil )nil naturalnumbers nil )"odd_int" integers nil )"real" product "reals/" )nil sigma "reals/" )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" multi_bernstein nil )"[T -> real]" sigma "reals/" )"DegreeMono" multi_bernstein nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )nil sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )eq -decl nil integers nil )"real" bernstein_polynomials "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"posint" nil )"DegreeMono" multi_bernstein nil )"nat" multi_bernstein nil )eq -decl nil product "reals/" )eq -decl nil product "reals/" )nil extra_real_props nil )"[T -> real]" product "reals/" )1 skolem-const-decl "nat" multi_bernstein nil )2 skolem-const-decl "nat" multi_bernstein nil )"CoeffMono" multi_bernstein nil )nil product "reals/" )"real" multi_bernstein nil ))nil ))0 3 nil 3499083601 "" case "FORALL (X: Vars, bsdegmono: DegreeMono, bspoly: MultiBernstein, AND cfn+lb<=ct AND ct<=terms-1 IMPLIES LET cfnew = (LAMBDA (i:nat): IF i<=cfn+lb AND i>=cfn THEN cf(i) ELSE 0 ENDIF) INLAMBDA (i: nat): 0 )(X)") "1" (skeep)"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "0" "terms-1" "terms-1" "terms-1" )"1" (assert )"1" case "multibs_eval(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,AND multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): 0 )(X) = multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X)") "1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2 )"2" (hide -1 )"2" (split)"1" (expand "multibs_eval" )"1" (rewrite "sigma_restrict_eq" )"1" (hide 2 )"1" (decompose-equality)"1" (expand "restrict" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" case "FORALL (v:nat,cfmono:CoeffMono): v<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,") "1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,") "1" (assert ) nil nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "v" )"2" (flatten)"2" (skeep)"2" expand "multibs_eval_rec" +)"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (induct "pz" )"1" (assert ) nil nil )"2" (skeep)"2" (case "lb = 0" )"1" (replace -1 )"1" (hide -1 )"1" (hide -1 )"1" "bspolynew" "LAMBDA (i:nat): bspoly(i+cfn)" )"1" (lemma "multibs_eval_1_term" )"1" "X" "bsdegmono" "bspolynew" "LAMBDA (i:nat): IF i=0 THEN cf(cfn) ELSE 0 ENDIF" "nvars" )"1" case "multibs_eval(bspolynew, bsdegmono, LAMBDA (i: nat): IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 )LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,and LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): 0 )(X)=LAMBDA (i: nat):IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 , nvars)LAMBDA (i: nat): 0 )(X)") "1" (assert )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil )"2" (hide 2 )"2" (hide -1 )"2" "1" expand "multibs_eval" )"1" expand "sigma" + 1 )"1" expand "sigma" + 1 )"1" "sigma_split" )"1" "1" "cfn" )"1" assert )"1" replace -1 )"1" 1 )"1" "sigma_split" )"1" "LAMBDA (i_1: nat): IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *" "cfn" "0" "cfn-1" )"1" assert )"1" replace -1 )"1" 1 )"1" case "sigma(0, cfn - 1, LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 AND 0 =1 + cfn, terms - 1 ,LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *") "1" "1" replace 1 )"1" 1 )"1" replace 1 "1" 1 )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" expand "bspolynew" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "1" rewrite "sigma_restrict_eq_0" )nil nil )"2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (cfm:CoeffMono,vv:nat): vv<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat):IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 , vv)") "1" "1" (assert ) nil nil ))nil )"2" 2 )"2" "vv" )"1" "1" expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat):IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 )") "1" (assert ) nil nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" expand "sigma" + 2 )"2" expand "sigma" 2 )"2" expand "bspolynew" )"2" "sigma_split" )"2" "2" "cfn" )"2" assert )"2" replace 1 )"2" 1 )"2" "sigma_split" )"2" "(LAMBDA (i_1: nat): IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 , nvars - 1 ,LAMBDA (j: nat): bspoly(i_1)(j)(cfm(j))))" "cfn" "0" "cfn-1" )"2" assert )"2" replace 1 )"2" 1 )"2" case "sigma(0, cfn - 1, LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 , nvars - 1 ,LAMBDA (j: nat): bspoly(i_1)(j)(cfm(j)))))=0 AND 0 =1 + cfn, terms - 1 ,LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 , nvars - 1 ,LAMBDA (j: nat): bspoly(i_1)(j)(cfm(j))))") "1" "1" replace 1 )"1" 1 )"1" replace 1 "1" 1 )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "1" rewrite "sigma_restrict_eq_0" )nil nil )"2" rewrite "sigma_restrict_eq_0" )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" 1 "vv" )"2" "2" "2" expand "multibs_eval_rec" "2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (skolem 1 "pz" )"3" (flatten)"3" (skeep)"3" (case "lb = 0" )"1" (inst?)"1" (inst - "cfn+lb" ) (("1" (assert ) nil nil ))nil ))nil )"2" (label "lbzero" 1 )"2" (hide "lbzero" )"2" "cflow" "LAMBDA (i:nat): IF i<=cfn+lb-1 AND i>=cfn THEN cf(i) ELSE 0 ENDIF" )"2" "cfhigh" "LAMBDA (i:nat): IF i=cfn+lb THEN cf(i) ELSE 0 ENDIF" )"2" case "multibs_eval(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i) ELSE 0 ENDIF,") "1" (replace -1 )"1" case "multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i)0 LAMBDA (i: nat): 0 )(X) = multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat): 0 )(X)+multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat): 0 )(X)") "1" replace -1 )"1" 1 )"1" 1 )"1" "lbzero" )"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "cfn" "ct" "lb-1" )"1" "lbzero" )"1" assert )"1" replace -2 )"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "cfn+lb" "ct" "0" )"1" assert )"1" case "(LAMBDA (i: nat): IF i <= cfn + lb AND i >= cfn + lb THEN cf(i)0 ") "1" assert )nil nil )"2" 1 )"2" expand "cfhigh" )"2" "2" if )"2" if )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" 1 )"2" 1 )"2" 1 )"2" 1 )"2" case "FORALL (v:nat,iggy:CoeffMono): v<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i)0 ") "1" "1" (assert ) nil nil ))nil )"2" 2 )"2" "v" )"1" "1" expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i)0 ") "1" assert )nil nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" rewrite "sigma_sum" )"2" 1 )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "1" expand "cfhigh" )"1" expand "cflow" )"1" if )"1" if )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "cfhigh" )"2" expand "cflow" )"2" nil nil ))nil ))nil )"3" expand "cflow" )"3" expand "cfhigh" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 "v" )"2" "2" "2" expand "multibs_eval_rec" "2" rewrite "sigma_sum" "2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (hide -1 )"2" 1 )"2" 1 )"2" expand "multibs_eval" )"2" rewrite "sigma_sum" )"2" rewrite "sigma_restrict_eq" )"2" "2" 2 )"2" expand "restrict" )"2" if )"2" "1" expand "cfhigh" )"1" expand "cflow" )"1" if )"1" if )"1" nil nil ))nil ))nil ))nil ))nil )"2" expand "cfhigh" )"2" expand "cflow" )"2" nil nil ))nil ))nil )"3" expand "cfhigh" )"3" expand "cflow" )"3" 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 )"[nat -> real]" multi_bernstein nil )"nat" multi_bernstein nil )nil sigma "reals/" )"[nat -> real]" multi_bernstein nil )nil multi_bernstein nil )"odd_int" integersnil )"[nat -> Polyproduct]" multi_bernsteinnil )nil sigma "reals/" )"real" reals nil )nil sigma "reals/" )"real" sigma "reals/" )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"real" multi_bernstein nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"[T -> real]" sigma "reals/" )"posint" nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"real" multi_bernstein nil )eq -decl nil product "reals/" )eq -decl nil product "reals/" )"real" product "reals/" )nil naturalnumbers nil )eq -decl nil defined_types nil )"RealOrder" util nil )"(total_order?[real])" 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" multi_bernstein nil )eq -decl nil util nil )"real" multi_bernstein nil )IF const-decl "[boolean, T, T -> T]" if_def nil ))nil )2 nil 3499083540 "" case "FORALL (X: Vars, bsdegmono: DegreeMono, bspoly: MultiBernstein, AND cfn+lb<=ct AND ct<=terms-1 IMPLIES LET cfnew = (LAMBDA (i:nat): IF i<=cfn+lb AND i>=cfn THEN cf(i) ELSE 0 ENDIF) INLAMBDA (i: nat): 0 )(X)") "1" (skeep)"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "0" "terms-1" "terms-1" "terms-1" )"1" (assert )"1" case "multibs_eval(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,AND multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): 0 )(X) = multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X)") "1" (assert ) (("1" (flatten) (("1" (assert ) nil )))))"2" (hide 2 )"2" (hide -1 )"2" (split)"1" (expand "multibs_eval" )"1" (rewrite "sigma_restrict_eq" )"1" (hide 2 )"1" (decompose-equality)"1" (expand "restrict" )"1" (propax) nil )))))))))))"2" case "FORALL (v:nat,cfmono:CoeffMono): v<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,") "1" (inst?) (("1" (assert ) nil )))"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,") "1" (assert ) nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" nil )))))))))))))))))))"2" (skolem 1 "v" )"2" (flatten)"2" (skeep)"2" expand "multibs_eval_rec" +)"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))"2" (hide 2 )"2" (induct "pz" )"1" (assert ) nil )"2" (skeep)"2" (case "lb = 0" )"1" (replace -1 )"1" (hide -1 )"1" (hide -1 )"1" "bspolynew" "LAMBDA (i:nat): bspoly(i+cfn)" )"1" (lemma "multibs_eval_equiv2" )"1" "X" "bsdegmono" "bspolynew" "LAMBDA (i:nat): IF i=0 THEN cf(cfn) ELSE 0 ENDIF" "nvars" )"1" case "multibs_eval(bspolynew, bsdegmono, LAMBDA (i: nat): IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 )LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,and LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): 0 )(X)=LAMBDA (i: nat):IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 , nvars)LAMBDA (i: nat): 0 )(X)") "1" (assert )"1" (flatten) (("1" (assert ) nil )))))"2" (hide 2 )"2" (hide -1 )"2" "1" expand "multibs_eval" )"1" expand "sigma" + 1 )"1" expand "sigma" + 1 )"1" "sigma_split" )"1" "1" "cfn" )"1" assert )"1" replace -1 )"1" 1 )"1" "sigma_split" )"1" "LAMBDA (i_1: nat): IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *" "cfn" "0" "cfn-1" )"1" assert )"1" replace -1 )"1" 1 )"1" case "sigma(0, cfn - 1, LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 AND 0 =1 + cfn, terms - 1 ,LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *") "1" "1" replace 1 )"1" 1 )"1" replace 1 "1" 1 )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" expand "bspolynew" )"1" nil )))))))))))))))))))"2" 2 )"2" "1" rewrite "sigma_restrict_eq_0" )nil )"2" rewrite "sigma_restrict_eq_0" )nil )))))))))))))))))))))))))))))))))))"2" case "FORALL (cfm:CoeffMono,vv:nat): vv<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat):IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 , vv)") "1" (inst?) (("1" (assert ) nil )))"2" 2 )"2" "vv" )"1" "1" expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn AND i >= cfn THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat):IF i = 0 THEN cf(cfn) ELSE 0 ENDIF,1 )") "1" (assert ) nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" expand "sigma" + 2 )"2" expand "sigma" 2 )"2" expand "bspolynew" )"2" "sigma_split" )"2" "2" "cfn" )"2" assert )"2" replace 1 )"2" 1 )"2" "sigma_split" )"2" "(LAMBDA (i_1: nat): IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 , nvars - 1 ,LAMBDA (j: nat): bspoly(i_1)(j)(cfm(j))))" "cfn" "0" "cfn-1" )"2" assert )"2" replace 1 )"2" 1 )"2" case "sigma(0, cfn - 1, LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 , nvars - 1 ,LAMBDA (j: nat): bspoly(i_1)(j)(cfm(j)))))=0 AND 0 =1 + cfn, terms - 1 ,LAMBDA (i_1: nat):IF i_1 <= cfn AND i_1 >= cfn THEN cf(i_1) ELSE 0 ENDIF *0 , nvars - 1 ,LAMBDA (j: nat): bspoly(i_1)(j)(cfm(j))))") "1" "1" replace 1 )"1" 1 )"1" replace 1 "1" 1 )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" nil )))))))))))))))))"2" 2 )"2" "1" rewrite "sigma_restrict_eq_0" )nil )"2" rewrite "sigma_restrict_eq_0" )nil )))))))))))))))))))))))))))))))))))))))))))))"2" 1 "vv" )"2" "2" "2" expand "multibs_eval_rec" "2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))))))))"2" (assert ) nil )))))"3" (skolem 1 "pz" )"3" (flatten)"3" (skeep)"3" (case "lb = 0" )"1" (inst?)"1" (inst - "cfn+lb" ) (("1" (assert ) nil )))))"2" (label "lbzero" 1 )"2" (hide "lbzero" )"2" "cflow" "LAMBDA (i:nat): IF i<=cfn+lb-1 AND i>=cfn THEN cf(i) ELSE 0 ENDIF" )"2" "cfhigh" "LAMBDA (i:nat): IF i=cfn+lb THEN cf(i) ELSE 0 ENDIF" )"2" case "multibs_eval(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i) ELSE 0 ENDIF,") "1" (replace -1 )"1" case "multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i)0 LAMBDA (i: nat): 0 )(X) = multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat): 0 )(X)+multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat): 0 )(X)") "1" replace -1 )"1" 1 )"1" 1 )"1" "lbzero" )"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "cfn" "ct" "lb-1" )"1" "lbzero" )"1" assert )"1" replace -2 )"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "cfn+lb" "ct" "0" )"1" assert )"1" case "(LAMBDA (i: nat): IF i <= cfn + lb AND i >= cfn + lb THEN cf(i)0 ") "1" (assert ) nil )"2" 1 )"2" expand "cfhigh" )"2" "2" if )"2" if )"2" nil )))))))))))))))))))))))"2" (assert ) nil )))))))))))"2" 2 )"2" 1 )"2" 1 )"2" 1 )"2" 1 )"2" case "FORALL (v:nat,iggy:CoeffMono): v<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i)0 ") "1" "1" (assert ) nil )))"2" 2 )"2" "v" )"1" "1" expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= cfn + lb AND i >= cfn THEN cf(i)0 ") "1" (assert ) nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" rewrite "sigma_sum" )"2" 1 )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "1" expand "cfhigh" )"1" expand "cflow" )"1" if )"1" if )"1" if )"1" nil )))))))))))"2" expand "cfhigh" )"2" expand "cflow" )"2" nil )))))"3" expand "cflow" )"3" expand "cfhigh" )"3" nil )))))))))))))))))))))))))))))))"2" 1 "v" )"2" "2" "2" expand "multibs_eval_rec" "2" rewrite "sigma_sum" "2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" nil )))))))))))))))))))))))))))))))))))))))))))"2" (hide 2 )"2" (hide -1 )"2" 1 )"2" 1 )"2" expand "multibs_eval" )"2" rewrite "sigma_sum" )"2" rewrite "sigma_restrict_eq" )"2" "2" 2 )"2" expand "restrict" )"2" if )"2" "1" expand "cfhigh" )"1" expand "cflow" )"1" if )"1" if )"1" if )"1" nil )))))))))))"2" expand "cfhigh" )"2" expand "cflow" )"2" nil )))))"3" expand "cfhigh" )"3" expand "cflow" )"3" nil ))))))))))))))))))))))))))))))))))))))))))))))))))))nil )nil nil )1 nil 3498990121 "" case "FORALL (X: Vars, bsdegmono: DegreeMono, bspoly: MultiBernstein, LET cfnew = (LAMBDA (i:nat): IF i<=cfn THEN cf(i) ELSE 0 ENDIF) INLAMBDA (i: nat): 0 )(X)") "1" (skeep)"1" "X" "bsdegmono" "bspoly" "cf" "nvars" "terms" "terms-1" "terms-1" )"1" (assert )"1" case "multibs_eval(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,AND multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): 0 )(X) = multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X)") "1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil )"2" (hide 2 )"2" (hide -1 )"2" (split)"1" (expand "multibs_eval" )"1" (rewrite "sigma_restrict_eq" )"1" (hide 2 )"1" (decompose-equality)"1" (expand "restrict" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" case "FORALL (v:nat,cfmono:CoeffMono): v<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,") "1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (expand "multibs_eval_rec" )"1" case "multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat):IF i <= terms - 1 THEN cf(i) ELSE 0 ENDIF,") "1" (assert ) nil nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "v" )"2" (flatten)"2" (skeep)"2" expand "multibs_eval_rec" +)"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (induct "ct" )"1" (assert ) nil nil )"2" case "FORALL (X: Vars, bsdegmono: DegreeMono, bspoly: MultiBernstein, 1 )1 , nvars)LAMBDA (i: nat): 0 )(X)") "1" (skeep)"1" (case "cfn = 0" )"1" (replace -1 )"1" (hide -3 )"1" (hide -1 )"1" case "multibs_eval(bspoly, bsdegmono, LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,1 )") "1" case " multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): 0 )(X) = multibs_eval_rec(bspoly, bsdegmono,LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,1 , nvars)LAMBDA (i: nat): 0 )(X)") "1" "X" "bsdegmono" "bspoly" "LAMBDA (i:nat): IF i<=0 THEN cf(i) ELSE 0 ENDIF" "nvars" "1" )"1" (assert ) nil nil )) nil )"2" (hide 2 )"2" (hide -1 )"2" (hide -1 )"2" case "FORALL (cfmono:CoeffMono,v:nat):v<=nvars IMPLIES multibs_eval_rec(bspoly, bsdegmono, LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,1 , v)") "1" "1" (assert ) nil nil ))nil )"2" 2 )"2" "v" )"1" "1" expand "multibs_eval_rec" )"1" case " multibs_eval_mono(bspoly, bsdegmono, LAMBDA (i: nat): IF i <= 0 THEN cf(i) ELSE 0 ENDIF,LAMBDA (i: nat):IF i <= 0 THEN cf(i) ELSE 0 ENDIF,1 )") "1" (assert ) nil nil )"2" 2 )"2" expand "multibs_eval_mono" )"2" "sigma_split" )"2" "2" "0" )"2" assert )"2" replace -1 )"2" 1 )"2" assert )"2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 "v" )"2" "2" "2" expand "multibs_eval_rec" "2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (hide -1 )"2" (expand "multibs_eval" )"2" (lemma "sigma_split" )"2" "2" "0" )"2" assert )"2" replace -1 )"2" 1 )"2" assert )"2" rewrite "sigma_restrict_eq_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2 )"2" (skeep)"2" (expand "multibs_eval" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "bsproduct_eval" )"2" case "FORALL (cfmono:CoeffMono,v:nat): v<nvars IMPLIES cf(0) * 0 , v,LAMBDA (i: nat):0 , bsdegmono(i),LAMBDA (j: nat):IF j > bsdegmono(i) THEN 0 0 )(i)(j) * Bern(j, bsdegmono(i))(X(i))1 , 1 , v+1 )") "1" (inst?) (("1" (assert ) nil nil )) nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" expand "product" )"1" expand "product" )"1" expand "multibs_eval_rec" )"1" rewrite "sigma_scal" :dir rl)"1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" if )"1" "1" 3 )"1" expand "multibs_eval_rec" )"1" expand "product" )"1" expand "product" )"1" expand "multibs_eval_mono" )"1" expand "sigma" )"1" expand "product" )"1" expand "sigma" )"1" expand "product" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "v" )"2" "2" "2" expand "product " +)"2" "1" assert )"1" case "NOT cf(0) * 0 , bsdegmono(1 + v),LAMBDA (j: nat):IF j > bsdegmono(1 + v) THEN 0 0 )(1 + v)(j) *1 + v))(X(1 + v))0 , v,LAMBDA (i: nat):0 , bsdegmono(i),LAMBDA (j: nat):IF j > bsdegmono(i) THEN 0 0 )(i)(j) *1 + v, 1 , 1 + v)(cf)(X)*sigma(0 , bsdegmono(1 + v),LAMBDA (j: nat):IF j > bsdegmono(1 + v) THEN 0 0 )(1 + v)(j) *1 + v))(X(1 + v))") "1" (assert ) nil nil )"2" replace -1 )"2" 1 )"2" 1 )"2" expand "multibs_eval_rec" 2 )"2" rewrite "sigma_scal" "2" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" if )"1" "1" 3 )"1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil )"4" (postpone) nil nil )"5" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil )"4" (postpone) nil nil ))nil ))nil )"3" (postpone) nil nil )"4" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (postpone) nil nil ))nil ))nil ))nil )nil shostak))0 1 nil 3509119235 "" (skosimp*)"" (expand "multibs_eval" )"" (rewrite "sigma_eq" )"" (hide 2 )"" (skosimp*)"" case "bsproduct_eval(bspoly!1(n!1), bsdegmono!1, nvars!1)(X!1) 1 (n!1 ), bsdegmono!1 , nvars!1 )(Y!1 )") "1" (assert ) nil nil )"2" (hide 2 )"2" (expand "bsproduct_eval" )"2" (rewrite "product_eq" )"1" (hide 2 )"1" (skosimp*)"1" (rewrite "sigma_eq" )"1" (hide 2 )"1" (skosimp*)"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" multi_bernstein nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil integers nil )"RealOrder" util nil )"(total_order?[real])" nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )nil product "reals/" )"real" sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )eq -decl nil integers nil )"real" bernstein_polynomials "reals/" )eq -decl nil product "reals/" )eq -decl nil product "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 )eq -decl nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil util nil )"real" multi_bernstein nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )nil sigma "reals/" )"int" integers nil )"real" reals nil ))0 1 nil 3500206292 "" (skeep)"" (expand "multibs_eval" )"" (decompose-equality)"" (rewrite "sigma_restrict_eq" )"" (hide 2 )"" (decompose-equality)"" (expand "restrict" )"" (lift-if )"" (ground)"" case "bsproduct_eval(bspoly(x!2), bsdegmono, nvars)(x!1) = 2 ), bsdegmono, nvars)(x!1 )") "1" (assert ) nil nil )"2" (hide 3 )"2" (expand "bsproduct_eval" )"2" (rewrite "product_restrict_eq" )"1" (hide 2 )"1" "1" expand "restrict" )"1" if )"1" "1" rewrite "sigma_restrict_eq" )"1" 3 )"1" "1" expand "restrict" )"1" if )"1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" multi_bernstein nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )"[T, T -> boolean]" equalities nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil naturalnumbers nil )3 skolem-const-decl "nat" multi_bernstein nil )"[T -> real]" product "reals/" )"DegreeMono" multi_bernstein nil )nil product "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )eq -decl nil integers nil )"real" bernstein_polynomials "reals/" )eq -decl nil product "reals/" )eq -decl nil product "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil util nil )"real" multi_bernstein nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )"real" sigma "reals/" )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil util nil )"int" integers nil )"real" reals nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3509113819 "" (skeep)"" (expand "multibscoeff" )"" (rewrite "sigma_eq" )"" (hide 2 )"" (skosimp*)"" case "product(0, nvars - 1, LAMBDA (j: nat): bspoly(n!1 )(j)(coeffmono1(j)))0 , nvars - 1 ,LAMBDA (j: nat): bspoly(n!1 )(j)(coeffmono2(j)))") "1" (assert ) nil nil )"2" (hide 2 )"2" (rewrite "product_eq" )"2" (hide 2 )"2" (skosimp*)"2" (expand "eq_below_mono?" )"2" (inst - "n!2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" multi_bernstein nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil integers nil )nil product "reals/" )eq -decl nil naturalnumbers nil )"bool" reals nil )"bool" util nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" product "reals/" )eq -decl nil product "reals/" )eq -decl nil product "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil util nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )nil sigma "reals/" )"real" reals nil )"int" integers nil )"RealOrder" util nil )"(total_order?[real])" nil ))0 1 nil 3499007668 "" (induct "v" )"1" (skeep)"1" (expand "Bern_coeffs_rel_rec" )"1" (inst?) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (skolem 1 "v" )"2" (flatten)"2" (skeep)"2" (expand "Bern_coeffs_rel_rec" (-3 1 ))"2" (skosimp*)"2" (inst -3 "d!1" )"2" "a" "a1" "bsdegmono" "bspoly" "cf" "coeffmono WITH [(v):=d!1]" "nvars" "rel" "terms" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"posint" nil )"real" multi_bernstein nil )nil naturalnumbers nil )"bool" multi_bernstein nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil defined_types nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 ))0 1 nil 3498927613 "" case "FORALL (a: real, bsdegmono: DegreeMono, bspoly: MultiBernstein, ffmono(j)) IMPLIES multibscoeff(bspoly, bsdegmono, cf, nvars, terms)") "1" (label "cmlem" -1 )"1" (hide "cmlem" )"1" case "FORALL (a: real, bsdegmono: DegreeMono, bspoly: MultiBernstein, and v<=nvars IMPLIESAND (FORALL (k:nat): k>=v AND k<nvars IMPLIES iggy(k)=coeffmono(k)) IMPLIES") "1" (skeep)"1" (ground)"1" "a" "bsdegmono" "bspoly" "cf" "nvars" "rel" "terms" "nvars" "LAMBDA (i:nat): 0" )"1" (expand "Bern_coeffs_rel" )"1" (assert )"1" (skosimp*)"1" (split -)"1" (inst - "coeffmono!1" )"1" (assert )"1" (skosimp*) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1 ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "a" "bsdegmono" "bspoly" "cf" "nvars" "rel" "terms" "nvars" "LAMBDA (i:nat): 0" )"2" (ground)"1" (expand "Bern_coeffs_rel" )"1" (propax) nil nil )) nil )"2" (skosimp*)"2" (inst -3 "coeffmono!1" )"2" (assert ) nil nil )) nil ))nil )"3" (hide-all-but 1 ) (("3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (hide -2 )"1" (ground)"1" (skosimp*)"1" (reveal "cmlem" )"1" "a" "bsdegmono" "bspoly" "cf" "nvars" "rel" "terms" "nvars" "iggy" "coeffmono!1" )"1" (assert )"1" (expand "Bern_coeffs_rel_rec" )"1" assert )"1" "1" "j!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst - "iggy" )"2" (assert )"2" (expand "Bern_coeffs_rel_rec" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "vv" )"2" (flatten)"2" (skeep)"2" (ground)"1" (skosimp*)"1" (expand "Bern_coeffs_rel_rec" -1 )"1" (inst - "coeffmono!1(vv)" )"1" (inst? -4 )"1" assert )"1" "1" "coeffmono!1" )"1" assert )"1" "1" "k!1" )"1" assert )"1" "1" case "k!1 = vv" )"1" replace -1 )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "le_below_mono?" )"2" "2" case "j!1 = vv" )"1" "vv" )"1" (assert ) nil nil ))nil )"2" 4 "j!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" expand "le_below_mono?" )"2" (inst - "vv" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "Bern_coeffs_rel_rec" +)"2" (skosimp*)"2" (inst? -2 )"2" assert )"2" "1" 2 )"1" "1" 3 "coeffmono!1" )"1" assert )"1" "1" 2 "k!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" 1 )"2" expand "le_below_mono?" )"2" "2" "j!1" )"2" case "j!1 = vv" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (skeep)"2" (expand "multibscoeff" )"2" (rewrite "sigma_restrict_eq" )"2" (hide 2 )"2" (decompose-equality)"2" (expand "restrict" )"2" (lift-if )"2" (ground)"2" case "product(0, nvars - 1, LAMBDA (j: nat): bspoly(x!1)(j)(coeffmono(j))) 0 , nvars - 1 , LAMBDA (j: nat): bspoly(x!1 )(j)(iggy(j)))") "1" (assert ) nil nil )"2" (hide 3 )"2" (rewrite "product_restrict_eq" )"2" (hide 2 )"2" "2" expand "restrict" )"2" if )"2" "2" "x!2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"[T -> real]" product "reals/" )nil product "reals/" )"[T -> real]" sigma "reals/" )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"real" product "reals/" )eq -decl nil product "reals/" )eq -decl nil product "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )nil sigma "reals/" )"real" reals nil )"int" integers nil )"bool" multi_bernstein nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" util nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" multi_bernstein nil )NOT const-decl "[bool -> bool]" booleans nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )eq -decl nil defined_types nil )nil naturalnumbers nil )"posint" nil )"posint" nil )eq -decl nil naturalnumbers nil )"DegreeMono" multi_bernstein nil )"nat" multi_bernstein nil )1 skolem-const-decl "CoeffMono" multi_bernstein 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"real" multi_bernstein nil ))0 2 nil 3509117841 "" (skosimp*)"" (assert )"" "Xv" "LAMBDA (i: nat): IF coeffmono!1 (i) = 0 THEN 0 ELSE 1 ENDIF") "" (replace -1 )"" (flatten)"" (expand "multibscoeff" )"" (expand "multibs_eval" )"" (rewrite "sigma_eq" )"" (hide 2 )"" (skosimp*)"" case "bsproduct_eval(bspoly!1(n!1), bsdegmono!1, nvars!1)(Xv) = 0 , nvars!1 - 1 ,LAMBDA (j: nat): bspoly!1 (n!1 )(j)(coeffmono!1 (j)))") "1" (assert ) nil nil )"2" (hide 2 )"2" (expand "bsproduct_eval" )"2" (rewrite "product_eq" )"1" 2 )"1" "1" "sigma_split" )"1" "1" "coeffmono!1(n!2)" )"1" assert )"1" "1" replace -1 )"1" 1 )"1" "sigma_split" )"1" 1 "coeffmono!1(n!2)-1" )"1" "1" assert )"1" replace -1 )"1" 1 )"1" case "sigma(0, coeffmono!1(n!2) - 1, LAMBDA (j: nat):IF j > bsdegmono!1 (n!2 ) THEN 0 1 (n!1 )(n!2 )(j) *1 (n!2 ))(Xv(n!2 ))0 AND sigma(1 + coeffmono!1 (n!2 ), bsdegmono!1 (n!2 ),LAMBDA (j: nat):IF j > bsdegmono!1 (n!2 ) THEN 0 1 (n!1 )(n!2 )(j) *1 (n!2 ))(Xv(n!2 ))0 ") "1" "1" replace 1 )"1" 1 )"1" replace 1 )"1" 1 )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" if )"1" "1" expand "corner_point?" )"1" "n!2" )"1" assert )nil nil ))nil ))nil )"2" case "Bern(coeffmono!1(n!2), bsdegmono!1(n!2))(Xv(n!2))=1" )"1" assert )nil nil )"2" 2 )"2" 2 )"2" expand "Xv" "2" if )"2" "1" expand "Bern" )"1" rewrite "expt_1i" )"1" replace 1 )"1" expand "^" )"1" expand "expt" )"1" expand "C" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "Bern" )"2" rewrite "expt_1i" )"2" expand "corner_point?" )"2" "n!2" )"2" assert )"2" replace 2 )"2" assert )"2" expand "^" )"2" expand "expt" )"2" expand "C" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "1" rewrite "sigma_restrict_eq_0" )"1" 2 )"1" "1" if )"1" "1" expand "Bern" )"1" expand "Xv" "1" expand "^" )"1" expand "expt" 1 )"1" if )"1" "1" expand "corner_point?" )"1" "n!2" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sigma_restrict_eq_0" )"2" 2 )"2" "2" expand "Bern" )"2" expand "Xv" "2" if )"2" "1" expand "^" 1 )"1" expand "expt" "1" nil nil ))nil ))nil )"2" expand "^" 1 )"2" expand "expt" "2" if )"2" "2" expand "corner_point?" )"2" "n!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" 2 )"3" "3" assert )nil nil ))nil ))nil )"4" "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "corner_point?" )"2" "n!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" multi_bernstein nil )"(total_order?[real])" nil )"RealOrder" util nil )"real" reals nil )"int" integers nil )nil sigma "reals/" )eq -decl nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )"real" multi_bernstein nil )eq -decl nil util nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil product "reals/" )eq -decl nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"real" bernstein_polynomials "reals/" )eq -decl nil integers nil )"real" sigma "reals/" )nil product "reals/" )1 skolem-const-decl "DegreeMono" multi_bernstein nil )1 skolem-const-decl "posnat" multi_bernstein nil )2 skolem-const-decl "subrange(0, nvars!1 - 1)" multi_bernsteinnil )"odd_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )eq -decl nil naturalnumbers nil )"bool" reals nil )"bool" util nil )"[nat -> naturalnumber]" multi_bernstein nil )nil exponentiation nil )"nat" exponentiation nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"real" exponentiation nil )"posnat" binomial "reals/" )"posrat" nil )"posint" nil )nil factorial "ints/" )"real" exponentiation nil )"posint" exponentiation nil )"even_int" integersnil )"posnat" exponentiation nil )"even_int" integersnil )"nat" exponentiation nil )nil sigma "reals/" )"nonneg_rat" nil )"odd_int" integersnil )"nzreal" exponentiation nil )"rat" exponentiation nil )"nzrat" rationalsnil )"rat" rationals nil )"even_int" integersnil )"int" exponentiation nil )"real" reals nil )"posint" nil )nil sigma "reals/" )eq -decl nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" multi_bernstein 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )eq -decl nil util nil )eq -decl nil naturalnumbers nil ))nil )1 nil 3509117746 "" (skeep)"" (assert )"" "Xv" "LAMBDA (i: nat): IF coeffmon(i) = 0 THEN 0 ELSE 1 ENDIF") "" (replace -1 )"" (flatten) (("" (postpone) nil nil )) nil )) nil ))nil ))nil ))nil )nil shostak))0 1 nil 3499949735 "" case "FORALL (cf: Coeff, bspoly, bspolz, bsdegmono, nvars, terms, rel, a): ") "1" (skeep)"1" (iff)"1" (split)"1" (inst?) (("1" (ground) nil nil )) nil )"2" (inst?)"2" (ground)"2" (skeep)"2" (inst? -2 ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (skeep)"2" (expand "forall_X" )"2" (skeep)"2" (inst? -2 )"2" (assert )"2" (lemma "multibs_eval_id" )"2" 1 "bspoly" "bspolz" "bsdegmono" "cf" "nvars" "terms" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )eq -decl nil util nil )nil multi_bernstein 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" multi_bernstein nil ))0 1 nil 3507233890 "" case "FORALL (cf: Coeff, amin, amax: real) ") "1" (skosimp*)"1" (iff)"1" (split)"1" (inst?) (("1" (ground) nil nil )) nil )"2" 1 "cf!1" "amin!1" "amax!1" "bspolz!1" "bspoly!1" "bsdegmono!1" "nvars!1" "terms!1" )"2" (ground)"2" (skeep 1 )"2" (inst? -2 ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (skosimp*)"2" (expand "forall_X_between" )"2" (skeep)"2" (inst? -2 )"2" (assert )"2" (lemma "multibs_eval_id" )"2" (inst?)"2" (inst -1 "bspolz!1" )"2" (split -1 )"1" (ground) nil nil ) ("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )eq -decl nil util nil )nil multi_bernstein nil )"RealOrder" util nil )"(total_order?[real])" 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"bool" multi_bernstein nil ))nil ))0 1 nil 3499440937 "" (skeep) (("" (assert ) nil nil )) nil ) nil nil ))0 1 nil 3499440937 "" (skeep) (("" (assert ) nil nil )) nil ) nil nil ))0 1 nil 3503309476 "" (subtype-tcc) nil nil )nil booleans nil )eq -decl 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 )eq -decl nil integers nil )eq -decl nil naturalnumbers nil )"int" integers nil )"(total_order?[real])" nil )"RealOrder" util nil ))nil ))0 1 nil 3503309476 "" (subtype-tcc) nil nil ) nil nil ))0 1 nil 3503309637 "" (skeep) (("" (assert ) nil nil )) nil ) nil nil ))0 1 nil 3499440937 "" (expand "Bern_coeffs_endpoints_rel" )"" "eptest?" "(LAMBDA (bsdegmono:DegreeMono,nvars): (LAMBDA (cfm:CoeffMono): (FORALL (i:below(nvars)): cfm(i)=0 OR cfm(i)=bsdegmono(i))))" )"" (skosimp*)"" (lift-if )"" (split)"1" (flatten)"1" case "FORALL (a: real, bsdegmono: DegreeMono, bspoly: MultiBernstein, AND ") "1" (inst?)"1" (assert ) nil nil )"2" (hide 2 )"2" (expand "eptest?" ) (("2" (propax) nil nil ))nil ))nil ))nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (expand "Bern_coeffs_endpoints_rel_rec" )"1" (assert )"1" (lift-if +)"1" (assert )"1" "1" 2 )"1" "Xnew" "LAMBDA (i:nat): IF cfm(i)=0 THEN 0 ELSE 1 ENDIF" )"1" expand "forall_X" )"1" "Xnew" )"1" "1" case "multibs_eval(bspoly, bsdegmono, cf, nvars, terms)(Xnew) = multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(cfm)" )"1" (assert ) nil nil )"2" 2 )"2" expand "multibscoeff" )"2" expand "multibs_eval" )"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" case "bsproduct_eval(bspoly(x!1), bsdegmono, nvars)(Xnew) = 0 , nvars - 1 , LAMBDA (j: nat): bspoly(x!1 )(j)(cfm(j)))") "1" assert )nil nil )"2" 3 )"2" expand "bsproduct_eval" "2" rewrite "product_restrict_eq" )"1" 2 )"1" "1" expand "restrict" )"1" if )"1" "1" "cfm" )"1" "sigma_split" )"1" "1" "cfm(x!2)" )"1" assert )"1" case "cfm(x!2)<=bsdegmono(x!2)" )"1" assert )"1" replace 2 )"1" 2 )"1" case "sigma(1 + cfm(x!2), bsdegmono(x!2), LAMBDA (j: nat):IF j > bsdegmono(x!2 ) THEN 0 1 )(x!2 )(j) *2 ))(Xnew(x!2 ))0 ") "1" replace 1 )"1" 1 )"1" assert )"1" "sigma_split" )"1" "1" "cfm(x!2)-1" )"1" assert )"1" replace 1 )"1" 1 )"1" case "sigma(0, cfm(x!2) - 1, LAMBDA (j: nat):IF j > bsdegmono(x!2 ) THEN 0 1 )(x!2 )(j) * Bern(j, bsdegmono(x!2 ))(Xnew(x!2 ))0 ") "1" replace 1 )"1" 1 )"1" assert )"1" expand "sigma" "1" expand "sigma" "1" expand "Xnew" "1" if )"1" "1" replace 1 )"1" expand "Bern" "1" assert )"1" expand "^" "1" expand "expt" 1 )"1" case "FORALL (t:nat): expt(1,t) = 1" )"1" "bsdegmono(x!2)" )"1" replace 1 )"1" assert )"1" expand "C" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" 1 )"2" "t" )"1" expand "expt" )"1" nil nil ))nil )"2" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cfm" )"2" expand "eptest?" 1 )"2" "x!2" )"2" assert )"2" replace 1 )"2" expand "Bern" "2" expand "^" "2" expand "expt" 1 )"2" case "FORALL (t:nat): expt(1,t) = 1" )"1" "bsdegmono(x!2)" )"1" replace 1 )"1" expand "C" "1" assert )nil nil ))nil ))nil ))nil )"2" 1 )"2" "t" )"1" expand "expt" )"1" nil nil ))nil )"2" "2" expand "expt" "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 )"2" 3 )"2" rewrite "sigma_restrict_eq_0" )"2" 2 )"2" "2" "i!1" )"2" expand "Xnew" "2" expand "Bern" "2" case "FORALL (t:nat): 0^(t+1)=0" )"1" "bsdegmono(x!2)-i!1-1" )"1" assert )nil nil ))nil )"2" 1 )"2" "t" )"1" expand "^" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" assert )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 ))nil ))nil ))nil ))nil ))nil )"2" 3 )"2" rewrite "sigma_restrict_eq_0" )"2" 2 )"2" "2" expand "Xnew" "2" if )"2" "1" expand "Bern" "1" expand "^" )"1" expand "expt" 1 )"1" nil nil ))nil ))nil ))nil )"2" expand "Bern" "2" "i!1" )"2" "cfm" )"2" expand "eptest?" 1 )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" expand "eptest?" 1 )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" expand "Xnew" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "vv" )"2" (flatten)"2" (skeep)"2" expand "Bern_coeffs_endpoints_rel_rec" +)"2" (lift-if )"2" "1" "1" (assert ) nil nil )"2" 1 )"2" expand "eptest?" )"2" "2" if )"2" "2" "cfm" )"2" expand "eptest?" )"2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "a" "bsdegmono" "bspoly" "cf" "nvars" "rel" "terms" "cfm WITH [(vv):=bsdegmono(vv)]" )"1" (assert ) nil nil )"2" 1 )"2" expand "eptest?" )"2" "2" if )"2" "2" "cfm" )"2" expand "eptest?" )"2" "i!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil naturalnumbers nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 )"DegreeMono" multi_bernstein nil )"posnat" multi_bernstein nil )"(eptest?(bsdegmono, nvars))" nil )"nat" multi_bernstein nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"real" bernstein_polynomials "reals/" )eq -decl nil integers nil )"real" sigma "reals/" )nil product "reals/" )"DegreeMono" multi_bernstein nil )"[T -> real]" product "reals/" )2 skolem-const-decl "nat" multi_bernstein nil )"odd_int" integersnil )"real" reals nil )eq -decl nil integers nil )"nat" exponentiation nil )"even_int" integersnil )"int" integers nil )"nonneg_rat" nil )"nnrat" exponentiation nil )"boolean" notequal nil )"posint" nil )nil sigma "reals/" )"posint" exponentiation nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"real" exponentiation nil )nil factorial "ints/" )"posrat" nil )"posnat" binomial "reals/" )"posint" nil )"posnat" exponentiation nil )"real" exponentiation nil )"[nat -> naturalnumber]" multi_bernsteinnil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )nil sigma "reals/" )eq -decl nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_bernstein nil )eq -decl nil product "reals/" )eq -decl nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )"RealOrder" util nil )"(total_order?[real])" nil )"real" multi_bernstein nil )"real" multi_bernstein nil )eq -decl nil naturalnumbers nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil naturalnumbers nil )eq -decl nil defined_types nil )"[[DegreeMono, posnat] -> [CoeffMono -> boolean]]" multi_bernsteinnil )1 skolem-const-decl "DegreeMono" multi_bernstein nil )1 skolem-const-decl "posnat" multi_bernstein nil )"RealOrder" util nil )"(total_order?[real])" nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" multi_bernstein nil )nil list_adt nil )eq -decl nil defined_types nil )"boolean" list_adt nil )"[list -> boolean]" list_adt nil )"[list -> boolean]" list_adt nil )eq -decl nil util nil )"bool" util nil )"T" array2list "structures/" )"nat" list_props nil )"{l: list[real] | 0 )(l)) AND length(l) = nvars}" nil )"{l: list[real] | 0 )(l)) AND length(l) = nvars}" nil ))0 1 nil 3499800124 "" (expand "Bern_coeffs_endpoints_rel" )"" "eptest?" "(LAMBDA (bsdegmono:DegreeMono,nvars): (LAMBDA (cfm:CoeffMono): (FORALL (i:below(nvars)): cfm(i)=0 OR cfm(i)=bsdegmono(i))))" )"" case "NOT FORALL (a: real, bsdegmono: DegreeMono, bspoly: MultiBernstein, NOT null?(Bern_coeffs_endpoints_rel_rec(bspoly,") "1" (hide-all-but (-1 1 ))"1" (skeep)"1" "Bern_coeffs_endpoints_rel_rec(bspoly, ") "1" (assert ) nil nil )) nil ))nil ))nil )"2" case "FORALL (a: real, bsdegmono: DegreeMono, bspoly: MultiBernstein, NOT null?(Bern_coeffs_endpoints_rel_rec(bspoly,NOT rel(multibs_eval(bspoly, bsdegmono, cf, nvars, terms)0 )") "1" (skeep)"1" case "FORALL (j: below(nvars)): intendpts(j)`1 AND intendpts(j)`2" )"1" (replace -1 )"1" (inst? -3 )"1" (assert )"1" (inst? -2 )"1" (assert ) nil nil )"2" (hide-all-but 1 )"2" (expand "eptest?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (hide-all-but 1 )"2" (expand "eptest?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (replace 1 ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (inst?)"1" (assert )"1" (expand "Bern_coeffs_endpoints_rel_rec" )"1" (lift-if )"1" (ground)"1" (hide 2 3 )"1" "Xnew" "LAMBDA (i:nat): IF i<nvars THEN (IF cfm(i)=0 THEN 0 ELSE 1 ENDIF) ELSE 0 ENDIF" )"1" case "list2array(0)(corner_to_point(cfm, nvars)) = Xnew" )"1" replace -1 )"1" 1 )"1" case "multibs_eval(bspoly, bsdegmono, cf, nvars, terms)(Xnew) = multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(cfm)" )"1" (assert ) nil nil )"2" 2 )"2" 2 )"2" expand "multibscoeff" )"2" expand "multibs_eval" +)"2" rewrite "sigma_restrict_eq" )"2" 2 )"2" "2" expand "restrict" )"2" if )"2" "2" case "bsproduct_eval(bspoly(x!1), bsdegmono, nvars)(Xnew) = 0 , nvars - 1 , LAMBDA (j: nat): bspoly(x!1 )(j)(cfm(j)))") "1" assert )nil nil )"2" 3 )"2" expand "bsproduct_eval" "2" rewrite "product_restrict_eq" )"1" 2 )"1" "1" expand "restrict" )"1" if )"1" "1" "cfm" )"1" "sigma_split" )"1" "1" "cfm(x!2)" )"1" assert )"1" case "cfm(x!2)<=bsdegmono(x!2)" )"1" assert )"1" replace 2 )"1" 2 )"1" case "sigma(1 + cfm(x!2), bsdegmono(x!2), LAMBDA (j: nat):IF j > bsdegmono(x!2 ) THEN 0 1 )(x!2 )(j) *2 ))(Xnew(x!2 ))0 ") "1" replace 1 )"1" 1 )"1" assert )"1" "sigma_split" )"1" "1" "cfm(x!2)-1" )"1" assert )"1" replace 1 )"1" 1 )"1" case "sigma(0, cfm(x!2) - 1, LAMBDA (j: nat):IF j > bsdegmono(x!2 ) THEN 0 1 )(x!2 )(j) * Bern(j, bsdegmono(x!2 ))(Xnew(x!2 ))0 ") "1" replace 1 )"1" 1 )"1" assert )"1" expand "sigma" "1" expand "sigma" "1" expand "Xnew" "1" if )"1" "1" replace 1 )"1" expand "Bern" "1" assert )"1" expand "^" "1" expand "expt" 1 )"1" "expt_1i" )"1" "bsdegmono(x!2)" )"1" assert )"1" expand "C" "1" assert )"1" expand "^" 1 )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "cfm" )"2" expand "eptest?" 1 )"2" "x!2" )"2" assert )"2" replace 1 )"2" expand "Bern" "2" expand "^" "2" expand "expt" 1 )"2" "expt_1i" )"2" "bsdegmono(x!2)" )"2" expand "^" 1 )"2" replace 1 )"2" expand "C" "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 )"2" 3 )"2" rewrite "sigma_restrict_eq_0" )"2" 2 )"2" "2" "i!1" )"2" expand "Xnew" "2" expand "Bern" "2" expand "^" "2" expand "expt" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 3 )"2" rewrite "sigma_restrict_eq_0" )"2" 2 )"2" "2" expand "Xnew" "2" if )"2" "1" expand "Bern" "1" expand "^" )"1" expand "expt" 1 )"1" nil nil ))nil ))nil ))nil )"2" expand "Bern" "2" "i!1" )"2" "cfm" )"2" expand "eptest?" 1 )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" 1 )"2" expand "eptest?" 1 )"2" "x!2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 :dir rl)"2" 1 )"2" expand "corner_to_point" )"2" case "x!1 < nvars" )"1" assert )"1" rewrite "array2list_inv[real]" )nil nil ))nil )"2" assert )"2" rewrite "list2array_sound" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "vv" )"2" (flatten)"2" (skeep)"2" expand "Bern_coeffs_endpoints_rel_rec" (-2 1 ))"2" (lift-if )"2" (ground)"1" (inst? -4 )"1" (assert ) nil nil )"2" (hide-all-but 1 )"2" "cfm" )"2" expand "eptest?" )"2" "2" "i!1" )"2" if )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst? -2 )"1" (assert ) nil nil )"2" (hide-all-but 1 )"2" "cfm" )"2" expand "eptest?" )"2" "2" "i!1" )"2" if )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil naturalnumbers nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 )"real" multi_bernstein nil )eq -decl nil util nil )"[[DegreeMono, posnat] -> [CoeffMono -> boolean]]" multi_bernsteinnil )"DegreeMono" multi_bernstein nil )"posnat" multi_bernstein nil )eq -decl nil defined_types nil )nil naturalnumbers nil )nil more_list_props "structures/" )IF const-decl "[boolean, T, T -> T]" if_def nil )eq -decl nil naturalnumbers nil )nil array2list "structures/" )eq -decl nil nat_types nil )"T" list_props nil )"{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" "structures/" )nil array2list "structures/" )"real" multi_bernstein nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" bernstein_polynomials "reals/" )eq -decl nil integers nil )"real" sigma "reals/" )nil product "reals/" )"DegreeMono" multi_bernstein nil )"[T -> real]" product "reals/" )2 skolem-const-decl "nat" multi_bernstein nil )"odd_int" integersnil )"real" reals nil )eq -decl nil integers nil )nil sigma "reals/" )"posint" exponentiation nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"real" exponentiation nil )"posnat" binomial "reals/" )nil factorial "ints/" )"posrat" nil )"posrat" nil )"posint" nil )"posnat" exponentiation nil )nil exponentiation nil )"real" exponentiation nil )"[nat -> naturalnumber]" multi_bernsteinnil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )"RealOrder" util nil )"(total_order?[real])" nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"int" integers nil )nil sigma "reals/" )eq -decl nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_bernstein nil )"bool" reals nil )eq -decl nil product "reals/" )eq -decl nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )"RealOrder" util nil )"(total_order?[real])" nil )"{l: listn[real](nvars) | unitbox?(nvars)(list2array(0)(l))}" utilnil )eq -decl nil listn "structures/" )"nat" multi_bernstein nil )"(eptest?(bsdegmono, nvars))" nil )"posnat" multi_bernstein nil )"DegreeMono" multi_bernstein nil )NOT const-decl "[bool -> bool]" booleans nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )"[bool, bool -> bool]" booleans nil )nil list_adt nil )eq -decl nil defined_types nil )"boolean" list_adt nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[list -> boolean]" list_adt nil )"[list -> boolean]" list_adt nil )eq -decl nil util nil )"bool" util nil )"T" array2list "structures/" )"nat" list_props nil )"{l: list[real] | 0 )(l)) AND length(l) = nvars}" nil )"{l: list[real] | 0 )(l)) AND length(l) = nvars}" nil ))nil ))0 1 nil 3499875743 "" (skeep)"" (rewrite "Bern_coeffs_rel_def" )"" (expand "forall_X" )"" (skosimp*)"" (rewrite "multibs_eval_equiv" )"" (name "cfnew" "LAMBDA (i:nat): a/(terms)" )"" (name "bspolynew" "LAMBDA(i:nat)(j:nat)(k:nat): 1" )"" case "multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, nvars) LAMBDA (i: nat): 0 )(X!1 ) <= multibs_eval_rec(bspolynew, bsdegmono, cfnew, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X!1 ) AND multibs_eval_rec(bspolynew, bsdegmono, cfnew, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X!1 ) =a") "1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 2 )"2" (split)"1" case "FORALL (cmo:CoeffMono,v:nat): v<=nvars AND le_below_mono?(nvars)(cmo,bsdegmono) IMPLIES multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, v) 1 )1 )") "1" (inst?)"1" (assert )"1" (hide-all-but 1 )"1" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" expand "multibs_eval_rec" +)"1" case "product(0, nvars - 1, LAMBDA (k: nat):IF cmo(k) <= bsdegmono(k)1 (k))1 0 ") "1" case "multibs_eval_mono(bspoly, bsdegmono, cf, nvars, terms)(cmo) ") "1" 1 "product(0, nvars - 1, LAMBDA (k: nat):IF cmo(k) <= bsdegmono(k)1 (k))1 ") "1" 2 )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" 2 )"2" 1 )"2" expand "multibs_eval_mono" )"2" expand "bspolynew" +)"2" expand "cfnew" +)"2" expand "multibscoeff" )"2" "cmo" )"2" assert )"2" case "FORALL (j:nat): j<terms IMPLIES sigma(0, j, LAMBDA (i: nat):0 , nvars - 1 , LAMBDA (j: nat): 1 )) = a*((j+1 )/(terms))") "1" "terms-1" )"1" assert )nil nil ))nil )"2" 2 )"2" case "FORALL (kr:nat): product(0,kr,LAMBDA (j:nat): 1) = 1" )"1" "j" )"1" assert )"1" expand "sigma" "1" expand "sigma" "1" "nvars-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" 1 "j" )"2" "2" assert )"2" expand "sigma" "2" replace 1 )"2" "nvars-1" )"2" replace 3 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "kr" )"1" expand "product" )"1" expand "product" )"1" nil nil ))nil ))nil )"2" 1 "kr" )"2" "2" expand "product" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" case "FORALL (kr:nat): kr<=nvars-1 IMPLIES product(0, kr, LAMBDA (k: nat):IF cmo(k) <= bsdegmono(k)1 (k))1 0 ") "1" "nvars-1" )"1" (assert ) nil nil ))nil )"2" 2 )"2" "kr" )"1" "1" expand "product" )"1" expand "product" )"1" if )"1" "1" "Bern_nonnegative" )"1" "X!1(0)" )"1" "1" nil nil )"2" expand "unitbox?" )"2" "2" 8 "0" )"2" nil nil ))nil ))nil ))nil )"3" "3" expand "unitbox?" )"3" 8 "0" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "product" +)"2" if )"2" "2" 2 "Bern(cmo(1 + j), bsdegmono(1 + j))(X!1(1 + j))" )"1" assert )nil nil )"2" 2 )"2" "2" assert )nil nil ))nil ))nil )"3" 2 )"3" "Bern_nonnegative" )"3" "X!1(1+j)" )"3" expand "unitbox?" )"3" 10 "1+j" )"3" "1" nil nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skeep)"2" "2" expand "multibs_eval_rec" +)"2" rewrite "sigma_le" )"2" 2 )"2" "2" "2" assert )"2" 1 )"2" expand "le_below_mono?" )"2" "2" case "j!1 = j" )"1" assert )nil nil )"2" 2 "j!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "multibs_eval_equiv" + :dir rl)"2" (expand "multibs_eval" )"2" case "(LAMBDA (i: nat): 1 )) = (LAMBDA (i:nat): a/terms)") "1" (replace -1 )"1" 1 )"1" case "FORALL (j:nat): j<terms IMPLIES sigma(0,j,(LAMBDA (i:nat): a/terms)) = (j+1)*a/terms" )"1" "terms-1" )"1" (assert ) nil nil ))nil )"2" 2 )"2" "j" )"1" assert )"1" expand "sigma" )"1" expand "sigma" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" 1 "j" )"2" "2" assert )"2" expand "sigma" +)"2" replace -1 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" "2" expand "cfnew" )"2" expand "bsproduct_eval" )"2" expand "bspolynew" )"2" case "(LAMBDA (i: nat): 0 , bsdegmono(i),LAMBDA (j: nat):IF j > bsdegmono(i) THEN 0 1 * Bern(j, bsdegmono(i))(X!1 (i))LAMBDA (i:nat): 1 )") "1" replace -1 )"1" 1 )"1" case "FORALL (kr:nat): product(0,kr,LAMBDA (j:nat): 1) = 1" )"1" "nvars-1" )"1" replace -1 )"1" assert )nil nil ))nil ))nil )"2" 2 )"2" "kr" )"1" expand "product" )"1" expand "product" )"1" nil nil ))nil ))nil )"2" 1 "jj" )"2" "2" expand "product" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "1" "Bernstein_partition_of_unity" )"1" "bsdegmono(x!2)" "X!1(x!2)" )"1" assert )"1" replace -1 )"1" nil nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil )"4" "4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil multi_bernstein 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 )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil naturalnumbers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )"real" reals nil )eq -decl nil number_fields nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil util nil )"real" multi_bernstein nil )"(total_order?[real])" nil )"RealOrder" util nil )eq -decl nil integers nil )nil sigma "reals/" )"int" integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil product "reals/" )eq -decl nil product "reals/" )"real" product "reals/" )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )eq -decl nil integers nil )"real" bernstein_polynomials "reals/" )"[nat -> real]" multi_bernstein nil )eq -decl nil sigma "reals/" )eq -decl nil sigma "reals/" )"real" sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posrat" nil )"nat" product_nat "reals/" )"posreal" product_nat "reals/" )"posnat" product_nat "reals/" )"posint" nil )"posint" nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"nnreal" product_nat "reals/" )"real" multi_bernstein nil )"[nat -> [nat -> [nat -> posint]]]" nil )nil extra_real_propsnil )eq -decl nil real_types nil )1 skolem-const-decl "Vars" multi_bernstein nil )"DegreeMono" multi_bernstein nil )"CoeffMono" multi_bernstein nil )"posnat" multi_bernstein nil )"RealOrder" util nil )"(total_order?[real])" nil )"real" reals nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"real" multi_bernstein nil )nil bernstein_polynomials "reals/" )"bool" util nil )"nat" multi_bernstein nil )nil extra_real_propsnil )nil naturalnumbers nil )eq -decl nil defined_types nil )eq -decl nil naturalnumbers nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"bool" util nil )"[bool, bool -> bool]" booleans nil )"real" multi_bernstein nil )nil "reals/" )"real" multi_bernstein nil )eq -decl nil integers nil )nil multi_bernstein nil )eq -decl nil util nil )"bool" multi_bernstein nil ))nil ))0 1 nil 3499875835 "" (expand "Bern_coeffs_rel" )"" case "FORALL (a: real, bsdegmono: DegreeMono, bspoly: MultiBernstein, AND AND Bern_coeffs_rel_rec(bspoly, bsdegmono, cf, nvars, terms, v)") "1" (skeep)"1" (inst?)"1" (assert )"1" (skeep -1 )"1" (lemma "Bern_le" )"1" "anew" "bsdegmono" "bspoly" "cf" "nvars" "terms" )"1" (expand "Bern_coeffs_rel" )"1" (assert )"1" (expand "forall_X" )"1" (skosimp*)"1" (inst - "X!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" (expand "Bern_coeffs_rel_rec" )"1" "(multibscoeff(bspoly, bsdegmono, cf, nvars, terms)(cmo) + a)/2" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (skolem 1 "v" )"2" (flatten)"2" (skeep)"2" (expand "Bern_coeffs_rel_rec" (-3 1 ))"2" case "FORALL (d:nat): d<=bsdegmono(v) IMPLIES (EXISTS (anew: real):FORALL (gg:nat):gg<=d IMPLIES AND ") "1" (inst - "bsdegmono(v)" )"1" (assert )"1" (skeep -1 )"1" (inst + "anew" )"1" (assert )"1" case "anew < a" )"1" assert )"1" "1" "d!1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (induct "d" )"1" (assert )"1" (flatten)"1" "a" "bsdegmono" "bspoly" "cf" "nvars" "terms" "cmo WITH [(v):=0]" )"1" assert )"1" 4 "0" )"1" assert )"1" "1" "anew!1" )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skolem 1 "dd" )"2" (flatten)"2" (assert )"2" "2" "a" "bsdegmono" "bspoly" "cf" "nvars" "terms" "cmo WITH [(v):=dd+1]" )"2" assert )"2" 5 "dd+1" )"2" assert )"2" "2" "max(anew!1,anew!2)" )"2" "2" "1" "0" )"1" assert )"1" "1" expand "max" )"1" if )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "gg!1 = 1+dd" )"1" assert )"1" replace -1 )"1" "Bern_coeffs_rel_implic" )"1" "1" "anew!2" )"1" assert )"1" 1 )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "gg!1" )"2" assert )"2" "2" "Bern_coeffs_rel_implic" )"2" "2" "anew!1" )"2" assert )"2" 1 )"2" 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 )"bool" reals nil )"bool" multi_bernstein nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )eq -decl nil util nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil util nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl 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 )eq -decl nil util nil )"bool" multi_bernstein nil )nil multi_bernstein nil )"RealOrder" util nil )"(strict_total_order?[real])" real_props nil )"RealOrder" util nil )"(total_order?[real])" nil )eq -decl nil defined_types nil )nil naturalnumbers nil )"real" reals nil )eq -decl nil number_fields nil )"boolean" notequal nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" multi_bernstein nil )"real" reals nil )"posint" nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )nil multi_bernstein nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"posint" nil )eq -decl nil naturalnumbers nil )"bool" multi_bernstein nil ))nil ))0 1 nil 3499875940 "" (skeep)"" (rewrite "Bern_coeffs_rel_def" )"" (expand "forall_X" )"" (skosimp*)"" (rewrite "multibs_eval_equiv" )"" (name "cfnew" "LAMBDA (i:nat): a/(terms)" )"" (name "bspolynew" "LAMBDA(i:nat)(j:nat)(k:nat): 1" )"" case "multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, nvars) LAMBDA (i: nat): 0 )(X!1 ) >= multibs_eval_rec(bspolynew, bsdegmono, cfnew, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X!1 ) AND multibs_eval_rec(bspolynew, bsdegmono, cfnew, nvars, terms, nvars)LAMBDA (i: nat): 0 )(X!1 ) =a") "1" (flatten) (("1" (assert ) nil nil )) nil )"2" (hide 2 )"2" (split)"1" case "FORALL (cmo:CoeffMono,v:nat): v<=nvars AND le_below_mono?(nvars)(cmo,bsdegmono) IMPLIES multibs_eval_rec(bspoly, bsdegmono, cf, nvars, terms, v) 1 )1 )") "1" (inst?)"1" (assert )"1" (hide-all-but 1 )"1" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2 )"2" (induct "v" )"1" (skeep)"1" expand "multibs_eval_rec" +)"1" case "product(0, nvars - 1, LAMBDA (k: nat):IF cmo(k) <= bsdegmono(k)1 (k))1 0 ") "1" case "multibs_eval_mono(bspoly, bsdegmono, cf, nvars, terms)(cmo) ") "1" 1 "product(0, nvars - 1, LAMBDA (k: nat):IF cmo(k) <= bsdegmono(k)1 (k))1 ") "1" 2 )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" 2 )"2" 1 )"2" expand "multibs_eval_mono" )"2" expand "bspolynew" +)"2" expand "cfnew" +)"2" expand "multibscoeff" )"2" "cmo" )"2" assert )"2" case "FORALL (j:nat): j<terms IMPLIES sigma(0, j, LAMBDA (i: nat):0 , nvars - 1 , LAMBDA (j: nat): 1 )) = a*((j+1 )/(terms))") "1" "terms-1" )"1" assert )nil nil ))nil )"2" 2 )"2" case "FORALL (kr:nat): product(0,kr,LAMBDA (j:nat): 1) = 1" )"1" "j" )"1" assert )"1" expand "sigma" "1" expand "sigma" "1" "nvars-1" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" 1 "j" )"2" "2" assert )"2" expand "sigma" "2" replace 1 )"2" "nvars-1" )"2" replace 3 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" "kr" )"1" expand "product" )"1" expand "product" )"1" nil nil ))nil ))nil )"2" 1 "kr" )"2" "2" expand "product" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 2 )"2" case "FORALL (kr:nat): kr<=nvars-1 IMPLIES product(0, kr, LAMBDA (k: nat):IF cmo(k) <= bsdegmono(k)1 (k))1 0 ") "1" "nvars-1" )"1" (assert ) nil nil ))nil )"2" 2 )"2" "kr" )"1" "1" expand "product" )"1" expand "product" )"1" if )"1" "1" "Bern_nonnegative" )"1" "X!1(0)" )"1" "1"
Messung V0.5 in Prozent C=100 H=95 G=97
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.1.94Bemerkung:
(vorverarbeitet am 2026-09-29)
¤ *Bot Zugriff
2026-10-10
Neuigkeiten Aktuelles Motto des Tages Open Source Software
Jenseits des Üblichen ....
Besucherstatistik
Statistik #Sources=1126864 #Domains=1897691
