Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
exact_real_arith.summary
Sprache: Unknown
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[281] Hlasm[1767] Haskell[2105]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** top (20:51:52 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory prelude_aux
lt_times_lt_nn1.......................proved - complete [shostak](0.20 s)
lt_times_lt_np1.......................proved - complete [shostak](0.18 s)
both_sides_times_nonneg_le1...........proved - complete [shostak](0.07 s)
both_sides_times_nonpos_le1...........proved - complete [shostak](0.06 s)
abs_nonneg............................proved - complete [shostak](0.02 s)
abs_nonpos............................proved - complete [shostak](0.03 s)
odd_even..............................proved - complete [shostak](0.12 s)
odd_or_even...........................proved - complete [shostak](0.03 s)
expt_product_aux_TCC1.................proved - complete [shostak](0.02 s)
expt_product_aux_TCC2.................proved - complete [shostak](0.02 s)
expt_product_aux......................proved - complete [shostak](0.29 s)
expt_product_TCC1.....................proved - complete [shostak](0.02 s)
expt_product_TCC2.....................proved - complete [shostak](0.02 s)
expt_product..........................proved - complete [shostak](0.03 s)
expt_division_aux_TCC1................proved - complete [shostak](0.02 s)
expt_division_aux.....................proved - complete [shostak](0.02 s)
expt_division_TCC1....................proved - complete [shostak](0.02 s)
expt_division.........................proved - complete [shostak](0.32 s)
expt_minus1...........................proved - complete [shostak](-1.44 s)
lt_equiv_not_le.......................proved - complete [shostak](0.03 s)
le_equiv_not_lt.......................proved - complete [shostak](0.03 s)
lt_equiv_le_plus_one..................proved - complete [shostak](0.06 s)
lt_plus_one_equiv_le..................proved - complete [shostak](0.05 s)
lt_le_transitivity....................proved - complete [shostak](0.03 s)
le_lt_transitivity....................proved - complete [shostak](0.02 s)
exp_of2_exists_aux_TCC1...............proved - complete [shostak](0.03 s)
exp_of2_exists_aux....................proved - complete [shostak](0.95 s)
exp_of2_exists_TCC1...................proved - complete [shostak](0.03 s)
exp_of2_exists........................proved - complete [shostak](0.17 s)
exp_of_exists2........................proved - complete [shostak](0.33 s)
floor_sqrt_val........................proved - complete [shostak](0.16 s)
ceiling_sqrt_0........................proved - complete [shostak](0.03 s)
ceiling_sqrt_val......................proved - complete [shostak](0.17 s)
log2_TCC1.............................proved - incomplete [shostak](0.03 s)
log2_2_expt_i.........................proved - incomplete [shostak](0.23 s)
log2_strict_increasing................proved - incomplete [shostak](0.07 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (2.48 s)
Proof summary for theory prelude_A4
expt_neg_even_TCC1....................proved - complete [shostak](0.02 s)
expt_neg_even_TCC2....................proved - complete [shostak](0.02 s)
expt_neg_even.........................proved - complete [shostak](0.13 s)
expt_neg_odd_TCC1.....................proved - complete [shostak](0.05 s)
expt_neg_odd_TCC2.....................proved - complete [shostak](0.05 s)
expt_neg_odd..........................proved - complete [shostak](0.16 s)
expt_0pn..............................proved - complete [shostak](0.03 s)
expt_inverse_inv_TCC1.................proved - complete [shostak](0.02 s)
expt_inverse_inv......................proved - complete [shostak](0.06 s)
expt_product_n0i_TCC1.................proved - complete [shostak](0.02 s)
expt_product_n0i_TCC2.................proved - complete [shostak](0.03 s)
expt_product_n0i......................proved - complete [shostak](0.08 s)
expt_division_TCC1....................proved - complete [shostak](0.03 s)
expt_division_TCC2....................proved - complete [shostak](0.02 s)
expt_division.........................proved - complete [shostak](0.10 s)
A4_0_TCC1.............................proved - complete [shostak](0.06 s)
A4_0..................................proved - complete [shostak](0.10 s)
A4_1_TCC1.............................proved - complete [shostak](0.07 s)
A4_1..................................proved - complete [shostak](0.07 s)
A4_2..................................proved - complete [shostak](0.31 s)
A4_3_n................................proved - complete [shostak](0.13 s)
A4_3_0_TCC1...........................proved - complete [shostak](0.06 s)
A4_3_0................................proved - complete [shostak](0.13 s)
A4_3_p_TCC1...........................proved - complete [shostak](0.06 s)
A4_3_p................................proved - complete [shostak](0.10 s)
A4_4..................................proved - complete [shostak](0.56 s)
A4_5pp_TCC1...........................proved - complete [shostak](0.07 s)
A4_5pp................................proved - complete [shostak](1.17 s)
A4_5nn_TCC1...........................proved - complete [shostak](0.08 s)
A4_5nn................................proved - complete [shostak](1.43 s)
A4_5nn_general_TCC1...................proved - complete [shostak](0.06 s)
A4_5nn_general........................proved - complete [shostak](0.25 s)
A4_5_TCC1.............................proved - complete [shostak](0.06 s)
A4_5..................................proved - complete [shostak](0.46 s)
A4_6pp_TCC1...........................proved - complete [shostak](0.03 s)
A4_6pp................................proved - complete [shostak](1.17 s)
A4_6pp_general_TCC1...................proved - complete [shostak](0.04 s)
A4_6pp_general........................proved - complete [shostak](0.18 s)
A4_6nn_TCC1...........................proved - complete [shostak](0.03 s)
A4_6nn................................proved - complete [shostak](1.02 s)
A4_6nn_general_TCC1...................proved - complete [shostak](0.03 s)
A4_6nn_general........................proved - complete [shostak](0.18 s)
A4_sqrt_ineq1.........................proved - complete [shostak](0.06 s)
A4_sqrt_ineq2.........................proved - complete [shostak](0.16 s)
A4_sqrt_ineq3.........................proved - complete [shostak](0.16 s)
A4_logsize............................proved - complete [shostak](0.10 s)
A4_lemma_ineq1........................proved - complete [shostak](0.24 s)
A4_lemma_ineq2........................proved - complete [shostak](0.12 s)
A4_lemma_large_UB_0_TCC1..............proved - complete [shostak](0.09 s)
A4_lemma_large_UB_0...................proved - complete [shostak](0.93 s)
A4_lemma_large_UB_TCC1................proved - complete [shostak](0.12 s)
A4_lemma_large_UB.....................proved - complete [shostak](1.51 s)
A4_lemma_large_LB_TCC1................proved - complete [shostak](0.11 s)
A4_lemma_large_LB.....................proved - complete [shostak](1.41 s)
A4_lemma_large_ge3....................proved - complete [shostak](0.14 s)
A4_lemma_large_lt3_TCC1...............proved - complete [shostak](0.11 s)
A4_lemma_large_lt3_TCC2...............proved - complete [shostak](0.14 s)
A4_lemma_large_lt3....................proved - complete [shostak](0.84 s)
A4_lemma_small_UB_TCC1................proved - complete [shostak](0.10 s)
A4_lemma_small_UB.....................proved - complete [shostak](1.25 s)
A4_lemma_small_LB_TCC1................proved - complete [shostak](0.09 s)
A4_lemma_small_LB.....................proved - complete [shostak](0.90 s)
A4_lemma_small_TCC1...................proved - complete [shostak](0.08 s)
A4_lemma_small_TCC2...................proved - complete [shostak](0.14 s)
A4_lemma_small........................proved - complete [shostak](0.37 s)
A4_lemma_px_TCC1......................proved - complete [shostak](0.11 s)
A4_lemma_px_TCC2......................proved - complete [shostak](0.11 s)
A4_lemma_px...........................proved - complete [shostak](0.22 s)
A4_lemma_p............................proved - complete [shostak](0.22 s)
A4_lemma_0_px_TCC1....................proved - complete [shostak](0.06 s)
A4_lemma_0_px_TCC2....................proved - complete [shostak](0.06 s)
A4_lemma_0_px.........................proved - complete [shostak](0.27 s)
A4_lemma_0_p..........................proved - complete [shostak](0.56 s)
A4_lemma_0_TCC1.......................proved - complete [shostak](0.06 s)
A4_lemma_0_TCC2.......................proved - complete [shostak](0.07 s)
A4_lemma_0............................proved - complete [shostak](1.03 s)
A4_lemma_n_even_TCC1..................proved - complete [shostak](0.06 s)
A4_lemma_n_even_TCC2..................proved - complete [shostak](0.07 s)
A4_lemma_n_even.......................proved - complete [shostak](0.49 s)
A4_lemma_n_odd_TCC1...................proved - complete [shostak](0.07 s)
A4_lemma_n_odd_TCC2...................proved - complete [shostak](0.07 s)
A4_lemma_n_odd........................proved - complete [shostak](0.54 s)
A4_lemma_n_TCC1.......................proved - complete [shostak](0.06 s)
A4_lemma_n_TCC2.......................proved - complete [shostak](0.07 s)
A4_lemma_n............................proved - complete [shostak](0.59 s)
Theory totals: 85 formulas, 85 attempted, 85 succeeded (22.69 s)
Proof summary for theory appendix
lemma_A1..............................proved - complete [shostak](0.11 s)
lemma_A2..............................proved - complete [shostak](0.49 s)
lemma_A3..............................proved - incomplete [shostak](0.12 s)
lemma_A4_TCC1.........................proved - incomplete [shostak](0.12 s)
lemma_A4_TCC2.........................proved - incomplete [shostak](0.12 s)
lemma_A4_TCC3.........................proved - incomplete [shostak](0.12 s)
lemma_A4..............................proved - incomplete [shostak](0.68 s)
epsilon_log2_aux......................proved - complete [shostak](0.15 s)
epsilon_log2..........................proved - complete [shostak](0.08 s)
floor_sqrt_aux_TCC1...................proved - complete [shostak](0.13 s)
floor_sqrt_aux_TCC2...................proved - complete [shostak](0.18 s)
floor_sqrt_def........................proved - complete [shostak](1.53 s)
floor_log2_TCC1.......................proved - complete [shostak](0.05 s)
floor_log2_TCC2.......................proved - complete [shostak](0.05 s)
floor_log2_def........................proved - incomplete [shostak](2.12 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (6.04 s)
Proof summary for theory prelude_sqrt
square_le1............................proved - complete [shostak](0.17 s)
square_le2............................proved - complete [shostak](0.10 s)
square_le3............................proved - complete [shostak](0.08 s)
square_eq1............................proved - complete [shostak](0.07 s)
square_le4............................proved - complete [shostak](0.08 s)
square_le5............................proved - complete [shostak](0.17 s)
square_le6............................proved - complete [shostak](0.13 s)
square_archimedean1...................proved - complete [shostak](0.16 s)
square_archimedean2...................proved - complete [shostak](0.42 s)
square_exist_lt1......................proved - complete [shostak](0.69 s)
square_exist_lt2......................proved - complete [shostak](0.09 s)
square_exist_lt3......................proved - complete [shostak](0.24 s)
square_exist_gt3......................proved - complete [shostak](0.31 s)
sqrt_set_nonempty.....................proved - complete [shostak](0.03 s)
sqrt_set_has_UB_TCC1..................proved - complete [shostak](0.03 s)
sqrt_set_has_UB.......................proved - complete [shostak](0.14 s)
sqrt_set_LUB..........................proved - complete [shostak](0.30 s)
square_injective......................proved - complete [shostak](0.07 s)
square_surjective.....................proved - complete [shostak](0.12 s)
square_bijective......................proved - complete [shostak](0.02 s)
square_is.............................proved - complete [shostak](0.02 s)
sqrt_square1..........................proved - complete [shostak](0.03 s)
sqrt_square2..........................proved - complete [shostak](0.02 s)
square_times..........................proved - complete [shostak](0.04 s)
sqrt_times............................proved - complete [shostak](0.07 s)
sqrt_zero.............................proved - complete [shostak](0.07 s)
sqrt_one..............................proved - complete [shostak](0.07 s)
both_sides_sqrt1......................proved - complete [shostak](0.09 s)
both_sides_sqrt2......................proved - complete [shostak](-1.58 s)
both_sides_sqrt_lt1...................proved - complete [shostak](0.09 s)
both_sides_sqrt_lt2...................proved - complete [shostak](0.09 s)
both_sides_sqrt_lt3...................proved - complete [shostak](0.09 s)
both_sides_sqrt_le1...................proved - complete [shostak](0.10 s)
both_sides_sqrt_le2...................proved - complete [shostak](0.09 s)
both_sides_sqrt_le3...................proved - complete [shostak](0.10 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (2.80 s)
Proof summary for theory cauchy
cauchy_real_TCC1......................proved - complete [shostak](0.02 s)
cauchy_nzreal_TCC1....................proved - complete [shostak](0.03 s)
cauchy_nnreal_TCC1....................proved - complete [shostak](0.03 s)
cauchy_npreal_TCC1....................proved - complete [shostak](0.03 s)
cauchy_posreal_TCC1...................proved - complete [shostak](0.02 s)
cauchy_negreal_TCC1...................proved - complete [shostak](0.04 s)
cauchy_smallreal_TCC1.................proved - complete [shostak](0.03 s)
subtype_TCC1..........................proved - complete [shostak](0.02 s)
subtype_TCC2..........................proved - complete [shostak](0.03 s)
subtype_TCC3..........................proved - complete [shostak](0.02 s)
subtype_TCC4..........................proved - complete [shostak](0.03 s)
subtype_TCC5..........................proved - complete [shostak](0.02 s)
subtype_TCC6..........................proved - complete [shostak](0.03 s)
subtype_TCC7..........................proved - complete [shostak](0.03 s)
subtype_TCC8..........................proved - complete [shostak](0.02 s)
cauchy_zero_TCC1......................proved - complete [shostak](0.03 s)
unique_cauchy_zero....................proved - complete [shostak](0.25 s)
unique_cauchy_zero2...................proved - complete [shostak](0.07 s)
unique_cauchy_zero3...................proved - complete [shostak](0.03 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.78 s)
Proof summary for theory int
cauchy_int_TCC1.......................proved - complete [shostak](0.35 s)
cauchy_nat_TCC1.......................proved - complete [shostak](0.05 s)
int_lemma.............................proved - complete [shostak](0.03 s)
nat_lemma.............................proved - complete [shostak](0.05 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.48 s)
Proof summary for theory add
cauchy_add_TCC1.......................proved - complete [shostak](0.28 s)
add_lemma.............................proved - complete [shostak](0.24 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.52 s)
Proof summary for theory neg
cauchy_neg_TCC1.......................proved - complete [shostak](0.09 s)
neg_lemma.............................proved - complete [shostak](0.12 s)
neg_cauchy_nzreal_is_cauchy_nzreal....proved - complete [shostak](0.04 s)
neg_cauchy_posreal_is_cauchy_negreal...proved - complete [shostak](0.04 s)
neg_cauchy_negreal_is_cauchy_posreal...proved - complete [shostak](0.04 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.33 s)
Proof summary for theory sub
sub_lemma.............................proved - complete [shostak](0.04 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.04 s)
Proof summary for theory mul
D1....................................proved - complete [shostak](0.06 s)
D2....................................proved - complete [shostak](0.05 s)
D3....................................proved - complete [shostak](0.06 s)
negreal_times_posreal_is_negreal......proved - complete [shostak](0.08 s)
lt_times_lt_nonneg1...................proved - complete [shostak](0.13 s)
lt_times_lt_nonneg2...................proved - complete [shostak](0.16 s)
D_pp..................................proved - complete [shostak](0.49 s)
D_pn..................................proved - complete [shostak](0.46 s)
D_nn..................................proved - complete [shostak](1.27 s)
D_p0..................................proved - complete [shostak](0.16 s)
D_n0..................................proved - complete [shostak](0.49 s)
D.....................................proved - complete [shostak](0.65 s)
mul_p1................................proved - incomplete [shostak](0.28 s)
mul_p2................................proved - incomplete [shostak](1.04 s)
mul_p3................................proved - incomplete [shostak](0.24 s)
mul_p4................................proved - incomplete [shostak](0.42 s)
mul_p5................................proved - incomplete [shostak](2.23 s)
mul_p6................................proved - incomplete [shostak](0.68 s)
cauchy_mul_type_TCC1..................proved - incomplete [shostak](0.16 s)
cauchy_mul_type.......................proved - incomplete [shostak](0.77 s)
cauchy_mul_TCC1.......................proved - incomplete [shostak](0.28 s)
mul_lemma.............................proved - incomplete [shostak](0.89 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (11.08 s)
Proof summary for theory inv
expt_x2_TCC1..........................proved - complete [shostak](0.03 s)
expt_x2...............................proved - complete [shostak](0.02 s)
expt_times2_TCC1......................proved - complete [shostak](0.02 s)
expt_times2_TCC2......................proved - complete [shostak](0.02 s)
expt_times2...........................proved - complete [shostak](0.09 s)
minimum_inv_exists....................proved - complete [shostak](0.51 s)
minimum_inv_TCC1......................proved - complete [shostak](0.02 s)
minimum_inv_prop0.....................proved - complete [shostak](0.10 s)
minimum_inv_prop1.....................proved - complete [shostak](0.28 s)
minimum_inv_prop2.....................proved - complete [shostak](0.40 s)
minimum_inv_aux_TCC1..................proved - complete [shostak](0.04 s)
minimum_inv_aux_TCC2..................proved - complete [shostak](0.11 s)
minimum_inv_aux_TCC3..................proved - complete [shostak](0.14 s)
minimum_inv_impl_TCC1.................proved - complete [shostak](0.02 s)
minimum_inv_impl_def..................proved - complete [shostak](0.34 s)
inv_p0................................proved - complete [shostak](0.11 s)
inv_p1................................proved - complete [shostak](0.35 s)
inv_p2................................proved - complete [shostak](0.23 s)
inv_p3................................proved - complete [shostak](0.58 s)
inv_p4................................proved - complete [shostak](0.60 s)
inv_p5................................proved - complete [shostak](0.50 s)
inv_p6................................proved - complete [shostak](0.49 s)
inv_p7_TCC1...........................proved - complete [shostak](0.39 s)
inv_p7................................proved - complete [shostak](0.95 s)
inv_p8................................proved - complete [shostak](0.26 s)
inv_p9................................proved - complete [shostak](0.74 s)
inv_n5_TCC1...........................proved - complete [shostak](0.18 s)
inv_n5................................proved - complete [shostak](0.65 s)
inv_n6_TCC1...........................proved - complete [shostak](0.10 s)
inv_n6................................proved - complete [shostak](-.92 s)
inv_n7_TCC1...........................proved - complete [shostak](0.18 s)
inv_n7_TCC2...........................proved - complete [shostak](0.12 s)
inv_n7................................proved - complete [shostak](0.34 s)
inv_n8................................proved - complete [shostak](0.29 s)
inv_n9................................proved - complete [shostak](1.08 s)
inv_p.................................proved - complete [shostak](1.05 s)
minimum_inv_prop3_TCC1................proved - complete [shostak](0.24 s)
minimum_inv_prop3.....................proved - complete [shostak](0.29 s)
cauchy_nz_inv_TCC1....................proved - complete [shostak](0.66 s)
cauchy_nz_inv_TCC2....................proved - complete [shostak](0.14 s)
inv_nz_lemma..........................proved - complete [shostak](0.14 s)
inv_lemma.............................proved - complete [shostak](0.04 s)
Theory totals: 42 formulas, 42 attempted, 42 succeeded (11.96 s)
Proof summary for theory unique
unique_cauchy.........................proved - complete [shostak](0.70 s)
cauchy_dich1..........................proved - complete [shostak](0.05 s)
cauchy_dich2..........................proved - complete [shostak](0.03 s)
cauchy_dich3..........................proved - complete [shostak](0.03 s)
cauchy_dich4..........................proved - complete [shostak](0.03 s)
cauchy_dich5..........................proved - complete [shostak](0.04 s)
cauchy_trich..........................proved - complete [shostak](0.06 s)
cauchy_pos_characteristic.............proved - complete [shostak](0.13 s)
cauchy_neg_characteristic.............proved - complete [shostak](0.13 s)
cauchy_pos_monotonic..................proved - complete [shostak](0.37 s)
cauchy_monotonic......................proved - complete [shostak](0.61 s)
cauchy_odd_extend.....................proved - complete [shostak](0.43 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (2.61 s)
Proof summary for theory div
div_lemma.............................proved - incomplete [shostak](0.09 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.09 s)
Proof summary for theory rat
denominators_TCC1.....................proved - complete [shostak](0.03 s)
numerator_TCC1........................proved - complete [shostak](0.14 s)
cauchy_rat_TCC1.......................proved - complete [shostak](0.02 s)
rat_lemma.............................proved - incomplete [shostak](0.08 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.28 s)
Proof summary for theory shift
cauchy_div2n_TCC1.....................proved - complete [shostak](0.04 s)
cauchy_div2n_TCC2.....................proved - complete [shostak](0.28 s)
cauchy_mul2n_TCC1.....................proved - complete [shostak](0.18 s)
lemma_div2n...........................proved - complete [shostak](0.30 s)
lemma_mul2n...........................proved - complete [shostak](0.16 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.96 s)
Proof summary for theory min
cauchy_min_TCC1.......................proved - complete [shostak](0.54 s)
min_lemma.............................proved - complete [shostak](0.55 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.09 s)
Proof summary for theory max
cauchy_max_TCC1.......................proved - complete [shostak](0.36 s)
max_lemma.............................proved - complete [shostak](0.36 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.72 s)
Proof summary for theory sqrtx
nnsqrt_TCC1...........................proved - complete [shostak](0.02 s)
sqrt_p1_TCC1..........................proved - complete [shostak](0.02 s)
sqrt_p1_TCC2..........................proved - complete [shostak](0.03 s)
sqrt_p1...............................proved - complete [shostak](0.31 s)
sqrt_p2_TCC1..........................proved - complete [shostak](0.06 s)
sqrt_p2...............................proved - complete [shostak](0.13 s)
sqrt_p3...............................proved - complete [shostak](0.10 s)
cauchy_nnsqrt_TCC1....................proved - complete [shostak](0.11 s)
cauchy_nnsqrt_TCC2....................proved - complete [shostak](0.66 s)
sqrt_nn_lemma.........................proved - complete [shostak](0.74 s)
sqrt_lemma............................proved - complete [shostak](0.03 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.20 s)
Proof summary for theory bisection_nat_sqrt
fs_lt_def.............................proved - complete [shostak](0.12 s)
fs_eq_def.............................proved - complete [shostak](0.13 s)
fs_gt_def.............................proved - complete [shostak](0.11 s)
fs_trichotomy.........................proved - complete [shostak](0.12 s)
fs_le_ge..............................proved - complete [shostak](0.10 s)
bisection_sqrt_aux_TCC1...............proved - complete [shostak](0.05 s)
bisection_sqrt_aux_TCC2...............proved - complete [shostak](0.12 s)
bisection_sqrt_aux_TCC3...............proved - complete [shostak](0.15 s)
bisection_sqrt_aux_TCC4...............proved - complete [shostak](0.14 s)
bisection_sqrt_aux_TCC5...............proved - complete [shostak](0.15 s)
bisection_sqrt_aux_TCC6...............proved - complete [shostak](0.12 s)
bisection_sqrt_aux_prop...............proved - complete [shostak](0.57 s)
bisection_sqrt_TCC1...................proved - complete [shostak](0.03 s)
bisection_sqrt_TCC2...................proved - complete [shostak](0.08 s)
bisection_sqrt_def....................proved - complete [shostak](0.16 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (2.15 s)
Proof summary for theory power
abs_ge0...............................proved - complete [shostak](0.02 s)
abs_neg...............................proved - complete [shostak](0.03 s)
abs_interval..........................proved - complete [shostak](0.08 s)
abs_interval1.........................proved - complete [shostak](0.04 s)
abs_interval2.........................proved - complete [shostak](0.05 s)
triangle_open.........................proved - complete [shostak](0.14 s)
abs_error.............................proved - complete [shostak](0.23 s)
lemma_A2_generalized..................proved - complete [shostak](0.09 s)
cauchy_power_lt1_n_odd_TCC1...........proved - incomplete [shostak](0.13 s)
cauchy_power_lt1_n_odd_TCC2...........proved - incomplete [shostak](0.16 s)
cauchy_power_lt1_n_odd................proved - incomplete [shostak](1.08 s)
cauchy_power_lt1_n_even_TCC1..........proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_n_even_TCC2..........proved - incomplete [shostak](0.14 s)
cauchy_power_lt1_n_even...............proved - incomplete [shostak](-.88 s)
cauchy_power_lt1_snz_odd_TCC1.........proved - incomplete [shostak](0.13 s)
cauchy_power_lt1_snz_odd_TCC2.........proved - incomplete [shostak](0.15 s)
cauchy_power_lt1_snz_odd..............proved - incomplete [shostak](0.98 s)
cauchy_power_lt1_snz_even_TCC1........proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_snz_even_TCC2........proved - incomplete [shostak](0.14 s)
cauchy_power_lt1_snz_even.............proved - incomplete [shostak](0.60 s)
cauchy_power_lt1_sn_odd_TCC1..........proved - incomplete [shostak](0.13 s)
cauchy_power_lt1_sn_odd_TCC2..........proved - incomplete [shostak](0.18 s)
cauchy_power_lt1_sn_odd...............proved - incomplete [shostak](1.82 s)
cauchy_power_lt1_sn_even_TCC1.........proved - incomplete [shostak](0.12 s)
cauchy_power_lt1_sn_even_TCC2.........proved - incomplete [shostak](0.14 s)
cauchy_power_lt1_sn_even..............proved - incomplete [shostak](1.84 s)
cauchy_power_lt1_z_TCC1...............proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_z_TCC2...............proved - incomplete [shostak](0.15 s)
cauchy_power_lt1_z....................proved - incomplete [shostak](1.00 s)
cauchy_power_lt1_sp_odd_TCC1..........proved - incomplete [shostak](0.13 s)
cauchy_power_lt1_sp_odd...............proved - incomplete [shostak](1.17 s)
cauchy_power_lt1_sp_even_TCC1.........proved - incomplete [shostak](0.12 s)
cauchy_power_lt1_sp_even..............proved - incomplete [shostak](1.90 s)
cauchy_power_lt1_pz_TCC1..............proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_pz...................proved - incomplete [shostak](0.59 s)
cauchy_power_lt1_p_TCC1...............proved - incomplete [shostak](0.12 s)
cauchy_power_lt1_p....................proved - incomplete [shostak](0.67 s)
cauchy_power_lt1_main_generalized_TCC1...proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_main_generalized_TCC2...proved - incomplete [shostak](0.14 s)
cauchy_power_lt1_main_generalized.....proved - incomplete [shostak](0.51 s)
cauchy_power_lt1_main_TCC1............proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_main_TCC2............proved - incomplete [shostak](0.14 s)
cauchy_power_lt1_main.................proved - incomplete [shostak](0.17 s)
cauchy_power_lt1_isreal_TCC1..........proved - incomplete [shostak](-1.30 s)
cauchy_power_lt1_isreal_TCC2..........proved - incomplete [shostak](0.04 s)
cauchy_power_lt1_isreal_TCC3..........proved - incomplete [shostak](0.11 s)
cauchy_power_lt1_isreal...............proved - incomplete [shostak](0.37 s)
cauchy_power_lt1_TCC1.................proved - incomplete [shostak](0.02 s)
power_lemma_lt1_TCC1..................proved - complete [shostak](0.02 s)
power_lemma_lt1.......................proved - incomplete [shostak](0.43 s)
cauchy_power_div1.....................proved - incomplete [shostak](0.23 s)
cauchy_power_main_TCC1................proved - incomplete [shostak](0.16 s)
cauchy_power_main_TCC2................proved - incomplete [shostak](0.18 s)
cauchy_power_main.....................proved - incomplete [shostak](1.03 s)
cauchy_power_isreal_TCC1..............proved - incomplete [shostak](0.37 s)
cauchy_power_isreal...................proved - incomplete [shostak](0.86 s)
cauchy_power_TCC1.....................proved - incomplete [shostak](0.02 s)
power_lemma_TCC1......................proved - complete [shostak](0.02 s)
power_lemma...........................proved - incomplete [shostak](0.92 s)
Theory totals: 59 formulas, 59 attempted, 59 succeeded (18.50 s)
Proof summary for theory sum
IMP_sigma_TCC1........................proved - complete [shostak](0.03 s)
sum_lemma2_TCC1.......................proved - complete [shostak](0.03 s)
sum_lemma2_TCC2.......................proved - complete [shostak](0.02 s)
sum_lemma2............................proved - complete [shostak](0.87 s)
cauchy_sum_aux_TCC1...................proved - complete [shostak](0.03 s)
cauchy_sum_aux_TCC2...................proved - complete [shostak](0.02 s)
sum_lemma3_TCC1.......................proved - complete [shostak](0.03 s)
sum_lemma3_TCC2.......................proved - complete [shostak](0.02 s)
sum_lemma3............................proved - complete [shostak](0.11 s)
sum_lemma4_TCC1.......................proved - incomplete [shostak](0.17 s)
sum_lemma4............................proved - incomplete [shostak](0.52 s)
sum_lemma5............................proved - incomplete [shostak](0.83 s)
cauchys_real_TCC1.....................proved - complete [shostak](0.02 s)
cauchys_real_TCC2.....................proved - complete [shostak](0.02 s)
cauchy_sum_TCC1.......................proved - incomplete [shostak](0.22 s)
sum_lemma_TCC1........................proved - complete [shostak](0.03 s)
sum_lemma.............................proved - incomplete [shostak](0.20 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (3.17 s)
Proof summary for theory series
sum_TCC1..............................proved - complete [shostak](0.03 s)
sum_TCC2..............................proved - complete [shostak](0.02 s)
sum_lemma1............................proved - complete [shostak](0.15 s)
geometric_series_TCC1.................proved - complete [shostak](0.02 s)
geometric_series_aux1_TCC1............proved - complete [shostak](0.03 s)
geometric_series_aux1_TCC2............proved - complete [shostak](0.03 s)
geometric_series_aux1.................proved - complete [shostak](0.28 s)
geometric_series_aux_odd_TCC1.........proved - complete [shostak](0.09 s)
geometric_series_aux_odd..............proved - complete [shostak](0.85 s)
geometric_series_aux_even_TCC1........proved - complete [shostak](0.10 s)
geometric_series_aux_even_TCC2........proved - complete [shostak](0.02 s)
geometric_series_aux_even.............proved - complete [shostak](0.48 s)
geometric_series_approx_set_contains1...proved - complete [shostak](0.03 s)
geometric_series_approx_set_nonempty...proved - complete [shostak](0.03 s)
geometric_series_approx_set_pos_upper_bound_TCC1...proved - complete [shostak](0.03 s)
geometric_series_approx_set_pos_upper_bound_TCC2...proved - complete [shostak](0.02 s)
geometric_series_approx_set_pos_upper_bound...proved - complete [shostak](0.18 s)
geometric_series_approx_set_pos_least_upper_bound...proved - complete [shostak](0.30 s)
geometric_series_pos_limit_TCC1.......proved - complete [shostak](0.05 s)
geometric_series_pos_limit............proved - complete [shostak](0.05 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (2.79 s)
Proof summary for theory powerseries
powerseries_TCC1......................proved - complete [shostak](0.02 s)
powerseries_TCC2......................proved - complete [shostak](0.02 s)
powerseries_TCC3......................proved - complete [shostak](0.02 s)
cauchy_powerseries_TCC1...............proved - complete [shostak](0.03 s)
cauchy_powerseries_TCC2...............proved - incomplete [shostak](0.10 s)
powerseries_lemma_TCC1................proved - complete [shostak](0.03 s)
powerseries_lemma.....................proved - incomplete [shostak](0.14 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.36 s)
Proof summary for theory atanx
cauchy_ssmallreal_TCC1................proved - complete [shostak](0.03 s)
subtype_TCC1..........................proved - complete [shostak](0.04 s)
cauchy_vsmallreal_TCC1................proved - complete [shostak](0.02 s)
subtype_TCC2..........................proved - complete [shostak](0.03 s)
cauchy_atan_drx_series_TCC1...........proved - complete [shostak](0.13 s)
cauchy_atan_drx_series_TCC2...........proved - complete [shostak](0.14 s)
atan_series_lemma.....................proved - incomplete [shostak](0.17 s)
cauchy_atan_drxx_TCC1.................proved - incomplete [shostak](0.03 s)
cauchy_atan_drxx_prop_TCC1............proved - complete [shostak](0.02 s)
cauchy_atan_drxx_prop_TCC2............proved - complete [shostak](0.03 s)
cauchy_atan_drxx_prop.................proved - incomplete [shostak](1.32 s)
cauchy_atan_dr_TCC1...................proved - incomplete [shostak](0.14 s)
cauchy_atan_dr_TCC2...................proved - incomplete [shostak](0.18 s)
atan_dr_lemma.........................proved - incomplete [shostak](0.35 s)
cauchy_pi_TCC1........................proved - complete [shostak](0.06 s)
cauchy_pi_TCC2........................proved - incomplete [shostak](0.06 s)
cauchy_pi_TCC3........................proved - complete [shostak](0.50 s)
cauchy_pi_TCC4........................proved - incomplete [shostak](0.06 s)
pi_lemma..............................proved - incomplete [shostak](0.25 s)
cauchy_atan_TCC1......................proved - incomplete [shostak](0.13 s)
cauchy_atan_TCC2......................proved - incomplete [shostak](0.23 s)
cauchy_atan_TCC3......................proved - incomplete [shostak](0.16 s)
cauchy_atan_TCC4......................proved - incomplete [shostak](0.23 s)
cauchy_atan_TCC5......................proved - incomplete [shostak](0.14 s)
cauchy_atan_TCC6......................proved - incomplete [shostak](0.14 s)
cauchy_atan_TCC7......................proved - incomplete [shostak](0.23 s)
cauchy_atan_TCC8......................proved - incomplete [shostak](0.12 s)
cauchy_atan_TCC9......................proved - incomplete [shostak](0.18 s)
atan_lemma............................proved - incomplete [shostak](1.17 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (6.30 s)
Proof summary for theory asinx
cauchy_real_abs_le1_TCC1..............proved - complete [shostak](0.03 s)
subtype_TCC1..........................proved - complete [shostak](0.03 s)
cauchy_asin_TCC1......................proved - incomplete [shostak](0.09 s)
cauchy_asin_TCC2......................proved - incomplete [shostak](0.20 s)
cauchy_asin_TCC3......................proved - incomplete [shostak](0.11 s)
asin_lemma............................proved - incomplete [shostak](0.81 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.28 s)
Proof summary for theory acosx
acos_lemma............................proved - incomplete [shostak](0.08 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)
Proof summary for theory sincosx
real_3pi16_TCC1.......................proved - incomplete [shostak](0.12 s)
cauchy_real_3pi16_TCC1................proved - incomplete [shostak](0.15 s)
cauchy_nnsreal_TCC1...................proved - complete [shostak](0.03 s)
subtype_TCC1..........................proved - complete [shostak](0.02 s)
subtype_TCC2..........................proved - complete [shostak](0.03 s)
subtype_TCC3..........................proved - incomplete [shostak](0.09 s)
cauchy_sin_series_TCC1................proved - incomplete [shostak](0.09 s)
cauchy_cos_series_TCC1................proved - incomplete [shostak](0.07 s)
sin_series_lemma......................proved - incomplete [shostak](0.16 s)
cos_series_lemma......................proved - incomplete [shostak](0.16 s)
cauchy_sin_drx_TCC1...................proved - incomplete [shostak](0.02 s)
cauchy_sin_drx_TCC2...................proved - incomplete [shostak](2.36 s)
cauchy_cos_drx_TCC1...................proved - incomplete [shostak](0.03 s)
cauchy_cos_drx_TCC2...................proved - incomplete [shostak](2.97 s)
sin_drx_lemma_TCC1....................proved - incomplete [shostak](0.05 s)
sin_drx_lemma.........................proved - incomplete [shostak](3.06 s)
cauchy_sin_dr_TCC1....................proved - incomplete [shostak](0.34 s)
sin_dr_lemma..........................proved - incomplete [shostak](0.59 s)
cos_dr_lemma..........................proved - incomplete [shostak](2.55 s)
cauchy_sin_TCC1.......................proved - incomplete [shostak](0.06 s)
cauchy_sin_TCC2.......................proved - incomplete [shostak](0.09 s)
cauchy_sin_TCC3.......................proved - incomplete [shostak](0.48 s)
sin_lemma.............................proved - incomplete [shostak](4.25 s)
cos_lemma.............................proved - incomplete [shostak](4.04 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (21.80 s)
Proof summary for theory remx
modx_TCC1.............................proved - complete [shostak](0.12 s)
modx_def..............................proved - complete [shostak](0.10 s)
remx_TCC1.............................proved - complete [shostak](0.08 s)
remx_def..............................proved - complete [shostak](0.15 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.45 s)
Proof summary for theory trigx
sin_nz_TCC1...........................proved - incomplete [shostak](0.02 s)
cos_nz_TCC1...........................proved - incomplete [shostak](0.02 s)
cauchy_sin_nz_TCC1....................proved - incomplete [shostak](0.06 s)
cauchy_cos_nz_TCC1....................proved - incomplete [shostak](0.08 s)
subtype_TCC1..........................proved - incomplete [shostak](0.03 s)
subtype_TCC2..........................proved - incomplete [shostak](0.02 s)
cauchy_sec_TCC1.......................proved - incomplete [shostak](0.03 s)
cauchy_cosec_TCC1.....................proved - incomplete [shostak](0.04 s)
sec_TCC1..............................proved - incomplete [shostak](0.02 s)
cosec_TCC1............................proved - incomplete [shostak](0.03 s)
sec_lemma.............................proved - incomplete [shostak](0.06 s)
cosec_lemma...........................proved - incomplete [shostak](0.06 s)
tan_lemma_TCC1........................proved - incomplete [shostak](0.02 s)
tan_lemma.............................proved - incomplete [shostak](0.06 s)
cot_lemma.............................proved - incomplete [shostak](0.06 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.60 s)
Proof summary for theory log
cauchy_ln_small_TCC1..................proved - complete [shostak](0.03 s)
subtype_TCC1..........................proved - complete [shostak](0.03 s)
cauchy_ln_med_TCC1....................proved - complete [shostak](0.03 s)
subtype_TCC2..........................proved - complete [shostak](0.02 s)
cauchy_gt_quarter_TCC1................proved - complete [shostak](0.02 s)
subtype_TCC3..........................proved - complete [shostak](0.03 s)
cauchy_ln_series_TCC1.................proved - complete [shostak](0.03 s)
cauchy_ln_series_TCC2.................proved - complete [shostak](0.03 s)
ln_series_lemma_TCC1..................proved - complete [shostak](0.02 s)
ln_series_lemma.......................proved - incomplete [shostak](0.29 s)
ln_estimate_lemma_TCC1................proved - incomplete [shostak](0.04 s)
ln_estimate_lemma.....................proved - incomplete [shostak](0.28 s)
cauchy_ln_drx_TCC1....................proved - incomplete [shostak](0.04 s)
ln_drx_lemma_TCC1.....................proved - complete [shostak](0.03 s)
ln_drx_lemma..........................proved - incomplete [shostak](1.04 s)
cauchy_ln_drx_TCC2....................proved - incomplete [shostak](0.05 s)
cauchy_ln_half_TCC1...................proved - complete [shostak](0.07 s)
cauchy_ln_half_TCC2...................proved - incomplete [shostak](0.08 s)
cauchy_ln_half_lemma..................proved - incomplete [shostak](0.07 s)
cauchy_ln2_lemma......................proved - incomplete [shostak](0.06 s)
cauchy_ln_sqrt2_TCC1..................proved - incomplete [shostak](0.05 s)
cauchy_ln_sqrt2_lemma.................proved - incomplete [shostak](0.11 s)
cauchy_ln_dr_TCC1.....................proved - complete [shostak](0.12 s)
cauchy_ln_dr_TCC2.....................proved - complete [shostak](0.11 s)
ln_dr_lemma_TCC1......................proved - complete [shostak](0.03 s)
ln_dr_lemma...........................proved - incomplete [shostak](0.29 s)
cauchy_lnx_TCC1.......................proved - complete [shostak](0.09 s)
cauchy_lnx_TCC2.......................proved - complete [shostak](0.04 s)
cauchy_lnx_TCC3.......................proved - incomplete [shostak](0.20 s)
cauchy_lnx_TCC4.......................proved - incomplete [shostak](0.83 s)
ln_lemma_x_TCC1.......................proved - complete [shostak](0.02 s)
ln_lemma_x............................proved - incomplete [shostak](0.81 s)
cauchy_lnx_TCC5.......................proved - incomplete [shostak](0.03 s)
cauchy_ln_TCC1........................proved - complete [shostak](0.15 s)
cauchy_ln_TCC2........................proved - complete [shostak](0.10 s)
ln_lemma..............................proved - incomplete [shostak](0.19 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (5.46 s)
Proof summary for theory exp
cauchy_exp_series_TCC1................proved - complete [shostak](0.03 s)
cauchy_exp_series_TCC2................proved - complete [shostak](0.06 s)
exp_series_lemma......................proved - complete [shostak](0.06 s)
exp_estimate_lemma_TCC1...............proved - complete [shostak](0.03 s)
exp_estimate_lemma....................proved - incomplete [shostak](0.17 s)
cauchy_exp_dr_TCC1....................proved - complete [shostak](0.03 s)
exp_dr_lemma..........................proved - incomplete [shostak](3.06 s)
cauchy_exp_dr_TCC2....................proved - incomplete [shostak](0.03 s)
cauchy_exp_TCC1.......................proved - incomplete [shostak](0.51 s)
cauchy_exp_TCC2.......................proved - incomplete [shostak](0.03 s)
cauchy_exp_TCC3.......................proved - incomplete [shostak](0.52 s)
cauchy_exp_TCC4.......................proved - incomplete [shostak](0.03 s)
cauchy_exp_TCC5.......................proved - incomplete [shostak](0.48 s)
exp_lemma.............................proved - incomplete [shostak](1.03 s)
cauchy_exp_is_posreal.................proved - incomplete [shostak](0.04 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (6.11 s)
Proof summary for theory hyperbolicx
sinh_lemma............................proved - incomplete [shostak](0.10 s)
cosh_lemma............................proved - incomplete [shostak](0.13 s)
cauchy_sinh_type......................proved - incomplete [shostak](0.03 s)
cauchy_cosh_type......................proved - incomplete [shostak](0.03 s)
cauchy_coth_TCC1......................proved - incomplete [shostak](0.06 s)
tanh_lemma............................proved - incomplete [shostak](0.05 s)
sech_lemma............................proved - incomplete [shostak](0.06 s)
coth_lemma............................proved - incomplete [shostak](0.13 s)
csch_lemma............................proved - incomplete [shostak](0.06 s)
cauchy_tanh_type......................proved - incomplete [shostak](0.03 s)
cauchy_coth_type......................proved - incomplete [shostak](0.04 s)
cauchy_csch_type......................proved - incomplete [shostak](0.08 s)
cauchy_sech_type......................proved - incomplete [shostak](0.03 s)
cauchy_ge1_TCC1.......................proved - complete [shostak](0.03 s)
subtype_TCC1..........................proved - complete [shostak](0.03 s)
cauchy_asinh_TCC1.....................proved - incomplete [shostak](0.07 s)
cauchy_asinh_TCC2.....................proved - incomplete [shostak](0.16 s)
cauchy_acosh_TCC1.....................proved - incomplete [shostak](0.06 s)
cauchy_acosh_TCC2.....................proved - incomplete [shostak](0.13 s)
cauchy_atanh_TCC1.....................proved - complete [shostak](0.05 s)
cauchy_atanh_TCC2.....................proved - incomplete [shostak](-1.46 s)
asinh_lemma...........................proved - incomplete [shostak](0.16 s)
acosh_lemma...........................proved - incomplete [shostak](0.13 s)
atanh_lemma...........................proved - incomplete [shostak](0.14 s)
cauchy_asinh_type.....................proved - incomplete [shostak](0.03 s)
cauchy_acosh_type.....................proved - incomplete [shostak](0.03 s)
cauchy_atanh_type.....................proved - incomplete [shostak](0.03 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (0.42 s)
Proof summary for theory test
new_pi_bnds..........................proved - incomplete [shostak]( 3.57 s)
new_ln2_bnds.........................proved - incomplete [shostak]( 0.66 s)
new_e_bnds...........................proved - incomplete [shostak](37.42 s)
new_sqrt2_bnds.......................proved - complete [shostak]( 0.16 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (41.80 s)
Grand Totals: 582 proofs, 582 attempted, 582 succeeded (178.43 s)
[ Dauer der Verarbeitung: 0.122 Sekunden
]
|
|
