|
(sum
(IMP_sigma_TCC1 0
(IMP_sigma_TCC1-1 nil 3393219168 ("" (assuming-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)
(integer nonempty-type-from-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sum_lemma2_TCC1 0
(sum_lemma2_TCC1-1 nil 3393219168 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posnat_expt application-judgement "posnat" exponentiation nil))
nil))
(sum_lemma2_TCC2 0
(sum_lemma2_TCC2-1 nil 3393219168 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posnat_expt application-judgement "posnat" exponentiation nil))
nil))
(sum_lemma2 0
(sum_lemma2-1 nil 3250069472
("" (induct "n1")
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (inst - "0")
(("1" (expand "cauchy_prop")
(("1" (inst - "p!1")
(("1" (expand "cauchys_to_reals")
(("1" (flatten)
(("1" (rewrite "expt_inverse")
(("1" (rewrite "div_mult_pos_lt2" 1)
(("1"
(lemma "abs_mult"
("x"
"xs!1(0) - cxs!1(0)(p!1) * (1 / (2 ^ p!1))"
"y" "2 ^ p!1"))
(("1" (expand "abs" -1 3)
(("1" (hide -1)
(("1" (assert)
(("1"
(expand "sigma")
(("1"
(lemma
"abs_mult"
("x"
"xs!1(0) - cxs!1(0)(p!1) * (1 / (2 ^ p!1))"
"y"
"2^p!1"))
(("1"
(expand "abs" -1 3)
(("1"
(replace -1 1 rl)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(rewrite
"associative_mult"
:dir
rl)
(("1"
(rewrite "inverse_mult")
(("1"
(assert)
(("1"
(name-replace
"XP"
"xs!1(0) * 2 ^ p!1")
(("1"
(grind)
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" (skosimp*)
(("2" (inst - "cxs!1" "_" "xs!1")
(("2" (replace -2 -1)
(("2" (expand "sigma" 1)
(("2" (inst - "p!1")
(("2" (name-replace "SS" "sigma(0, j!1, xs!1)")
(("2"
(name-replace "CS"
"sigma(0, j!1, cauchys_to_reals(cxs!1, p!1))")
(("2" (expand "cauchys_to_reals")
(("2"
(lemma "triangle"
("x" "SS-CS" "y"
"xs!1(1 + j!1) - cxs!1(1 + j!1)(p!1) * 2 ^ -p!1"))
(("2"
(case "abs(xs!1(1 + j!1) - cxs!1(1 + j!1)(p!1) * 2 ^ -p!1)<=2^-p!1")
(("1" (assert) nil nil)
("2" (hide -1 -2 2)
(("2" (expand "cauchy_prop")
(("2" (inst - "1+j!1")
(("2"
(inst - "p!1")
(("2"
(flatten)
(("2"
(rewrite "expt_inverse")
(("2"
(rewrite "div_mult_pos_le2" 1)
(("2"
(lemma
"abs_mult"
("x"
"xs!1(1 + j!1) - cxs!1(1 + j!1)(p!1) * (1 / (2 ^ p!1))"
"y"
"2 ^ p!1"))
(("2"
(expand "abs" -1 3)
(("2"
(replace -1 1 rl)
(("2"
(expand "<=" 1)
(("2"
(flatten)
(("2"
(rewrite
"abs_interval")
(("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)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(triangle formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(abs_interval formula-decl nil power nil)
(posrat_plus_nnrat_is_posrat application-judgement "posrat"
rationals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(inverse_mult formula-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(associative_mult formula-decl nil number_fields nil)
(abs_mult formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_inverse formula-decl nil exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nat_induction formula-decl nil naturalnumbers nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cauchys_to_reals const-decl "[nat -> real]" sum nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(cauchy_prop const-decl "bool" cauchy nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? const-decl "bool" cauchy nil)
(pred type-eq-decl nil defined_types 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)
(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)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_int_is_int application-judgement "int" integers nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(cauchy_sum_aux_TCC1 0
(cauchy_sum_aux_TCC1-1 nil 3251267870 ("" (grind) 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(cauchy_sum_aux_TCC2 0
(cauchy_sum_aux_TCC2-1 nil 3251267870 ("" (grind) nil nil) nil
shostak))
(sum_lemma3_TCC1 0
(sum_lemma3_TCC1-1 nil 3393219168 ("" (subtype-tcc) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sum_lemma3_TCC2 0
(sum_lemma3_TCC2-1 nil 3393219168 ("" (subtype-tcc) nil nil) nil
nil))
(sum_lemma3 0
(sum_lemma3-1 nil 3250069472
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "cauchy_sum_aux")
(("1" (expand "cauchys_to_reals")
(("1" (expand "sigma")
(("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "cauchy_sum_aux" 1)
(("2" (expand "sigma" 1)
(("2" (inst - "cxs!1" "p!1")
(("2"
(name-replace "AA"
"cauchy_sum_aux(cxs!1, j!1, p!1) * 2 ^ -p!1")
(("2"
(name-replace "B"
"sigma(0,j!1,cauchys_to_reals(cxs!1, p!1))")
(("2" (expand "cauchys_to_reals")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((rat nonempty-type-eq-decl nil rationals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(nat_induction formula-decl nil naturalnumbers nil)
(cauchys_to_reals const-decl "[nat -> real]" sum nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(cauchy_sum_aux def-decl "int" sum nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? const-decl "bool" cauchy nil)
(pred type-eq-decl nil defined_types 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)
(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)
(minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sum_lemma4_TCC1 0
(sum_lemma4_TCC1-1 nil 3393620691
("" (skosimp)
(("" (expand "log2")
(("" (lemma "ln_strict_increasing")
(("" (expand "strict_increasing?")
(("" (inst-cp - "1" "2")
(("" (inst - "1" "1+n!1")
(("" (rewrite "ln_1")
(("" (assert)
(("" (case-replace "n!1=0")
(("1" (assert)
(("1" (rewrite "floor_int" 1)
(("1" (assert) nil nil)) nil))
nil)
("2" (assert)
(("2"
(lemma "posreal_div_posreal_is_posreal"
("px" "ln(1+n!1)" "py" "ln(2)"))
(("2" (typepred "floor(ln(1 + n!1) / ln(2))")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((log2 const-decl "real" prelude_aux nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(real_le_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)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(floor_int formula-decl nil floor_ceil nil)
(integer nonempty-type-from-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(ln const-decl "real" ln_exp "lnexp_fnd/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(ln_1 formula-decl nil ln_exp "lnexp_fnd/")
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/"))
nil))
(sum_lemma4 0
(sum_lemma4-1 nil 3250069472
("" (skosimp)
((""
(lemma "sum_lemma3"
("cxs" "cxs!1" "n" "n!1" "p" "p!1 + floor(log2(n!1 + 1)) + 2"))
(("1" (replace -1 1 rl)
(("1" (hide -1)
(("1" (expand "cauchy_sum_type_int")
(("1" (rewrite "floor_log2_def")
(("1"
(name-replace "AA"
"cauchy_sum_aux(cxs!1, n!1, 2 + floor(log2(1 + n!1)) + p!1)")
(("1"
(lemma "expt_inverse"
("n0x" "2" "i" "2 + floor(log2(1 + n!1))"))
(("1"
(lemma "expt_plus"
("n0x" "2" "i" "-(2 + floor(log2(1 + n!1)))" "j"
"-p!1"))
(("1" (replace -1)
(("1" (replace -2)
(("1"
(name-replace "B"
"2 ^ (2 + floor(log2(1 + n!1)))")
(("1"
(lemma "abs_mult"
("x" "AA/B - round(AA/B)" "y" "2 ^ -p!1"))
(("1" (replace -1 1)
(("1"
(hide -1 -2 -3)
(("1"
(name-replace "C" "AA/B")
(("1"
(lemma
"abs_interval2"
("x" "C - round(C)" "a" "1/2"))
(("1"
(lemma
"lemma_A2_generalized"
("r" "round(C)" "x" "C"))
(("1"
(assert)
(("1"
(flatten -1)
(("1"
(assert)
(("1"
(expand "abs" 1 2)
(("1"
(lemma
"expt_plus"
("n0x"
"2"
"i"
"-1"
"j"
"-p!1"))
(("1"
(lemma
"both_sides_times_pos_le1"
("x"
"abs(C - round(C))"
"y"
"1 / 2"
"pz"
"2 ^ -p!1"))
(("1"
(expand "^" -2 2)
(("1"
(expand
"expt"
-2)
(("1"
(expand
"expt"
-2)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "sum_lemma4_TCC1")
(("2" (inst - "n!1" "p!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((log2 const-decl "real" prelude_aux nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(integer nonempty-type-from-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? const-decl "bool" cauchy 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)
(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)
(sum_lemma3 formula-decl nil sum nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(floor_log2_def formula-decl nil appendix nil)
(expt_inverse formula-decl nil exponentiation nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(rat nonempty-type-eq-decl nil rationals nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}"
real_defs nil)
(lemma_A2_generalized formula-decl nil power nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(expt def-decl "real" exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(abs_interval2 formula-decl nil power nil)
(round const-decl "int" prelude_aux nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs_mult formula-decl nil real_props nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(expt_plus formula-decl nil exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(cauchy_sum_aux def-decl "int" sum nil)
(cauchy_sum_type_int const-decl "int" sum nil)
(posint_exp application-judgement "posint" exponentiation nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sum_lemma4_TCC1 subtype-tcc nil sum nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil))
nil))
(sum_lemma5 0
(sum_lemma5-1 nil 3250069472
("" (skosimp*)
(("" (lemma "sum_lemma2" ("xs" "xs!1" "n1" "n1!1" "cxs" "cxs!1"))
(("" (replace -2 -1)
(("" (lemma "sum_lemma4" ("cxs" "cxs!1" "n" "n1!1" "p" "p!1"))
(("" (case "floor(log2(n1!1 + 1))>=0")
(("1" (inst - "p!1 + floor(log2(n1!1 + 1)) + 2")
(("1" (name "AA" "sigma(0,n1!1,xs!1)")
(("1" (replace -1)
(("1"
(name "B" "cauchy_sum_type_int(cxs!1, n1!1, p!1)")
(("1" (replace -1)
(("1"
(name "C"
"sigma(0,n1!1,cauchys_to_reals(cxs!1,2+floor(log2(1+n1!1)) +
p!1))")
(("1"
(lemma "expt_inverse" ("n0x" "2" "i" "p!1"))
(("1" (replace -1)
(("1" (name "D" "B / 2 ^ p!1")
(("1"
(replace -1)
(("1"
(replace -3)
(("1"
(lemma
"triangle"
("x" "AA-C" "y" "C-D"))
(("1"
(case
"2 ^ -(p!1 + 1)+(n1!1 + 1) * 2 ^ -(p!1 + floor(log2(n1!1 + 1)) + 2)<= 1 / (2 ^ p!1)")
(("1" (assert) nil nil)
("2"
(hide
-1
-2
-3
-4
-5
-6
-8
-9
-10
2)
(("2"
(lemma
"lemma_A3"
("i"
"floor(log2(1 + n1!1))"
"px"
"1 + n1!1"))
(("2"
(simplify -1)
(("2"
(flatten -1)
(("2"
(hide -1)
(("2"
(lemma
"both_sides_times_pos_lt1"
("x"
"1 + n1!1"
"y"
"2 ^ (1 + floor(log2(1 + n1!1)))"
"pz"
"2 ^ -(p!1 + floor(log2(n1!1 + 1)) + 2)"))
(("2"
(replace -1 -2 rl)
(("2"
(hide -1)
(("2"
(lemma
"expt_plus"
("n0x"
"2"
"i"
"1 + floor(log2(1 + n1!1))"
"j"
"-(p!1 + floor(log2(n1!1 + 1)) + 2)"))
(("2"
(replace
-1
-2
rl)
(("2"
(hide -1)
(("2"
(name-replace
"FLOOR"
"floor(log2(n1!1 + 1))")
(("2"
(name-replace
"LHS"
"(1 + n1!1) * 2 ^ -(p!1 + FLOOR + 2)")
(("2"
(case-replace
"1 + FLOOR + -(p!1 + FLOOR + 2)= -(p!1+1)")
(("1"
(hide
-1
-3)
(("1"
(rewrite
"expt_inverse")
(("1"
(rewrite
"expt_plus")
(("1"
(rewrite
"expt_x1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (hide-all-but 1)
(("2"
(lemma "nonneg_floor_is_nat" ("x" "log2(n1!1 + 1)"))
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "log2")
(("2" (lemma "ln_strict_increasing")
(("2" (expand "strict_increasing?")
(("2" (inst - "1" "1+n1!1")
(("2" (case-replace "n1!1=0")
(("1" (rewrite "ln_1")
(("1" (assert) nil nil)) nil)
("2"
(lemma "both_sides_div_pos_lt1"
("x" "0" "y" "ln(1+n1!1)" "pz" "ln(2)"))
(("1"
(rewrite "ln_1")
(("1" (assert) nil nil))
nil)
("2"
(lemma "ln_strict_increasing")
(("2"
(expand "strict_increasing?")
(("2"
(inst - "1" "2")
(("2"
(rewrite "ln_1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? const-decl "bool" cauchy 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)
(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)
(sum_lemma2 formula-decl nil sum nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(sum_lemma4 formula-decl nil sum nil)
(ln_strict_increasing formula-decl nil ln_exp "lnexp_fnd/")
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(ln const-decl "real" ln_exp "lnexp_fnd/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ln_1 formula-decl nil ln_exp "lnexp_fnd/")
(real_div_nzreal_is_real application-judgement "real" reals nil)
(strict_increasing? const-decl "bool" real_fun_preds "reals/")
(nonneg_floor_is_nat judgement-tcc nil floor_ceil nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(n1!1 skolem-const-decl "nat" sum nil)
(p!1 skolem-const-decl "nat" sum nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(expt_inverse formula-decl nil exponentiation nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(rat nonempty-type-eq-decl nil rationals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_int_is_int application-judgement "int" integers nil)
(posrat_plus_nnrat_is_posrat application-judgement "posrat"
rationals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(lemma_A3 formula-decl nil appendix nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals nil)
(expt_x1 formula-decl nil exponentiation nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(expt_plus formula-decl nil exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(triangle formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_exp application-judgement "posint" exponentiation nil)
(cauchys_to_reals const-decl "[nat -> real]" sum nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(cauchy_sum_type_int const-decl "int" sum nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(integer nonempty-type-from-decl nil integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(log2 const-decl "real" prelude_aux nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil))
nil))
(cauchys_real_TCC1 0
(cauchys_real_TCC1-1 nil 3250069472
("" (expand "cauchy_real?")
(("" (inst + "0")
(("" (expand "cauchy_prop") (("" (propax) nil nil)) nil)) nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil)
(cauchy_real? const-decl "bool" cauchy nil))
nil))
(cauchys_real_TCC2 0
(cauchys_real_TCC2-1 nil 3250069472
("" (expand "cauchys_real?")
(("" (inst + "LAMBDA n: 0")
(("" (expand "cauchys_prop")
(("" (skolem!)
(("" (expand "cauchy_prop") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil)
(cauchys_prop const-decl "bool" sum nil)
(cauchys_real? const-decl "bool" sum nil))
nil))
(cauchy_sum_TCC1 0
(cauchy_sum_TCC1-1 nil 3250069472
("" (skosimp*)
(("" (typepred "cxs!1")
(("" (expand "cauchys_real?")
(("" (skosimp)
(("" (expand "cauchy_real?")
(("" (inst + "sigma(0,n!1,xs!1)")
(("" (expand "cauchy_prop")
(("" (skosimp)
((""
(lemma "sum_lemma5"
("cxs" "cxs!1" "xs" "xs!1" "n1" "n!1" "p" "p!1"))
(("" (split -1)
(("1" (hide -2)
(("1"
(name-replace "CS"
"cauchy_sum_type_int(cxs!1, n!1, p!1)")
(("1"
(name-replace "SS" "sigma(0, n!1, xs!1)")
(("1" (rewrite "expt_inverse")
(("1"
(lemma "expt_pos" ("px" "2" "i" "p!1"))
(("1"
(name-replace "P" "2 ^ p!1")
(("1"
(rewrite "div_mult_pos_lt2" -2)
(("1"
(lemma
"abs_mult"
("x" "SS-CS/P" "y" "P"))
(("1"
(expand "abs" -1 3)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "cauchys_prop")
(("2" (inst - "n!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cauchys_real nonempty-type-eq-decl nil sum nil)
(cauchys_real? const-decl "bool" sum nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? const-decl "bool" cauchy nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(cauchy_sum_type_int const-decl "int" sum nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(expt_inverse formula-decl nil exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(^ const-decl "real" exponentiation nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(abs_mult formula-decl nil 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_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(expt_pos formula-decl nil exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cauchys_prop const-decl "bool" sum nil)
(sum_lemma5 formula-decl nil sum nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(cauchy_prop const-decl "bool" cauchy nil)
(posint_exp application-judgement "posint" exponentiation nil))
nil))
(sum_lemma_TCC1 0
(sum_lemma_TCC1-1 nil 3250069472
("" (skosimp*)
(("" (expand "cauchys_real?")
(("" (inst + "xs!1")
(("" (expand "cauchys_prop") (("" (propax) nil nil)) nil))
nil))
nil))
nil)
((cauchys_real? const-decl "bool" sum nil)
(cauchys_prop const-decl "bool" sum 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)
(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))
nil))
(sum_lemma 0
(sum_lemma-1 nil 3250069472
("" (skosimp)
(("" (expand "cauchy_prop" 1)
(("" (skosimp)
((""
(lemma "sum_lemma5"
("xs" "xs!1" "cxs" "cxs!1" "n1" "m!1" "p" "p!1"))
(("" (replace -2 -1)
(("" (expand "cauchy_sum")
((""
(lemma "abs_interval1"
("x"
"sigma(0,m!1,xs!1) -cauchy_sum_type_int(cxs!1, m!1, p!1) * 2 ^ -p!1"
"a" "(2 ^ -p!1)"))
(("" (replace -2 -1)
(("" (simplify -1)
(("" (flatten)
(("" (name-replace "AA" "sigma(0,m!1,xs!1)")
((""
(name-replace "B"
"cauchy_sum_type_int(cxs!1,m!1,p!1)")
(("" (lemma "expt_pos" ("px" "2" "i" "p!1"))
(("" (rewrite "expt_inverse")
((""
(hide -4 -5)
((""
(rewrite "div_mult_pos_lt2" -3)
((""
(assert)
((""
(lemma
"div_mult_pos_lt1"
("py"
"2^p!1"
"x"
"AA"
"z"
"B-1"))
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_exp application-judgement "posint" exponentiation nil)
(cauchy_prop const-decl "bool" cauchy nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_real? const-decl "bool" cauchy 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)
(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)
(sum_lemma5 formula-decl nil sum nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(posrat_exp application-judgement "posrat" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(cauchy_sum const-decl "cauchy_real" sum nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_inverse formula-decl nil exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(real_times_real_is_real application-judgement "real" reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(expt_pos formula-decl nil exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(abs_interval1 formula-decl nil power nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(cauchy_sum_type_int const-decl "int" sum nil))
nil)))
¤ Dauer der Verarbeitung: 0.67 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.
|
