|
(bernstein_polynomials
(Bern_TCC1 0
(Bern_TCC1-1 nil 3479200111 ("" (subtype-tcc) nil nil) nil nil))
(Bern_TCC2 0
(Bern_TCC2-1 nil 3479200111 ("" (subtype-tcc) nil nil) nil nil))
(Bern_TCC3 0
(Bern_TCC3-1 nil 3479200111 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Bern_TCC4 0
(Bern_TCC4-1 nil 3479200335 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Bern_top_TCC1 0
(Bern_top_TCC1-1 nil 3479206792 ("" (subtype-tcc) nil nil) nil nil))
(Bern_top 0
(Bern_top-1 nil 3479206793
("" (skeep)
(("" (expand "Bern")
(("" (expand "C")
(("" (expand "^" 1 1)
(("" (expand "expt") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((Bern const-decl "real" bernstein_polynomials nil)
(^ const-decl "real" exponentiation nil)
(factorial_0 formula-decl nil factorial "ints/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(expt def-decl "real" exponentiation nil)
(C const-decl "posnat" binomial nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(Bern_bottom_TCC1 0
(Bern_bottom_TCC1-1 nil 3479206860 ("" (subtype-tcc) nil nil) nil
nil))
(Bern_bottom_TCC2 0
(Bern_bottom_TCC2-1 nil 3479206860 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(Bern_bottom 0
(Bern_bottom-1 nil 3479206860
("" (skeep)
(("" (expand "Bern")
(("" (expand "C")
(("" (expand "^" 1 2)
(("" (expand "expt") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((Bern const-decl "real" bernstein_polynomials nil)
(^ const-decl "real" exponentiation nil)
(factorial_0 formula-decl nil factorial "ints/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(expt def-decl "real" exponentiation nil)
(C const-decl "posnat" binomial nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil))
shostak))
(Bern_middle_zero 0
(Bern_middle_zero-1 nil 3480419658
("" (skeep)
(("" (expand "Bern")
(("" (case "0^i = 0")
(("1" (assert) nil nil)
("2" (expand "^" 1)
(("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((Bern const-decl "real" bernstein_polynomials nil)
(nat_expt application-judgement "nat" exponentiation nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(expt def-decl "real" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nat_exp application-judgement "nat" exponentiation nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(Bern_middle_one 0
(Bern_middle_one-1 nil 3480419912
("" (skeep)
(("" (expand "Bern")
(("" (case "0^(nn-i) = 0")
(("1" (assert) nil nil)
("2" (expand "^" 1)
(("2" (expand "expt" 1) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((Bern const-decl "real" bernstein_polynomials nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(nat_expt application-judgement "nat" exponentiation nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(expt def-decl "real" exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nat_exp application-judgement "nat" exponentiation nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real nonempty-type-from-decl nil reals nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil))
shostak))
(Bern_Polynomial_TCC1 0
(Bern_Polynomial_TCC1-1 nil 3479653703 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(above nonempty-type-eq-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(Bern_Polynomial_TCC2 0
(Bern_Polynomial_TCC2-1 nil 3479653703 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(above nonempty-type-eq-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(Bern_Polynomial 0
(Bern_Polynomial-1 nil 3479653689
("" (skeep)
(("" (decompose-equality)
(("1" (expand "Bern")
(("1" (lemma "neg_power_polynomial")
(("1"
(case "FORALL (n: nat):
(LAMBDA (x: real): (1 - x) ^ n) = polynomial(neg_power_fs(n), n)")
(("1" (hide -2)
(("1" (case "nn>=i")
(("1" (inst - "nn-i")
(("1" (decompose-equality)
(("1" (inst - "x!1")
(("1" (replace -1)
(("1" (hide -1)
(("1" (expand "polynomial")
(("1" (rewrite "sigma_scal" :dir rl)
(("1"
(name
"Bfun"
"LAMBDA (i_1: nat):
neg_power_fs(nn - i)(i_1) * C(nn, i) * x!1 ^ i *
(IF i_1 = 0 THEN 1 ELSE x!1 ^ i_1 ENDIF)")
(("1"
(replace -1)
(("1"
(name
"Afun"
"LAMBDA (i_1: nat):
IF i_1 < i OR i_1 > nn THEN 0
ELSE C(i_1, i) * C(nn, i_1) * (-1) ^ (i_1 - i)
ENDIF
* (IF i_1 = 0 THEN 1 ELSE x!1 ^ i_1 ENDIF)")
(("1"
(replace -1)
(("1"
(lemma "sigma_shift_T2")
(("1"
(inst
-
"lambda (iz:nat):IF iz < i THEN 0 ELSE Bfun(iz-i) ENDIF"
"nn-i"
"0"
"i")
(("1"
(assert)
(("1"
(case
"(LAMBDA (i_1: nat): Bfun(i_1)) = Bfun")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace
-1
:dir
rl)
(("1"
(hide -1)
(("1"
(lemma
"sigma_split")
(("1"
(inst
-
"Afun"
"nn"
"0"
"i-1")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(name
"Bfun2"
"LAMBDA (iz: nat): IF iz < i THEN 0 ELSE Bfun(iz - i) ENDIF")
(("1"
(replace
-1)
(("1"
(case
"sigma(0,i-1,Afun) = 0")
(("1"
(replace
-1)
(("1"
(lemma
"sigma_restrict_eq")
(("1"
(inst
-
"Bfun2"
"Afun"
"nn"
"i")
(("1"
(assert)
(("1"
(hide
2)
(("1"
(expand
"restrict")
(("1"
(decompose-equality
+)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(replace
-3
:dir
rl)
(("1"
(replace
-4
:dir
rl)
(("1"
(replace
-2
:dir
rl)
(("1"
(assert)
(("1"
(lift-if)
(("1"
(lift-if)
(("1"
(assert)
(("1"
(ground)
(("1"
(replace
-1)
(("1"
(case
"i = 0")
(("1"
(replace
-1)
(("1"
(assert)
(("1"
(expand
"neg_power_fs")
(("1"
(expand
"C")
(("1"
(assert)
(("1"
(expand
"^")
(("1"
(expand
"expt")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(replace
-1)
(("2"
(case
"x!2 = i")
(("1"
(replace
-1)
(("1"
(expand
"neg_power_fs")
(("1"
(expand
"C")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("3"
(expand
"neg_power_fs")
(("3"
(expand
"C")
(("3"
(hide
-)
(("3"
(lemma
"expt_plus")
(("3"
(inst
-
"x!2-i"
"i"
"x!1")
(("1"
(assert)
nil
nil)
("2"
(flatten)
(("2"
(replace
-1)
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"sigma_zero")
(("2"
(inst
-
"i-1"
"0")
(("2"
(lemma
"sigma_restrict_eq")
(("2"
(inst
-
"(LAMBDA (i: nat): 0)"
"Afun"
"i-1"
"0")
(("2"
(assert)
(("2"
(hide
(2
3))
(("2"
(decompose-equality
+)
(("2"
(expand
"restrict")
(("2"
(lift-if)
(("2"
(ground)
(("2"
(replace
-3
:dir
rl)
(("2"
(assert)
(("2"
(lift-if)
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skeep)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(decompose-equality +)
nil
nil))
nil))
nil)
("2"
(skeep)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(skeep)
(("2" (assert) nil nil))
nil)
("3"
(skeep)
(("3" (assert) 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" (case "n>0")
(("1" (inst - "n") nil nil)
("2" (case "n = 0")
(("1" (replace -1)
(("1" (hide-all-but 2)
(("1" (decompose-equality +)
(("1" (expand "^")
(("1" (expand "expt")
(("1"
(expand "polynomial")
(("1"
(expand "sigma")
(("1"
(assert)
(("1"
(expand "neg_power_fs")
(("1"
(expand "C")
(("1"
(assert)
(("1"
(expand "^")
(("1"
(expand "expt")
(("1" (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))
nil))
nil)
("2" (skeep) (("2" (assert) nil nil)) nil)
("3" (skeep) (("3" (assert) nil nil)) nil))
nil))
nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(<= const-decl "bool" reals nil)
(nn skolem-const-decl "above(i - 1)" bernstein_polynomials nil)
(above nonempty-type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" reals nil)
(i skolem-const-decl "nat" bernstein_polynomials nil)
(< const-decl "bool" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(Bern const-decl "real" bernstein_polynomials nil)
(sequence type-eq-decl nil sequences nil)
(polynomial const-decl "[real -> real]" polynomials nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(C const-decl "posnat" binomial nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(neg_power_polynomial formula-decl nil polynomials nil)
(n skolem-const-decl "nat" bernstein_polynomials nil)
(T_low type-eq-decl nil sigma nil)
(T_high type-eq-decl nil sigma nil)
(sigma_scal formula-decl nil sigma nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma def-decl "real" sigma nil)
(sigma_restrict_eq formula-decl nil sigma nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(restrict const-decl "[T -> real]" sigma nil)
(x!1 skolem-const-decl "real" bernstein_polynomials nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(expt_plus formula-decl nil exponentiation nil)
(factorial_0 formula-decl nil factorial "ints/")
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(expt def-decl "real" exponentiation nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(even_minus_even_is_even application-judgement "even_int" integers
nil)
(int_exp application-judgement "int" exponentiation nil)
(sigma_0_neg formula-decl nil sigma_nat nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(sigma_nnreal application-judgement "nnreal" sigma_nat nil)
(sigma_nat application-judgement "nat" sigma_nat nil)
(sigma_zero formula-decl nil sigma nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(sigma_split formula-decl nil sigma nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(sigma_shift_T2 formula-decl nil sigma nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(rat_exp application-judgement "rat" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(neg_power_fs const-decl "[nat -> int]" polynomials nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(Bernstein_Recursion_TCC1 0
(Bernstein_Recursion_TCC1-1 nil 3479211177 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Bernstein_Recursion_TCC2 0
(Bernstein_Recursion_TCC2-1 nil 3479211177 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Bernstein_Recursion_TCC3 0
(Bernstein_Recursion_TCC3-1 nil 3479211177 ("" (subtype-tcc) nil nil)
nil nil))
(Bernstein_Recursion_TCC4 0
(Bernstein_Recursion_TCC4-1 nil 3479211177 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(Bernstein_Recursion 0
(Bernstein_Recursion-1 nil 3479211177
("" (skeep)
(("" (case "C(k,r) = C(k-1,r) + C(k-1,r-1)")
(("1" (mult-by -1 "x^r*(1-x)^(k-r)")
(("1" (expand "Bern")
(("1" (case "x^r = x^(r-1)*x")
(("1" (case "(1-x)^(k-r) = (1-x)*(1-x)^(k-r-1)")
(("1" (assert) nil nil)
("2" (expand "^" 1)
(("2" (assert)
(("2" (expand "expt" 1 1) (("2" (assert) nil nil))
nil))
nil))
nil)
("3" (assert) nil nil))
nil)
("2" (expand "^" 1)
(("2" (expand "expt" 1 1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "C_n_plus_1")
(("2" (inst - "k-1" "r") (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (assert) nil nil) ("4" (assert) nil nil)
("5" (assert) nil nil))
nil))
nil)
((- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(C const-decl "posnat" binomial nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Bern const-decl "real" bernstein_polynomials nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(expt def-decl "real" exponentiation nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(x skolem-const-decl "real" bernstein_polynomials nil)
(k skolem-const-decl "posnat" bernstein_polynomials nil)
(r skolem-const-decl "posnat" bernstein_polynomials nil)
(^ const-decl "real" exponentiation nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times1_imp formula-decl nil extra_real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(C_n_plus_1 formula-decl nil binomial nil))
shostak))
(Bern_nonnegative 0
(Bern_nonnegative-1 nil 3479211589
("" (skeep)
(("" (skeep)
(("" (expand "Bern")
(("" (typepred "C(nn,i)")
(("" (lemma "nnreal_expt")
(("" (inst-cp - "i" "x")
(("1" (inst - "nn-i" "1-x")
(("1" (expand "^")
(("1" (assert)
(("1" (lemma "nnreal_times_nnreal_is_nnreal")
(("1" (inst?)
(("1" (lemma "nnreal_times_nnreal_is_nnreal")
(("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((above nonempty-type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(C const-decl "posnat" binomial nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x skolem-const-decl "real" bernstein_polynomials nil)
(nnreal type-eq-decl nil real_types nil)
(^ const-decl "real" exponentiation nil)
(nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil)
(nn skolem-const-decl "above(i - 1)" bernstein_polynomials nil)
(i skolem-const-decl "nat" bernstein_polynomials nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(expt def-decl "real" exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_expt judgement-tcc nil exponentiation nil)
(Bern const-decl "real" bernstein_polynomials nil))
shostak))
(Bern_positive 0
(Bern_positive-1 nil 3479211969
("" (skeep)
(("" (skeep)
(("" (expand "Bern")
(("" (typepred "C(nn,i)")
(("" (lemma "posreal_expt")
(("" (inst-cp - "i" "x")
(("1" (inst - "nn-i" "1-x")
(("1" (expand "^")
(("1" (assert)
(("1" (lemma "posreal_times_posreal_is_posreal")
(("1" (inst?)
(("1"
(case "C(nn, i) * expt((1 - x), (nn - i)) > 0")
(("1" (assert) nil nil)
("2" (hide 2)
(("2"
(lemma
"posreal_times_posreal_is_posreal")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((above nonempty-type-eq-decl nil integers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(C const-decl "posnat" binomial nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(> const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(x skolem-const-decl "real" bernstein_polynomials nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(^ const-decl "real" exponentiation nil)
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(nn skolem-const-decl "above(i - 1)" bernstein_polynomials nil)
(i skolem-const-decl "nat" bernstein_polynomials nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(expt def-decl "real" exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_expt judgement-tcc nil exponentiation nil)
(Bern const-decl "real" bernstein_polynomials nil))
nil))
(Bernstein_degree_raise_TCC1 0
(Bernstein_degree_raise_TCC1-1 nil 3479477346
("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.47 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
