Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
arithmetic_ops.prf
Sprache: Lisp
Untersuchungsergebnis.summary Download desMT940 {MT940[529] Hlasm[2033] Haskell[2351]}zum Wurzelverzeichnis wechseln
***
*** top (17:39:9 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 series
series_TCC1...........................proved - complete [shostak](0.04 s)
inf_sum_TCC1..........................proved - complete [shostak](0.07 s)
inf_sum_TCC2..........................proved - complete [shostak](0.03 s)
series_diff...........................proved - complete [shostak](0.07 s)
series_sum............................proved - complete [shostak](0.06 s)
series_m_diff.........................proved - complete [shostak](0.07 s)
series_m_sum..........................proved - complete [shostak](0.07 s)
series_m_scal.........................proved - complete [shostak](0.07 s)
series_m_eq...........................proved - complete [shostak](0.06 s)
series_scal...........................proved - complete [shostak](0.08 s)
conv_series_terms_to_0................proved - complete [shostak](0.10 s)
series_limit_0_TCC1...................proved - complete [shostak](0.02 s)
series_limit_0........................proved - complete [shostak](0.02 s)
convergent_abs........................proved - complete [shostak](0.69 s)
partial_sums..........................proved - complete [shostak](0.28 s)
zero_series_conv......................proved - complete [shostak](0.08 s)
zero_series_limit_TCC1................proved - complete [shostak](0.02 s)
zero_series_limit.....................proved - complete [shostak](0.08 s)
tail_series_conv......................proved - complete [shostak](0.32 s)
tail_series_conv2.....................proved - complete [shostak](0.30 s)
conv_series_shift.....................proved - complete [shostak](0.03 s)
tail_conv.............................proved - complete [shostak](0.14 s)
end_series_conv.......................proved - complete [shostak](0.46 s)
scal_series_conv......................proved - complete [shostak](0.35 s)
conv_series_scal......................proved - complete [shostak](0.18 s)
limit_series_shift_TCC1...............proved - complete [shostak](0.02 s)
limit_series_shift_TCC2...............proved - complete [shostak](0.02 s)
limit_series_shift....................proved - complete [shostak](0.31 s)
limit_pos.............................proved - complete [shostak](0.09 s)
series_first_TCC1.....................proved - complete [shostak](0.02 s)
series_first..........................proved - complete [shostak](0.19 s)
inf_sum_scal_TCC1.....................proved - complete [shostak](0.02 s)
inf_sum_scal_TCC2.....................proved - complete [shostak](0.15 s)
inf_sum_scal..........................proved - complete [shostak](0.04 s)
comparison_test.......................proved - complete [shostak](0.58 s)
comparison_test_gen...................proved - complete [shostak](0.10 s)
inf_sum_eq............................proved - complete [shostak](0.07 s)
inf_sum_le_TCC1.......................proved - complete [shostak](0.05 s)
inf_sum_le_TCC2.......................proved - complete [shostak](0.02 s)
inf_sum_le............................proved - complete [shostak](0.15 s)
inf_sum_le_abs........................proved - complete [shostak](-.70 s)
inf_sum_triangle_TCC1.................proved - complete [shostak](0.02 s)
inf_sum_triangle_TCC2.................proved - complete [shostak](0.02 s)
inf_sum_triangle......................proved - complete [shostak](0.08 s)
series_sum_conv.......................proved - complete [shostak](0.50 s)
series_sum_convergence................proved - complete [shostak](0.12 s)
inf_sum_of_sum_TCC1...................proved - complete [shostak](0.04 s)
inf_sum_of_sum_TCC2...................proved - complete [shostak](0.08 s)
inf_sum_of_sum_TCC3...................proved - complete [shostak](0.08 s)
inf_sum_of_sum........................proved - complete [shostak](0.05 s)
abs_x_to_n_conv_TCC1..................proved - complete [shostak](0.03 s)
abs_x_to_n_conv.......................proved - complete [shostak](0.21 s)
cnv_seq_abs_x_to_n_TCC1...............proved - complete [shostak](0.02 s)
cnv_seq_abs_x_to_n....................proved - complete [shostak](0.71 s)
x_to_n_conv_TCC1......................proved - complete [shostak](0.02 s)
x_to_n_conv...........................proved - complete [shostak](0.18 s)
convergence_x_to_n....................proved - complete [shostak](0.24 s)
geometric_TCC1........................proved - complete [shostak](0.02 s)
sigma_geometric_aux_TCC1..............proved - complete [shostak](0.02 s)
sigma_geometric_aux...................proved - complete [shostak](0.38 s)
sigma_geometric_TCC1..................proved - complete [shostak](0.03 s)
sigma_geometric.......................proved - complete [shostak](0.10 s)
geometric_series_TCC1.................proved - complete [shostak](0.03 s)
geometric_series......................proved - complete [shostak](0.37 s)
geometric_conv........................proved - complete [shostak](0.05 s)
const_geometric_series................proved - complete [shostak](0.18 s)
geometric_sum_TCC1....................proved - complete [shostak](0.04 s)
geometric_sum.........................proved - complete [shostak](0.05 s)
scaf_abs_TCC1.........................proved - complete [shostak](0.02 s)
scaf_abs..............................proved - complete [shostak](0.48 s)
ratio_test_TCC1.......................proved - complete [shostak](0.03 s)
ratio_test............................proved - complete [shostak](0.26 s)
ratio_test_gen........................proved - complete [shostak](0.41 s)
ratio_test_gt_N.......................proved - complete [shostak](0.20 s)
ratio_test_lim_TCC1...................proved - complete [shostak](0.03 s)
ratio_test_lim........................proved - complete [shostak](0.41 s)
Theory totals: 76 formulas, 76 attempted, 76 succeeded (10.33 s)
Proof summary for theory series_lems
zero_tail_series_conv.................proved - complete [shostak](0.11 s)
zero_tail_series_limit_TCC1...........proved - complete [shostak](0.02 s)
zero_tail_series_limit................proved - complete [shostak](0.12 s)
zero_tail_series......................proved - complete [shostak](0.03 s)
single_nz_series_conv.................proved - complete [shostak](0.02 s)
single_nz_series_limit_TCC1...........proved - complete [shostak](0.02 s)
single_nz_series_limit................proved - complete [shostak](0.12 s)
single_nz_series......................proved - complete [shostak](0.03 s)
limit_nonneg..........................proved - complete [shostak](0.04 s)
convergence_nonneg....................proved - complete [shostak](0.52 s)
nonneg_series_bij.....................proved - incomplete [shostak](3.20 s)
nonneg_series_bij_conv................proved - incomplete [shostak](0.11 s)
nonneg_series_bij_limit_TCC1..........proved - incomplete [shostak](0.03 s)
nonneg_series_bij_limit...............proved - incomplete [shostak](0.12 s)
abs_series_bij........................proved - incomplete [shostak](0.63 s)
abs_series_bij_conv...................proved - incomplete [shostak](0.03 s)
abs_series_bij_limit_TCC1.............proved - complete [shostak](0.02 s)
abs_series_bij_limit_TCC2.............proved - incomplete [shostak](0.03 s)
abs_series_bij_limit..................proved - incomplete [shostak](0.05 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (5.25 s)
Proof summary for theory series_aux
zero_tail_series_conv.................proved - complete [shostak](0.11 s)
zero_tail_series_limit_TCC1...........proved - complete [shostak](0.02 s)
zero_tail_series_limit................proved - complete [shostak](0.12 s)
zero_tail_series......................proved - complete [shostak](0.03 s)
single_nz_series_conv.................proved - complete [shostak](0.02 s)
single_nz_series_limit_TCC1...........proved - complete [shostak](0.02 s)
single_nz_series_limit................proved - complete [shostak](0.12 s)
single_nz_series......................proved - complete [shostak](0.03 s)
limit_nonneg..........................proved - complete [shostak](0.03 s)
convergence_nonneg....................proved - complete [shostak](0.49 s)
nonneg_series_bij.....................proved - incomplete [shostak](3.09 s)
nonneg_series_bij_conv................proved - incomplete [shostak](0.10 s)
nonneg_series_bij_limit_TCC1..........proved - incomplete [shostak](0.02 s)
nonneg_series_bij_limit...............proved - incomplete [shostak](0.12 s)
abs_series_bij........................proved - incomplete [shostak](0.62 s)
abs_series_bij_conv...................proved - incomplete [shostak](0.03 s)
abs_series_bij_limit_TCC1.............proved - complete [shostak](0.02 s)
abs_series_bij_limit_TCC2.............proved - incomplete [shostak](0.02 s)
abs_series_bij_limit..................proved - incomplete [shostak](0.05 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (5.06 s)
Proof summary for theory absconv_series
Convergent_Series_TCC1................proved - complete [shostak](0.02 s)
absconvergent_series_TCC1.............proved - complete [shostak](0.02 s)
absconvergent_series_is_convergent....proved - complete [shostak](0.02 s)
abs_series_bij_abs....................proved - incomplete [shostak](0.13 s)
abs_series_bij_conv_abs...............proved - incomplete [shostak](0.04 s)
abs_series_bij_limit_abs_TCC1.........proved - incomplete [shostak](0.03 s)
abs_series_bij_limit_abs..............proved - incomplete [shostak](0.05 s)
extract_convergent....................proved - complete [shostak](0.04 s)
extract_comp..........................proved - complete [shostak](0.65 s)
subseq_absconvergent..................proved - complete [shostak](0.27 s)
nonneg_subseq.........................proved - complete [shostak](0.24 s)
sum_absconvergent.....................proved - complete [shostak](0.14 s)
opp_absconvergent.....................proved - complete [shostak](0.09 s)
diff_absconvergent....................proved - complete [shostak](0.06 s)
scal_absconvergent....................proved - complete [shostak](0.43 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (2.22 s)
Proof summary for theory power_series
hat_02n...............................proved - complete [shostak](0.07 s)
powerseq_TCC1.........................proved - complete [shostak](0.02 s)
powerseries_bounded...................proved - complete [shostak](0.03 s)
powerseries_conv_point................proved - complete [shostak](0.57 s)
powerseries_conv......................proved - complete [shostak](0.06 s)
powerseries_diverg....................proved - complete [shostak](0.05 s)
zero_powerseries_conv.................proved - complete [shostak](0.07 s)
powerseries_three_cases...............proved - complete [shostak](1.22 s)
powerseries_conv_abs_intv.............proved - complete [shostak](0.19 s)
apow_rew..............................proved - complete [shostak](0.06 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.35 s)
Proof summary for theory trig_fun
useful_prep_TCC1......................proved - complete [shostak](0.02 s)
useful_prep...........................proved - complete [shostak](0.04 s)
altsign_prep..........................proved - complete [shostak](0.08 s)
altsign_TCC1..........................proved - complete [shostak](0.02 s)
altsign_TCC2..........................proved - complete [shostak](0.11 s)
altsign_TCC3..........................proved - complete [shostak](0.04 s)
altsign_TCC4..........................proved - complete [shostak](0.08 s)
abs_altsign...........................proved - complete [shostak](0.21 s)
sin_conv_TCC1.........................proved - complete [shostak](0.03 s)
sin_conv_TCC2.........................proved - complete [shostak](0.01 s)
sin_conv_TCC3.........................proved - complete [shostak](0.02 s)
sin_conv..............................proved - complete [shostak](0.47 s)
sin_TCC1..............................proved - complete [shostak](0.07 s)
cos_conv..............................proved - complete [shostak](0.67 s)
cos_TCC1..............................proved - complete [shostak](0.07 s)
tan_TCC1..............................proved - complete [shostak](0.07 s)
sin_0.................................proved - complete [shostak](0.19 s)
cos_0.................................proved - complete [shostak](0.19 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (2.38 s)
Proof summary for theory power_series_conv
Inf_sum_TCC1..........................proved - complete [shostak](0.06 s)
Inf_sum_TCC2..........................proved - complete [shostak](0.08 s)
end_powerseries_conv..................proved - complete [shostak](0.04 s)
Inf_inf_TCC1..........................proved - complete [shostak](0.07 s)
Inf_inf...............................proved - complete [shostak](0.03 s)
Inf_inf_m_TCC1........................proved - complete [shostak](0.02 s)
Inf_inf_m.............................proved - complete [shostak](0.04 s)
powerseries_abs_conv..................proved - complete [shostak](0.17 s)
simple_TCC1...........................proved - complete [shostak](0.02 s)
simple_0_conv.........................proved - complete [shostak](0.20 s)
simple_conv...........................proved - complete [shostak](0.53 s)
m1_conv...............................proved - complete [shostak](0.21 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.48 s)
Proof summary for theory trig_props
IMP_power_series_deriv_TCC1...........proved - complete [shostak](0.02 s)
IMP_power_series_deriv_TCC2...........proved - complete [shostak](0.02 s)
IMP_power_series_deriv_TCC3...........proved - complete [shostak](0.02 s)
IMP_power_series_deriv_TCC4...........proved - complete [shostak](0.02 s)
sin_derivable_TCC1....................proved - complete [shostak](0.06 s)
sin_derivable.........................proved - complete [shostak](0.02 s)
deriv_sin_TCC1........................proved - complete [shostak](0.02 s)
deriv_sin.............................proved - complete [shostak](1.93 s)
cos_derivable.........................proved - complete [shostak](0.03 s)
deriv_cos_TCC1........................proved - complete [shostak](0.02 s)
deriv_cos.............................proved - complete [shostak](0.81 s)
sin2_cos2_derivable...................proved - complete [shostak](0.23 s)
sin2_cos2.............................proved - complete [shostak](0.55 s)
sin_cos_one...........................proved - complete [shostak](0.57 s)
sin_lt_1..............................proved - complete [shostak](0.10 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (4.42 s)
Proof summary for theory power_series_deriv
deriv_domain.........................proved - complete [shostak]( 0.02 s)
IMP_power_series_deriv_scaf_TCC1.....proved - complete [shostak]( 0.02 s)
IMP_power_series_deriv_scaf_TCC2.....proved - complete [shostak]( 0.01 s)
IMP_power_series_deriv_scaf_TCC3.....proved - complete [shostak]( 0.03 s)
IMP_power_series_deriv_scaf_TCC4.....proved - complete [shostak]( 0.02 s)
powerseries_deriv_TCC1...............proved - complete [shostak]( 0.07 s)
powerseries_deriv_TCC2...............proved - complete [shostak]( 0.02 s)
powerseries_deriv_TCC3...............proved - complete [shostak]( 0.02 s)
powerseries_deriv_TCC4...............proved - complete [shostak]( 1.13 s)
powerseries_deriv....................proved - complete [shostak](11.37 s)
powerseries_derivable................proved - complete [shostak]( 0.02 s)
powerseries_cont.....................proved - complete [shostak]( 0.12 s)
Inf_sum_derivable....................proved - complete [shostak]( 0.03 s)
deriv_Inf_sum_TCC1...................proved - complete [shostak]( 0.02 s)
deriv_Inf_sum_TCC2...................proved - complete [shostak]( 0.02 s)
deriv_Inf_sum........................proved - complete [shostak](-1.07 s)
deriv_Inf_sum_derivable..............proved - complete [shostak]( 0.03 s)
Inf_sum_derivable_n_times............proved - complete [shostak]( 0.07 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (11.96 s)
Proof summary for theory power_series_deriv_scaf
deriv_domain.........................proved - complete [shostak]( 0.02 s)
IMP_power_series_derivseq_TCC1.......proved - complete [shostak]( 0.02 s)
IMP_power_series_derivseq_TCC2.......proved - complete [shostak]( 0.01 s)
IMP_power_series_derivseq_TCC3.......proved - complete [shostak]( 0.02 s)
IMP_power_series_derivseq_TCC4.......proved - complete [shostak]( 0.02 s)
GET_tk_prep_TCC1.....................proved - complete [shostak]( 0.05 s)
GET_tk_prep_TCC2.....................proved - complete [shostak]( 0.02 s)
GET_tk_prep_TCC3.....................proved - complete [shostak]( 0.03 s)
GET_tk_prep..........................proved - complete [shostak]( 0.68 s)
GET_tk_TCC1..........................proved - complete [shostak]( 0.33 s)
Gseq_TCC1............................proved - complete [shostak]( 0.08 s)
Gseq_TCC2............................proved - complete [shostak]( 0.11 s)
Gseq_TCC3............................proved - complete [shostak]( 0.03 s)
conv_scaf0_TCC1......................proved - complete [shostak]( 0.02 s)
conv_scaf0...........................proved - complete [shostak]( 2.36 s)
A2seq_TCC1...........................proved - complete [shostak]( 0.04 s)
A2_conv_scaf.........................proved - complete [shostak]( 0.63 s)
A2_conv..............................proved - complete [shostak]( 1.79 s)
Gseq_conv............................proved - complete [shostak](11.40 s)
abs_Gseq_conv........................proved - complete [shostak](13.14 s)
inf_sum_Gseq_abs_TCC1................proved - complete [shostak]( 0.03 s)
inf_sum_Gseq_abs_TCC2................proved - complete [shostak]( 0.03 s)
inf_sum_Gseq_abs.....................proved - complete [shostak]( 0.04 s)
conv_scaf2...........................proved - complete [shostak]( 1.11 s)
conv_scaf1_TCC1......................proved - complete [shostak]( 0.04 s)
conv_scaf1_TCC2......................proved - complete [shostak]( 0.02 s)
conv_scaf1...........................proved - complete [shostak]( 0.22 s)
conv_scaf3...........................proved - complete [shostak]( 0.40 s)
limit_eq_rew.........................proved - complete [shostak]( 0.02 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (32.70 s)
Proof summary for theory power_series_derivseq
IMP_power_series_conv_TCC1............proved - complete [shostak](0.02 s)
IMP_power_series_conv_TCC2............proved - complete [shostak](0.01 s)
IMP_power_series_conv_TCC3............proved - complete [shostak](0.02 s)
deriv_powerseq_TCC1...................proved - complete [shostak](0.03 s)
deriv_powerseries_conv................proved - complete [shostak](4.21 s)
derivseq_conv.........................proved - complete [shostak](0.28 s)
deriv_series_shift_TCC1...............proved - complete [shostak](0.02 s)
deriv_series_shift_TCC2...............proved - complete [shostak](0.02 s)
deriv_series_shift....................proved - complete [shostak](0.56 s)
conv_derivseq.........................proved - complete [shostak](0.10 s)
deriv_powerseq_lem....................proved - complete [shostak](0.34 s)
sigma_power_derivable_TCC1............proved - complete [shostak](0.02 s)
sigma_power_derivable.................proved - complete [shostak](0.16 s)
deriv_sigma_power_TCC1................proved - complete [shostak](0.02 s)
deriv_sigma_power.....................proved - complete [shostak](0.26 s)
deriv_sigma_power_conv................proved - complete [shostak](0.24 s)
deriv_conv_prep_TCC1..................proved - complete [shostak](0.04 s)
deriv_conv_prep.......................proved - complete [shostak](0.08 s)
deriv_powerseq_cont...................proved - complete [shostak](0.35 s)
lim_deriv_alt_TCC1....................proved - complete [shostak](0.03 s)
lim_deriv_alt.........................proved - complete [shostak](0.12 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (6.93 s)
Proof summary for theory taylor_series
T_pred_0..............................proved - complete [shostak](0.04 s)
IMP_power_series_deriv_TCC1...........proved - complete [shostak](0.02 s)
IMP_power_series_deriv_TCC2...........proved - complete [shostak](0.01 s)
IMP_power_series_deriv_TCC3...........proved - complete [shostak](0.02 s)
IMP_power_series_deriv_TCC4...........proved - complete [shostak](0.03 s)
deriv_domain..........................proved - complete [shostak](0.02 s)
Inf_sum_0_TCC1........................proved - complete [shostak](0.03 s)
Inf_sum_0.............................proved - complete [shostak](0.30 s)
nderivseq_lem.........................proved - complete [shostak](-.64 s)
conv_nderivseq........................proved - complete [shostak](0.10 s)
Inf_sum_derivable_n_times_TCC1........proved - complete [shostak](0.02 s)
Inf_sum_derivable_n_times.............proved - complete [shostak](0.04 s)
nderiv_Inf_sum_TCC1...................proved - complete [shostak](0.02 s)
nderiv_Inf_sum_TCC2...................proved - complete [shostak](0.02 s)
nderiv_Inf_sum........................proved - complete [shostak](1.29 s)
Taylor_expansion......................proved - complete [shostak](0.09 s)
Taylor_seq_TCC1.......................proved - complete [shostak](0.02 s)
Taylor_seq_TCC2.......................proved - complete [shostak](0.02 s)
Taylor_seq_TCC3.......................proved - complete [shostak](0.02 s)
Taylor_seq_term_TCC1..................proved - complete [shostak](0.02 s)
Taylor_seq_term_TCC2..................proved - complete [shostak](0.02 s)
Taylor_seq_term_TCC3..................proved - complete [shostak](0.02 s)
Taylor_seq_term.......................proved - complete [shostak](0.11 s)
GET_C_TCC1............................proved - complete [shostak](0.05 s)
GET_C_TCC2............................proved - complete [shostak](0.02 s)
GET_C_TCC3............................proved - complete [shostak](0.42 s)
is_taylor_prep_TCC1...................proved - complete [shostak](0.04 s)
is_taylor_prep........................proved - complete [shostak](0.26 s)
is_taylor_TCC1........................proved - complete [shostak](0.04 s)
is_taylor.............................proved - complete [shostak](0.23 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (2.70 s)
Proof summary for theory power_series_integ
deriv_domain..........................proved - complete [shostak](0.02 s)
IMP_power_series_conv_TCC1............proved - complete [shostak](0.01 s)
IMP_power_series_conv_TCC2............proved - complete [shostak](0.01 s)
IMP_power_series_conv_TCC3............proved - complete [shostak](0.02 s)
integseq_TCC1.........................proved - complete [shostak](0.03 s)
integseq_TCC2.........................proved - complete [shostak](0.02 s)
integ_powerseq_TCC1...................proved - complete [shostak](0.02 s)
conv_integseq.........................proved - complete [shostak](1.42 s)
integ_powerseries_conv................proved - complete [shostak](0.24 s)
integseq_lim_shift_TCC1...............proved - complete [shostak](0.11 s)
integseq_lim_shift_TCC2...............proved - complete [shostak](0.02 s)
integseq_lim_shift....................proved - complete [shostak](0.28 s)
IMP_power_series_deriv_TCC1...........proved - complete [shostak](0.01 s)
IMP_power_series_deriv_TCC2...........proved - complete [shostak](0.02 s)
powerseries_integrable?_TCC1..........proved - complete [shostak](0.10 s)
powerseries_integrable?...............proved - incomplete [shostak](0.03 s)
powerseries_integral_TCC1.............proved - incomplete [shostak](0.03 s)
powerseries_integral..................proved - incomplete [shostak](0.88 s)
integral_powerseries..................proved - incomplete [shostak](0.20 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (3.47 s)
Grand Totals: 301 proofs, 301 attempted, 301 succeeded (91.24 s)
[ zur Elbe Produktseite wechseln0.123Quellennavigators
]
|
|
