Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
Sprache: Unknown
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[760] Hlasm[2228] Haskell[2592]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** top (17:46:36 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 trig_doc
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory trig
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory trig_basic
sin2_cos2.............................proved - incomplete [shostak](0.30 s)
cos2..................................proved - incomplete [shostak](0.06 s)
sin2..................................proved - incomplete [shostak](0.05 s)
cos_0.................................proved - incomplete [shostak](0.16 s)
sin_0.................................proved - incomplete [shostak](0.15 s)
sin_pi2...............................proved - incomplete [shostak](0.25 s)
cos_pi2...............................proved - incomplete [shostak](0.11 s)
tan_0_TCC1............................proved - incomplete [shostak](0.18 s)
tan_0.................................proved - incomplete [shostak](0.02 s)
sin_neg...............................proved - incomplete [shostak](0.46 s)
cos_neg...............................proved - incomplete [shostak](0.27 s)
tan_neg_TCC1..........................proved - incomplete [shostak](0.03 s)
tan_neg...............................proved - incomplete [shostak](0.05 s)
cos_sin...............................proved - incomplete [shostak](1.38 s)
sin_cos...............................proved - incomplete [shostak](0.08 s)
sin_shift.............................proved - incomplete [shostak](0.07 s)
cos_shift.............................proved - incomplete [shostak](0.06 s)
neg_cos...............................proved - incomplete [shostak](0.12 s)
neg_sin...............................proved - incomplete [shostak](0.11 s)
sin_pi................................proved - incomplete [shostak](0.24 s)
cos_pi................................proved - incomplete [shostak](0.19 s)
tan_pi_TCC1...........................proved - incomplete [shostak](0.03 s)
tan_pi................................proved - incomplete [shostak](0.06 s)
sin_3pi2..............................proved - incomplete [shostak](0.10 s)
cos_3pi2..............................proved - incomplete [shostak](0.11 s)
sin_2pi...............................proved - incomplete [shostak](0.14 s)
cos_2pi...............................proved - incomplete [shostak](0.13 s)
tan_2pi_TCC1..........................proved - incomplete [shostak](0.02 s)
tan_2pi...............................proved - incomplete [shostak](0.08 s)
sin_plus..............................proved - incomplete [shostak](1.46 s)
sin_minus.............................proved - incomplete [shostak](0.08 s)
cos_plus..............................proved - incomplete [shostak](0.12 s)
cos_minus.............................proved - incomplete [shostak](0.08 s)
tan_plus_TCC1.........................proved - incomplete [shostak](0.06 s)
tan_plus..............................proved - incomplete [shostak](0.15 s)
tan_minus_TCC1........................proved - incomplete [shostak](0.07 s)
tan_minus.............................proved - incomplete [shostak](0.13 s)
arc_sin_cos...........................proved - incomplete [shostak](0.09 s)
pythagorean...........................proved - incomplete [shostak](0.14 s)
sin_2a................................proved - incomplete [shostak](0.10 s)
cos_2a................................proved - incomplete [shostak](0.09 s)
cos_2a_cos............................proved - incomplete [shostak](0.14 s)
cos_2a_sin............................proved - incomplete [shostak](0.10 s)
tan_2a_TCC1...........................proved - incomplete [shostak](0.08 s)
tan_2a................................proved - incomplete [shostak](0.10 s)
sin_period............................proved - incomplete [shostak](0.30 s)
cos_period............................proved - incomplete [shostak](0.16 s)
tan_period_TCC1.......................proved - incomplete [shostak](0.21 s)
tan_period............................proved - incomplete [shostak](0.24 s)
sin_k_pi..............................proved - incomplete [shostak](0.20 s)
cos_2k_pi.............................proved - incomplete [shostak](0.11 s)
cos_k_pi..............................proved - incomplete [shostak](0.23 s)
sin_k_pi2.............................proved - incomplete [shostak](0.10 s)
tan_k_pi_TCC1.........................proved - incomplete [shostak](0.06 s)
tan_k_pi..............................proved - incomplete [shostak](0.07 s)
sin_eq_0_2pi..........................proved - incomplete [shostak](0.42 s)
cos_eq_0_2pi..........................proved - incomplete [shostak](0.20 s)
sin_eq_0..............................proved - incomplete [shostak](0.76 s)
cos_eq_0..............................proved - incomplete [shostak](0.12 s)
sin_eq_1..............................proved - incomplete [shostak](1.02 s)
cos_eq_1..............................proved - incomplete [shostak](0.15 s)
Theory totals: 61 formulas, 61 attempted, 61 succeeded (12.36 s)
Proof summary for theory sincos_def
sin_TCC1..............................proved - incomplete [shostak](0.16 s)
sin_range.............................proved - incomplete [shostak](0.29 s)
cos_range.............................proved - incomplete [shostak](0.26 s)
sin_range_ax..........................proved - incomplete [shostak](0.02 s)
cos_range_ax..........................proved - incomplete [shostak](0.02 s)
tan_TCC1..............................proved - incomplete [shostak](0.03 s)
tan_rew...............................proved - incomplete [shostak](0.03 s)
sin_sin_phase_TCC1....................proved - incomplete [shostak](0.07 s)
sin_sin_phase.........................proved - incomplete [shostak](0.15 s)
cos_cos_phase.........................proved - incomplete [shostak](0.15 s)
sin_sin_value_TCC1....................proved - incomplete [shostak](0.06 s)
sin_sin_value.........................proved - incomplete [shostak](0.38 s)
cos_cos_value_TCC1....................proved - incomplete [shostak](0.02 s)
cos_cos_value.........................proved - incomplete [shostak](0.16 s)
tan_value_TCC.........................proved - incomplete [shostak](0.25 s)
tan_tan_value_TCC1....................proved - incomplete [shostak](0.05 s)
tan_tan_value_TCC2....................proved - incomplete [shostak](0.05 s)
tan_tan_value.........................proved - incomplete [shostak](0.25 s)
sin_asin..............................proved - incomplete [shostak](0.34 s)
cos_acos..............................proved - incomplete [shostak](0.16 s)
tan_atan_TCC1.........................proved - incomplete [shostak](0.07 s)
tan_atan..............................proved - incomplete [shostak](0.10 s)
asin_sin..............................proved - incomplete [shostak](0.07 s)
acos_cos..............................proved - incomplete [shostak](0.05 s)
atan_tan_TCC1.........................proved - incomplete [shostak](0.06 s)
atan_tan..............................proved - incomplete [shostak](0.08 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (3.33 s)
Proof summary for theory sincos_phase
trig_phase_TCC1.......................proved - incomplete [shostak](0.06 s)
sin_phase_TCC1........................proved - incomplete [shostak](0.16 s)
sin_phase_TCC2........................proved - incomplete [shostak](0.17 s)
sin_phase_TCC3........................proved - incomplete [shostak](0.15 s)
sin_phase_TCC4........................proved - incomplete [shostak](-1.14 s)
sin_phase_TCC5........................proved - incomplete [shostak](0.25 s)
sin_phase_TCC6........................proved - incomplete [shostak](0.13 s)
cos_phase_TCC1........................proved - incomplete [shostak](0.12 s)
cos_phase_TCC2........................proved - incomplete [shostak](0.22 s)
phase_sin_q1..........................proved - incomplete [shostak](0.21 s)
phase_sin_q2..........................proved - incomplete [shostak](0.21 s)
phase_sin_q3..........................proved - incomplete [shostak](0.21 s)
phase_sin_q4..........................proved - incomplete [shostak](0.20 s)
phases_sin............................proved - incomplete [shostak](0.12 s)
sin_q1_TCC1...........................proved - incomplete [shostak](0.09 s)
sin_q1................................proved - incomplete [shostak](0.09 s)
sin_q2_TCC1...........................proved - incomplete [shostak](0.09 s)
sin_q2................................proved - incomplete [shostak](0.15 s)
sin_q3_TCC1...........................proved - incomplete [shostak](0.10 s)
sin_q3................................proved - incomplete [shostak](0.09 s)
sin_q4_TCC1...........................proved - incomplete [shostak](0.10 s)
sin_q4................................proved - incomplete [shostak](0.16 s)
phase_cos_q1..........................proved - incomplete [shostak](0.18 s)
phase_cos_q2..........................proved - incomplete [shostak](0.20 s)
phases_cos............................proved - incomplete [shostak](0.07 s)
cos_q1_TCC1...........................proved - incomplete [shostak](0.09 s)
cos_q1................................proved - incomplete [shostak](0.12 s)
cos_q2_TCC1...........................proved - incomplete [shostak](0.10 s)
cos_q2................................proved - incomplete [shostak](0.12 s)
cos_q3_TCC1...........................proved - incomplete [shostak](0.11 s)
cos_q3................................proved - incomplete [shostak](0.14 s)
cos_q4_TCC1...........................proved - incomplete [shostak](0.10 s)
cos_q4................................proved - incomplete [shostak](0.15 s)
sin_h2_TCC1...........................proved - incomplete [shostak](0.08 s)
sin_h2................................proved - incomplete [shostak](0.23 s)
sin_h1_TCC1...........................proved - incomplete [shostak](0.10 s)
sin_h1................................proved - incomplete [shostak](0.14 s)
cos_h1................................proved - incomplete [shostak](0.15 s)
cos_h2................................proved - incomplete [shostak](0.09 s)
sin_phase_neg_TCC1....................proved - incomplete [shostak](0.07 s)
sin_phase_neg.........................proved - incomplete [shostak](0.58 s)
cos_phase_neg.........................proved - incomplete [shostak](0.16 s)
sin_eqv_cos_phase_TCC1................proved - incomplete [shostak](0.09 s)
sin_eqv_cos_phase_TCC2................proved - incomplete [shostak](0.08 s)
sin_eqv_cos_phase.....................proved - incomplete [shostak](0.51 s)
cos_eqv_sin_phase.....................proved - incomplete [shostak](0.29 s)
sin_phase_inv_TCC1....................proved - incomplete [shostak](0.09 s)
sin_phase_inv_TCC2....................proved - incomplete [shostak](0.03 s)
sin_phase_inv.........................proved - incomplete [shostak](0.23 s)
cos_phase_inv.........................proved - incomplete [shostak](0.23 s)
sin_phase_3pi2_TCC1...................proved - incomplete [shostak](0.07 s)
sin_phase_3pi2........................proved - incomplete [shostak](0.14 s)
sin_phase_0...........................proved - incomplete [shostak](0.04 s)
sin_phase_pi4_TCC1....................proved - incomplete [shostak](0.07 s)
sin_phase_pi4.........................proved - incomplete [shostak](0.19 s)
sin_phase_pi2_TCC1....................proved - incomplete [shostak](0.07 s)
sin_phase_pi2.........................proved - incomplete [shostak](0.11 s)
cos_phase_0...........................proved - incomplete [shostak](0.07 s)
cos_phase_pi4.........................proved - incomplete [shostak](0.18 s)
cos_phase_pi2.........................proved - incomplete [shostak](0.18 s)
cos_phase_pi_TCC1.....................proved - incomplete [shostak](0.06 s)
cos_phase_pi..........................proved - incomplete [shostak](0.03 s)
sin_phase_asin_TCC1...................proved - incomplete [shostak](0.13 s)
sin_phase_asin_TCC2...................proved - incomplete [shostak](0.05 s)
sin_phase_asin........................proved - incomplete [shostak](0.47 s)
cos_phase_acos_TCC1...................proved - incomplete [shostak](0.06 s)
cos_phase_acos........................proved - incomplete [shostak](0.11 s)
sin2_cos2_phase.......................proved - incomplete [shostak](0.51 s)
sin_phase_diff_TCC1...................proved - incomplete [shostak](0.07 s)
sin_phase_diff_TCC2...................proved - incomplete [shostak](0.09 s)
sin_phase_diff........................proved - incomplete [shostak](2.20 s)
cos_phase_sum_TCC1....................proved - incomplete [shostak](0.10 s)
cos_phase_sum.........................proved - incomplete [shostak](2.40 s)
cos_phase_diff........................proved - incomplete [shostak](0.32 s)
sin_phase_sum.........................proved - incomplete [shostak](0.45 s)
Theory totals: 75 formulas, 75 attempted, 75 succeeded (14.64 s)
Proof summary for theory sincos_quad
nnreal_quad1_closed_TCC1.............proved - incomplete [shostak]( 0.04 s)
nnreal_quad1_open_TCC1...............proved - incomplete [shostak]( 0.04 s)
posreal_lt_pi_TCC1...................proved - incomplete [shostak]( 0.03 s)
noa_real_lt_pi2......................proved - incomplete [shostak]( 0.08 s)
noa_real_abs_lt1.....................proved - complete [shostak]( 0.05 s)
noa_posreal_lt_pi....................proved - incomplete [shostak]( 0.05 s)
noa_real_abs_lt_pi2..................proved - incomplete [shostak]( 0.07 s)
noa_posreal_lt_pi4...................proved - incomplete [shostak]( 0.05 s)
conn_real_lt_pi2.....................proved - incomplete [shostak]( 0.05 s)
conn_real_abs_lt1....................proved - complete [shostak]( 0.03 s)
conn_posreal_lt_pi...................proved - incomplete [shostak]( 0.02 s)
deriv_domain_real_abs_lt1............proved - complete [shostak]( 0.03 s)
deriv_domain_posreal_lt_pi...........proved - incomplete [shostak]( 0.13 s)
deriv_domain_abs_lt_pi2..............proved - incomplete [shostak]( 0.05 s)
deriv_domain_posreal_lt_pi4..........proved - incomplete [shostak]( 0.15 s)
sin_value_bij........................proved - incomplete [shostak]( 0.03 s)
cos_value_bij........................proved - incomplete [shostak]( 0.03 s)
sin_value_strict_increasing..........proved - incomplete [shostak]( 0.09 s)
sin_value_increasing.................proved - incomplete [shostak]( 0.04 s)
cos_value_strict_decreasing..........proved - incomplete [shostak]( 0.07 s)
cos_value_decreasing.................proved - incomplete [shostak]( 0.04 s)
sin_value_neg_TCC1...................proved - incomplete [shostak]( 0.15 s)
sin_value_neg........................proved - incomplete [shostak]( 0.12 s)
cos_value_neg_TCC1...................proved - incomplete [shostak]( 0.04 s)
cos_value_neg........................proved - incomplete [shostak]( 0.16 s)
sin_eqv_cos_value_TCC1...............proved - incomplete [shostak]( 0.06 s)
sin_eqv_cos_value....................proved - incomplete [shostak](-1.16 s)
sin_eqv_cos_quad_TCC1................proved - incomplete [shostak]( 0.04 s)
sin_eqv_cos_quad_TCC2................proved - incomplete [shostak]( 0.04 s)
sin_eqv_cos_quad.....................proved - incomplete [shostak]( 0.08 s)
cos_eqv_sin_quad_TCC1................proved - incomplete [shostak]( 0.02 s)
cos_eqv_sin_quad_TCC2................proved - incomplete [shostak]( 0.06 s)
cos_eqv_sin_quad.....................proved - incomplete [shostak]( 0.05 s)
sin_value_minus_pi2_TCC1.............proved - incomplete [shostak]( 0.04 s)
sin_value_minus_pi2..................proved - incomplete [shostak]( 0.06 s)
sin_value_0_TCC1.....................proved - incomplete [shostak]( 0.04 s)
sin_value_0..........................proved - incomplete [shostak]( 0.05 s)
sin_value_pi4_TCC1...................proved - incomplete [shostak]( 0.05 s)
sin_value_pi4........................proved - incomplete [shostak]( 0.09 s)
sin_value_pi2_TCC1...................proved - incomplete [shostak]( 0.05 s)
sin_value_pi2........................proved - incomplete [shostak]( 0.07 s)
cos_value_0_TCC1.....................proved - incomplete [shostak]( 0.02 s)
cos_value_0..........................proved - incomplete [shostak]( 0.04 s)
cos_value_pi4_TCC1...................proved - incomplete [shostak]( 0.04 s)
cos_value_pi4........................proved - incomplete [shostak]( 0.10 s)
cos_value_pi2_TCC1...................proved - incomplete [shostak]( 0.04 s)
cos_value_pi2........................proved - incomplete [shostak]( 0.06 s)
cos_value_pi_TCC1....................proved - incomplete [shostak]( 0.02 s)
cos_value_pi.........................proved - incomplete [shostak]( 0.04 s)
asin_sin_value.......................proved - incomplete [shostak]( 0.04 s)
acos_cos_value.......................proved - incomplete [shostak]( 0.04 s)
sin_value_asin.......................proved - incomplete [shostak]( 0.03 s)
cos_value_acos.......................proved - incomplete [shostak]( 0.03 s)
sin2_cos2_value......................proved - incomplete [shostak]( 0.82 s)
sin_eqv_sqrt_cos_value_TCC1..........proved - incomplete [shostak]( 0.09 s)
sin_eqv_sqrt_cos_value...............proved - incomplete [shostak]( 0.19 s)
cos_eqv_sqrt_sin_value_TCC1..........proved - incomplete [shostak]( 0.10 s)
cos_eqv_sqrt_sin_value...............proved - incomplete [shostak]( 0.18 s)
atan_tan_value_TCC1..................proved - incomplete [shostak]( 0.06 s)
atan_tan_value_TCC2..................proved - incomplete [shostak]( 0.04 s)
atan_tan_value_TCC3..................proved - incomplete [shostak]( 0.06 s)
atan_tan_value.......................proved - incomplete [shostak]( 0.27 s)
sin_value_atan_TCC1..................proved - incomplete [shostak]( 0.07 s)
sin_value_atan.......................proved - incomplete [shostak]( 0.99 s)
cos_value_atan_TCC1..................proved - incomplete [shostak]( 0.05 s)
cos_value_atan.......................proved - incomplete [shostak]( 0.37 s)
sin_value_pi6_TCC1...................proved - incomplete [shostak]( 0.05 s)
sin_value_pi6........................proved - incomplete [shostak]( 0.45 s)
cos_value_pi6_TCC1...................proved - incomplete [shostak]( 0.04 s)
cos_value_pi6........................proved - incomplete [shostak]( 0.18 s)
cos_value_sum_TCC1...................proved - incomplete [shostak]( 0.07 s)
cos_value_sum........................proved - incomplete [shostak]( 0.42 s)
sin_value_diff_TCC1..................proved - incomplete [shostak]( 0.07 s)
sin_value_diff.......................proved - incomplete [shostak]( 0.33 s)
sin_value_derivable_TCC1.............proved - incomplete [shostak]( 0.05 s)
sin_value_derivable_TCC2.............proved - incomplete [shostak]( 0.05 s)
sin_value_derivable_TCC3.............proved - incomplete [shostak]( 0.02 s)
sin_value_derivable..................proved - incomplete [shostak]( 1.04 s)
sin_value_derivable_fun..............proved - incomplete [shostak]( 0.04 s)
deriv_sin_value_TCC1.................proved - incomplete [shostak]( 0.02 s)
deriv_sin_value_TCC2.................proved - incomplete [shostak]( 0.04 s)
deriv_sin_value......................proved - incomplete [shostak]( 2.04 s)
sin_value_sum_TCC1...................proved - incomplete [shostak]( 0.09 s)
sin_value_sum_TCC2...................proved - incomplete [shostak]( 0.08 s)
sin_value_sum........................proved - incomplete [shostak](10.45 s)
cos_value_diff_TCC1..................proved - incomplete [shostak]( 0.06 s)
cos_value_diff_TCC2..................proved - incomplete [shostak]( 0.05 s)
cos_value_diff.......................proved - incomplete [shostak]( 0.19 s)
cos_value_derivable_TCC1.............proved - incomplete [shostak]( 0.03 s)
cos_value_derivable_TCC2.............proved - incomplete [shostak]( 0.02 s)
cos_value_derivable_TCC3.............proved - incomplete [shostak]( 0.02 s)
cos_value_derivable..................proved - incomplete [shostak]( 0.38 s)
cos_value_derivable_fun..............proved - incomplete [shostak]( 0.03 s)
deriv_cos_value_TCC1.................proved - incomplete [shostak]( 0.03 s)
deriv_cos_value_TCC2.................proved - incomplete [shostak]( 0.06 s)
deriv_cos_value_TCC3.................proved - incomplete [shostak]( 0.06 s)
deriv_cos_value......................proved - incomplete [shostak]( 0.89 s)
Theory totals: 97 formulas, 97 attempted, 97 succeeded (22.42 s)
Proof summary for theory acos
nnreal_le_pi_TCC1.....................proved - incomplete [shostak](0.02 s)
acos_TCC1.............................proved - incomplete [shostak](0.06 s)
acos_neg_TCC1.........................proved - complete [shostak](0.03 s)
acos_neg..............................proved - incomplete [shostak](0.06 s)
acos_0................................proved - incomplete [shostak](0.09 s)
acos_sqrt_half_TCC1...................proved - complete [shostak](0.09 s)
acos_sqrt_half........................proved - incomplete [shostak](0.05 s)
acos_1................................proved - incomplete [shostak](0.04 s)
acos_minus1...........................proved - incomplete [shostak](0.05 s)
acos_minus_sqrt_half_TCC1.............proved - complete [shostak](0.10 s)
acos_minus_sqrt_half..................proved - incomplete [shostak](0.09 s)
acos_strict_decreasing................proved - incomplete [shostak](0.06 s)
acos_bij..............................proved - incomplete [shostak](0.13 s)
acos_sum_TCC1.........................proved - complete [shostak](0.04 s)
acos_sum_TCC2.........................proved - complete [shostak](0.06 s)
acos_sum_TCC3.........................proved - complete [shostak](0.32 s)
acos_sum..............................proved - incomplete [shostak](8.00 s)
acos_derivable_TCC1...................proved - complete [shostak](0.04 s)
acos_derivable_TCC2...................proved - complete [shostak](0.03 s)
acos_derivable_TCC3...................proved - complete [shostak](0.06 s)
acos_derivable........................proved - incomplete [shostak](0.09 s)
acos_derivable_fun....................proved - incomplete [shostak](0.02 s)
deriv_acos_fun_TCC1...................proved - incomplete [shostak](0.02 s)
deriv_acos_fun_TCC2...................proved - incomplete [shostak](0.02 s)
deriv_acos_fun........................proved - incomplete [shostak](0.13 s)
Theory totals: 25 formulas, 25 attempted, 25 succeeded (9.69 s)
Proof summary for theory asin
real_abs_le_pi2_TCC1..................proved - incomplete [shostak](0.04 s)
noa_abs_lt1...........................proved - complete [shostak](0.05 s)
noa_nnreal_lt1........................proved - complete [shostak](0.07 s)
deriv_domain_abs_lt1..................proved - complete [shostak](0.03 s)
deriv_domain_nnreal_lt_1..............proved - complete [shostak](0.12 s)
asin_TCC1.............................proved - incomplete [shostak](0.04 s)
asin_TCC2.............................proved - complete [shostak](0.15 s)
asin_TCC3.............................proved - complete [shostak](0.08 s)
asin_TCC4.............................proved - incomplete [shostak](0.31 s)
asin_TCC5.............................proved - incomplete [shostak](0.06 s)
asin_neg_restrict_TCC1................proved - complete [shostak](0.11 s)
asin_neg_restrict_TCC2................proved - complete [shostak](0.02 s)
asin_neg_restrict.....................proved - incomplete [shostak](0.37 s)
asin_pos_restrict_TCC1................proved - complete [shostak](0.08 s)
asin_pos_restrict_TCC2................proved - complete [shostak](0.02 s)
asin_pos_restrict.....................proved - incomplete [shostak](0.29 s)
asin_0................................proved - incomplete [shostak](0.03 s)
asin_sqrt_half_TCC1...................proved - complete [shostak](0.09 s)
asin_sqrt_half........................proved - incomplete [shostak](0.17 s)
asin_1................................proved - incomplete [shostak](0.02 s)
asin_neg_TCC1.........................proved - complete [shostak](0.02 s)
asin_neg..............................proved - incomplete [shostak](0.17 s)
asin_minus1...........................proved - incomplete [shostak](0.02 s)
asin_minus_sqrt_half_TCC1.............proved - complete [shostak](0.10 s)
asin_minus_sqrt_half..................proved - incomplete [shostak](0.09 s)
asin_strict_increasing................proved - incomplete [shostak](1.30 s)
asin_bij..............................proved - incomplete [shostak](1.03 s)
asin_diff_TCC1........................proved - complete [shostak](0.03 s)
asin_diff_TCC2........................proved - complete [shostak](0.05 s)
asin_diff_TCC3........................proved - complete [shostak](0.30 s)
asin_diff.............................proved - incomplete [shostak](3.21 s)
asin_derivable_TCC1...................proved - complete [shostak](0.03 s)
asin_derivable_TCC2...................proved - complete [shostak](0.03 s)
asin_derivable_TCC3...................proved - complete [shostak](0.02 s)
asin_derivable........................proved - incomplete [shostak](1.27 s)
asin_derivable_fun....................proved - incomplete [shostak](0.02 s)
deriv_asin_fun_TCC1...................proved - incomplete [shostak](0.02 s)
deriv_asin_fun_TCC2...................proved - complete [shostak](0.06 s)
deriv_asin_fun_TCC3...................proved - complete [shostak](0.07 s)
deriv_asin_fun........................proved - incomplete [shostak](2.86 s)
asin_pos_bnds_TCC1....................proved - incomplete [shostak](0.19 s)
asin_pos_bnds.........................proved - incomplete [shostak](4.11 s)
Theory totals: 42 formulas, 42 attempted, 42 succeeded (17.15 s)
Proof summary for theory atan
IMP_nth_derivatives_TCC1.............proved - complete [shostak]( 0.03 s)
IMP_nth_derivatives_TCC2.............proved - complete [shostak]( 0.02 s)
IMP_taylors_TCC1.....................proved - complete [shostak]( 0.02 s)
atan_deriv_fn_TCC1...................proved - complete [shostak]( 0.07 s)
atan_deriv_fn_TCC2...................proved - complete [shostak]( 0.07 s)
one_over_one_plus_t_sq_cont..........proved - complete [shostak]( 0.21 s)
atan_value_TCC1......................proved - incomplete [shostak]( 0.05 s)
atan_value_0.........................proved - incomplete [shostak]( 0.03 s)
atan_neg_value.......................proved - incomplete [shostak]( 0.43 s)
atan_inv_value.......................proved - incomplete [shostak](-0.68 s)
atan_inv_neg_value...................proved - incomplete [shostak]( 0.14 s)
atan_value_strict_increasing.........proved - incomplete [shostak]( 0.09 s)
atan_value_minus_x1_TCC1.............proved - complete [shostak]( 0.09 s)
atan_value_minus_x1..................proved - incomplete [shostak]( 3.02 s)
atan_value_minus_x2_TCC1.............proved - complete [shostak]( 0.09 s)
atan_value_minus_x2..................proved - incomplete [shostak]( 0.42 s)
atan_value_minus_TCC1................proved - complete [shostak]( 0.08 s)
atan_value_minus_TCC2................proved - incomplete [shostak]( 0.07 s)
atan_value_minus_TCC3................proved - incomplete [shostak]( 0.06 s)
atan_value_minus.....................proved - incomplete [shostak]( 0.30 s)
pi_TCC1..............................proved - incomplete [shostak]( 0.07 s)
real_abs_lt_pi2_TCC1.................proved - incomplete [shostak]( 0.04 s)
atan_TCC1............................proved - incomplete [shostak]( 0.22 s)
pi_value.............................proved - incomplete [shostak]( 0.06 s)
atan_strict_increasing...............proved - incomplete [shostak]( 0.03 s)
atan_bij.............................proved - incomplete [shostak]( 0.42 s)
atan_0...............................proved - incomplete [shostak]( 0.01 s)
atan_inv.............................proved - incomplete [shostak]( 0.08 s)
atan_inv_neg.........................proved - incomplete [shostak]( 0.11 s)
atan_def_TCC1........................proved - incomplete [shostak]( 0.11 s)
atan_def.............................proved - incomplete [shostak]( 0.02 s)
acot_TCC1............................proved - incomplete [shostak]( 0.07 s)
atan_neg.............................proved - incomplete [shostak]( 0.02 s)
acot_neg.............................proved - incomplete [shostak]( 0.07 s)
atan_minus_TCC1......................proved - incomplete [shostak]( 0.07 s)
atan_minus_TCC2......................proved - incomplete [shostak]( 0.07 s)
atan_minus...........................proved - incomplete [shostak]( 0.12 s)
atan_plus_TCC1.......................proved - complete [shostak]( 0.06 s)
atan_plus_TCC2.......................proved - incomplete [shostak]( 0.04 s)
atan_plus_TCC3.......................proved - incomplete [shostak]( 0.04 s)
atan_plus............................proved - incomplete [shostak]( 0.26 s)
atan_sub_swap_TCC1...................proved - complete [shostak]( 0.02 s)
atan_sub_swap_TCC2...................proved - complete [shostak]( 0.03 s)
atan_sub_swap_TCC3...................proved - complete [shostak]( 0.09 s)
atan_sub_swap........................proved - incomplete [shostak]( 0.26 s)
deriv_atan_fun.......................proved - incomplete [shostak]( 0.15 s)
continuous_atan......................proved - incomplete [shostak]( 0.07 s)
atan_1...............................proved - incomplete [shostak]( 0.29 s)
atan_bnds............................proved - incomplete [shostak]( 1.70 s)
pi_bnds..............................proved - incomplete [shostak]( 0.22 s)
atanF_TCC1...........................proved - complete [shostak]( 0.13 s)
atanF_TCC2...........................proved - complete [shostak]( 0.11 s)
atanF_TCC3...........................proved - complete [shostak]( 0.20 s)
atan_taylors_prep1_TCC1..............proved - complete [shostak]( 0.04 s)
atan_taylors_prep1...................proved - complete [shostak]( 0.67 s)
atan_taylors_prep2...................proved - complete [shostak]( 0.93 s)
atan_taylors_prep3...................proved - complete [shostak]( 0.48 s)
atanN_derivable......................proved - complete [shostak]( 0.03 s)
atanD_derivable......................proved - complete [shostak]( 0.04 s)
atan_taylors_prep4_TCC1..............proved - complete [shostak]( 0.02 s)
atan_taylors_prep4_TCC2..............proved - complete [shostak]( 0.09 s)
atan_taylors_prep4...................proved - complete [shostak]( 0.13 s)
atan_taylors_prep5_TCC1..............proved - complete [shostak]( 0.02 s)
atan_taylors_prep5...................proved - complete [shostak]( 0.39 s)
atan_taylors_prep6_TCC1..............proved - complete [shostak]( 0.03 s)
atan_taylors_prep6_TCC2..............proved - complete [shostak]( 0.08 s)
atan_taylors_prep6...................proved - complete [shostak]( 0.88 s)
atan_taylors_prep7_TCC1..............proved - complete [shostak]( 0.04 s)
atan_taylors_prep7_TCC2..............proved - complete [shostak]( 0.08 s)
atan_taylors_prep7...................proved - complete [shostak]( 0.42 s)
atan_taylors_prep8_TCC1..............proved - complete [shostak]( 0.11 s)
atan_taylors_prep8_TCC2..............proved - complete [shostak]( 0.04 s)
atan_taylors_prep8_TCC3..............proved - complete [shostak]( 0.10 s)
atan_taylors_prep8_TCC4..............proved - complete [shostak]( 0.05 s)
atan_taylors_prep8...................proved - complete [shostak](48.30 s)
atan_series_prep4....................proved - complete [shostak]( 0.12 s)
atan_series_prep5_TCC1...............proved - complete [shostak]( 0.02 s)
atan_series_prep5_TCC2...............proved - complete [shostak]( 0.13 s)
atan_series_prep5....................proved - complete [shostak]( 0.28 s)
atan_series_prep6....................proved - complete [shostak]( 0.39 s)
atan_nderiv_TCC1.....................proved - incomplete [shostak]( 0.24 s)
atan_nderiv_TCC2.....................proved - complete [shostak]( 0.10 s)
atan_nderiv_TCC3.....................proved - complete [shostak]( 0.12 s)
atan_nderiv_TCC4.....................proved - complete [shostak]( 0.20 s)
atan_nderiv_TCC5.....................proved - complete [shostak]( 0.11 s)
atan_nderiv_TCC6.....................proved - complete [shostak]( 0.13 s)
atan_nderiv..........................proved - incomplete [shostak]( 1.95 s)
atan_nderiv_0_TCC1...................proved - complete [shostak]( 0.10 s)
atan_nderiv_0_TCC2...................proved - complete [shostak]( 0.09 s)
atan_nderiv_0........................proved - incomplete [shostak]( 1.24 s)
atan_n_times_derivable...............proved - incomplete [shostak]( 0.20 s)
atan_series_prep7....................proved - complete [shostak]( 1.89 s)
atan_series_prep8_TCC1...............proved - incomplete [shostak]( 0.08 s)
atan_series_prep8....................proved - incomplete [shostak]( 0.37 s)
atan_series_term_TCC1................proved - complete [shostak]( 0.07 s)
atan_series_n_TCC1...................proved - complete [shostak]( 0.02 s)
atan_series_n_increasing.............proved - complete [shostak]( 3.49 s)
atan_series_n_a0.....................proved - complete [shostak]( 0.11 s)
atan_series_eqv_TCC1.................proved - complete [shostak]( 0.08 s)
atan_series_eqv_TCC2.................proved - incomplete [shostak]( 0.03 s)
atan_series_eqv_TCC3.................proved - complete [shostak]( 0.07 s)
atan_series_eqv......................proved - incomplete [shostak]( 1.05 s)
atan_taylors_TCC1....................proved - incomplete [shostak]( 0.09 s)
atan_taylors_TCC2....................proved - complete [shostak]( 0.07 s)
atan_taylors.........................proved - incomplete [shostak]( 0.48 s)
atan_series_TCC1.....................proved - complete [shostak]( 0.07 s)
atan_series..........................proved - incomplete [shostak]( 1.35 s)
Theory totals: 107 formulas, 107 attempted, 107 succeeded (77.60 s)
Proof summary for theory tan_quad
tan_value_def_TCC1....................proved - incomplete [shostak](0.05 s)
tan_value_def_TCC2....................proved - incomplete [shostak](0.06 s)
tan_value_def_TCC3....................proved - incomplete [shostak](0.08 s)
tan_value_def.........................proved - incomplete [shostak](0.32 s)
tan_value_0_TCC1......................proved - incomplete [shostak](0.04 s)
tan_value_0...........................proved - incomplete [shostak](0.03 s)
tan_value_pi4_TCC1....................proved - incomplete [shostak](0.05 s)
tan_value_pi4.........................proved - incomplete [shostak](0.10 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.73 s)
Proof summary for theory atan_approx
atan_pos_le1_ub_lt....................proved - complete [shostak](0.61 s)
atan_pos_le1_lb_lt....................proved - complete [shostak](0.63 s)
atan_pos_le1_bounds...................proved - incomplete [shostak](0.93 s)
atan_pos_le1_lb_inc...................proved - complete [shostak](0.79 s)
atan_pos_le1_ub_dec...................proved - complete [shostak](1.89 s)
pi_lbn_lt.............................proved - complete [shostak](0.17 s)
pi_lbn_LT.............................proved - complete [shostak](0.13 s)
pi_bounds.............................proved - incomplete [shostak](0.14 s)
pi_lb_pos.............................proved - complete [shostak](0.25 s)
pi_ub_pos.............................proved - incomplete [shostak](0.03 s)
pi_bounds0............................proved - incomplete [shostak](0.30 s)
pi_bounds2............................proved - incomplete [shostak](0.70 s)
pi_bound..............................proved - incomplete [shostak](0.03 s)
pi_lb_inc.............................proved - complete [shostak](0.09 s)
pi_ub_dec.............................proved - complete [shostak](0.10 s)
atan_pos_bounds_TCC1..................proved - complete [shostak](0.03 s)
atan_pos_bounds.......................proved - incomplete [shostak](0.33 s)
atan_lb_TCC1..........................proved - complete [shostak](0.03 s)
atan_lb_TCC2..........................proved - complete [shostak](0.03 s)
atan_bounds...........................proved - incomplete [shostak](0.07 s)
atan_lb_increasing....................proved - incomplete [shostak](1.04 s)
atan_ub_increasing....................proved - incomplete [shostak](0.94 s)
atan_pos_lb_inc.......................proved - complete [shostak](0.14 s)
atan_pos_ub_dec.......................proved - incomplete [shostak](0.15 s)
pi_lb_pi..............................proved - incomplete [shostak](0.38 s)
pi_ub_pi..............................proved - incomplete [shostak](0.37 s)
pi_lb_diff............................proved - complete [shostak](2.11 s)
pi_ub_diff............................proved - incomplete [shostak](0.88 s)
pi_lb_diff_bounds.....................proved - complete [shostak](3.86 s)
pi_lb_quot_bounds.....................proved - complete [shostak](0.88 s)
pi_ub_diff_bounds.....................proved - incomplete [shostak](3.46 s)
pi_ub_quot_bounds.....................proved - incomplete [shostak](-.66 s)
Theory totals: 32 formulas, 32 attempted, 32 succeeded (20.85 s)
Proof summary for theory trig_values
sin_cos_pi4...........................proved - incomplete [shostak](0.06 s)
cos_pi4...............................proved - incomplete [shostak](0.22 s)
sin_pi4...............................proved - incomplete [shostak](0.07 s)
cos_3pi4..............................proved - incomplete [shostak](0.21 s)
sin_3pi4..............................proved - incomplete [shostak](0.20 s)
tan_pi4_TCC1..........................proved - incomplete [shostak](0.06 s)
tan_pi4...............................proved - incomplete [shostak](0.06 s)
sin_pi3_cos_pi6.......................proved - incomplete [shostak](0.06 s)
sin_pi6_cos_pi3.......................proved - incomplete [shostak](0.06 s)
sin_pi6...............................proved - incomplete [shostak](0.23 s)
cos_pi6...............................proved - incomplete [shostak](0.20 s)
tan_pi6_TCC1..........................proved - incomplete [shostak](0.04 s)
tan_pi6...............................proved - incomplete [shostak](0.09 s)
sin_pi3...............................proved - incomplete [shostak](0.05 s)
cos_pi3...............................proved - incomplete [shostak](0.05 s)
tan_pi3_TCC1..........................proved - incomplete [shostak](0.05 s)
tan_pi3...............................proved - incomplete [shostak](0.08 s)
sin_2pi3..............................proved - incomplete [shostak](0.15 s)
cos_2pi3..............................proved - incomplete [shostak](0.17 s)
tan_2pi3_TCC1.........................proved - incomplete [shostak](0.16 s)
tan_2pi3..............................proved - incomplete [shostak](0.12 s)
cos_5pi4..............................proved - incomplete [shostak](0.20 s)
sin_5pi4..............................proved - incomplete [shostak](0.21 s)
sin_cos_5pi4..........................proved - incomplete [shostak](0.10 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (2.90 s)
Proof summary for theory trig_ineq
cos_gt_0..............................proved - incomplete [shostak](0.35 s)
sin_gt_0..............................proved - incomplete [shostak](0.08 s)
sin_ge_0..............................proved - incomplete [shostak](0.03 s)
cos_ge_0..............................proved - incomplete [shostak](0.09 s)
sin_lt_0..............................proved - incomplete [shostak](0.08 s)
cos_lt_0..............................proved - incomplete [shostak](0.11 s)
sin_le_0..............................proved - incomplete [shostak](0.09 s)
cos_le_0..............................proved - incomplete [shostak](0.11 s)
tan_gt_0_TCC1.........................proved - incomplete [shostak](0.09 s)
tan_gt_0..............................proved - incomplete [shostak](0.07 s)
tan_lt_0_TCC1.........................proved - incomplete [shostak](0.10 s)
tan_lt_0..............................proved - incomplete [shostak](0.07 s)
tan_pi2_def...........................proved - incomplete [shostak](0.06 s)
tan_npi_def...........................proved - incomplete [shostak](0.05 s)
cos_ge_0_3pi2.........................proved - incomplete [shostak](0.18 s)
sin_increasing_imp....................proved - incomplete [shostak](0.19 s)
sin_increasing........................proved - incomplete [shostak](0.07 s)
sin_decreasing........................proved - incomplete [shostak](0.27 s)
cos_increasing........................proved - incomplete [shostak](0.24 s)
cos_decreasing........................proved - incomplete [shostak](0.24 s)
tan_increasing_imp_TCC1...............proved - incomplete [shostak](0.03 s)
tan_increasing_imp_TCC2...............proved - incomplete [shostak](0.03 s)
tan_increasing_imp....................proved - incomplete [shostak](0.34 s)
tan_increasing_TCC1...................proved - incomplete [shostak](0.03 s)
tan_increasing_TCC2...................proved - incomplete [shostak](0.02 s)
tan_increasing........................proved - incomplete [shostak](0.08 s)
sin_incr..............................proved - incomplete [shostak](0.07 s)
sin_decr..............................proved - incomplete [shostak](0.11 s)
cos_incr..............................proved - incomplete [shostak](0.05 s)
cos_decr..............................proved - incomplete [shostak](0.04 s)
tan_incr..............................proved - incomplete [shostak](0.04 s)
sin_gt................................proved - incomplete [shostak](0.16 s)
sin_lt................................proved - incomplete [shostak](0.16 s)
sin_ge................................proved - incomplete [shostak](0.07 s)
Theory totals: 34 formulas, 34 attempted, 34 succeeded (3.79 s)
Proof summary for theory trig_full
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory trig_extra
sin_minus_2pi.........................proved - incomplete [shostak](0.12 s)
cos_minus_2pi.........................proved - incomplete [shostak](0.11 s)
tan_minus_2pi_TCC1....................proved - incomplete [shostak](0.07 s)
tan_minus_2pi_TCC2....................proved - incomplete [shostak](0.18 s)
tan_minus_2pi.........................proved - incomplete [shostak](0.09 s)
sin_minus_3pi2........................proved - incomplete [shostak](0.14 s)
cos_minus_3pi2........................proved - incomplete [shostak](0.13 s)
tan_minus_3pi2_TCC1...................proved - incomplete [shostak](0.16 s)
tan_minus_3pi2_TCC2...................proved - incomplete [shostak](0.03 s)
tan_minus_3pi2........................proved - incomplete [shostak](0.12 s)
sin_minus_pi..........................proved - incomplete [shostak](0.10 s)
cos_minus_pi..........................proved - incomplete [shostak](0.08 s)
tan_minus_pi_TCC1.....................proved - incomplete [shostak](0.04 s)
tan_minus_pi..........................proved - incomplete [shostak](0.06 s)
sin_minus_pi2.........................proved - incomplete [shostak](0.12 s)
cos_minus_pi2.........................proved - incomplete [shostak](0.09 s)
tan_minus_pi2_TCC1....................proved - incomplete [shostak](0.06 s)
tan_minus_pi2.........................proved - incomplete [shostak](0.09 s)
sin_2pi_minus.........................proved - incomplete [shostak](0.12 s)
cos_2pi_minus.........................proved - incomplete [shostak](0.13 s)
tan_2pi_minus_TCC1....................proved - incomplete [shostak](-1.21 s)
tan_2pi_minus.........................proved - incomplete [shostak](0.09 s)
sin_3pi2_minus........................proved - incomplete [shostak](0.13 s)
cos_3pi2_minus........................proved - incomplete [shostak](0.16 s)
tan_3pi2_minus_TCC1...................proved - incomplete [shostak](0.14 s)
tan_3pi2_minus........................proved - incomplete [shostak](0.11 s)
sin_pi_minus..........................proved - incomplete [shostak](0.10 s)
cos_pi_minus..........................proved - incomplete [shostak](0.11 s)
tan_pi_minus_TCC1.....................proved - incomplete [shostak](0.05 s)
tan_pi_minus..........................proved - incomplete [shostak](0.05 s)
sin_pi2_minus.........................proved - incomplete [shostak](0.11 s)
cos_pi2_minus.........................proved - incomplete [shostak](0.15 s)
tan_pi2_minus_TCC1....................proved - incomplete [shostak](0.08 s)
tan_pi2_minus.........................proved - incomplete [shostak](0.09 s)
sin_times_cos.........................proved - incomplete [shostak](0.12 s)
cos_times_cos.........................proved - incomplete [shostak](0.12 s)
sin_times_sin.........................proved - incomplete [shostak](0.11 s)
sin_sum...............................proved - incomplete [shostak](0.13 s)
sin_diff..............................proved - incomplete [shostak](0.13 s)
cos_sum...............................proved - incomplete [shostak](0.28 s)
cos_diff..............................proved - incomplete [shostak](0.29 s)
tan_diff_TCC1.........................proved - incomplete [shostak](0.03 s)
tan_diff..............................proved - incomplete [shostak](0.15 s)
sq_sin................................proved - incomplete [shostak](0.10 s)
sq_cos................................proved - incomplete [shostak](0.12 s)
sin_half_zeroes.......................proved - incomplete [shostak](0.10 s)
cos_half_zeroes.......................proved - incomplete [shostak](0.12 s)
cos_half_zeroes2......................proved - incomplete [shostak](0.09 s)
sq_tan_TCC1...........................proved - incomplete [shostak](0.07 s)
sq_tan................................proved - incomplete [shostak](0.17 s)
sin_half_TCC1.........................proved - incomplete [shostak](0.04 s)
sin_half_TCC2.........................proved - incomplete [shostak](0.08 s)
sin_half..............................proved - incomplete [shostak](0.21 s)
cos_half_TCC1.........................proved - incomplete [shostak](0.08 s)
cos_half_TCC2.........................proved - incomplete [shostak](0.10 s)
cos_half_TCC3.........................proved - incomplete [shostak](0.11 s)
cos_half..............................proved - incomplete [shostak](0.35 s)
tan_half_TCC1.........................proved - incomplete [shostak](0.13 s)
tan_half_TCC2.........................proved - incomplete [shostak](0.35 s)
tan_half..............................proved - incomplete [shostak](0.16 s)
tan_half2_TCC1........................proved - incomplete [shostak](0.08 s)
tan_half2.............................proved - incomplete [shostak](0.13 s)
sin_3a................................proved - incomplete [shostak](0.26 s)
cos_3a................................proved - incomplete [shostak](0.23 s)
sin_eq_sin............................proved - incomplete [shostak](0.56 s)
cos_eq_cos............................proved - incomplete [shostak](0.39 s)
tan_eq_tan............................proved - incomplete [shostak](0.19 s)
sin_cos_eq............................proved - incomplete [shostak](0.44 s)
sin_eq_cos............................proved - incomplete [shostak](0.17 s)
tan_eq_1..............................proved - incomplete [shostak](0.04 s)
sin_eq_pm1............................proved - incomplete [shostak](0.26 s)
cos_eq_pm1............................proved - incomplete [shostak](0.19 s)
sin_plus_cos..........................proved - incomplete [shostak](0.15 s)
spc_tan_prep..........................proved - incomplete [shostak](0.43 s)
sin_plus_cos_atan2_TCC1...............proved - complete [shostak](0.04 s)
sin_plus_cos_atan2....................proved - incomplete [shostak](0.91 s)
Theory totals: 76 formulas, 76 attempted, 76 succeeded (10.41 s)
Proof summary for theory atan2
atan2_TCC1............................proved - complete [shostak](0.04 s)
atan2_TCC2............................proved - complete [shostak](0.03 s)
atan2_TCC3............................proved - complete [shostak](0.03 s)
atan2_0_2pi_TCC1......................proved - complete [shostak](0.04 s)
atan2_0_2pi_TCC2......................proved - incomplete [shostak](0.14 s)
atan2_0_2pi_TCC3......................proved - incomplete [shostak](0.02 s)
atan2_0_2pi_TCC4......................proved - incomplete [shostak](0.03 s)
atan2_0_2pi...........................proved - incomplete [shostak](0.33 s)
atan2_ge_0_lt_2pi_TCC1................proved - complete [shostak](0.04 s)
atan2_ge_0_lt_2pi.....................proved - incomplete [shostak](0.15 s)
nnreal_lt_2pi_TCC1....................proved - incomplete [shostak](0.07 s)
atan2_TCC4............................proved - incomplete [shostak](0.03 s)
atan2_cancel_pos_TCC1.................proved - complete [shostak](0.10 s)
atan2_cancel_pos......................proved - incomplete [shostak](0.21 s)
atan2_cancel_neg_TCC1.................proved - complete [shostak](0.11 s)
atan2_cancel_neg......................proved - incomplete [shostak](0.32 s)
atan2_swap_pos_TCC1...................proved - complete [shostak](0.07 s)
atan2_swap_pos_TCC2...................proved - complete [shostak](0.03 s)
atan2_swap_pos_TCC3...................proved - complete [shostak](0.02 s)
atan2_swap_pos_TCC4...................proved - complete [shostak](0.09 s)
atan2_swap_pos........................proved - incomplete [shostak](-.91 s)
atan2_swap_neg_TCC1...................proved - complete [shostak](0.07 s)
atan2_swap_neg_TCC2...................proved - complete [shostak](0.02 s)
atan2_swap_neg_TCC3...................proved - complete [shostak](0.03 s)
atan2_swap_neg_TCC4...................proved - complete [shostak](0.09 s)
atan2_swap_neg........................proved - incomplete [shostak](0.41 s)
atan2_swap_zero_TCC1..................proved - complete [shostak](0.03 s)
atan2_swap_zero_TCC2..................proved - incomplete [shostak](0.11 s)
atan2_swap_zero.......................proved - incomplete [shostak](0.15 s)
atan2_cos_sin_TCC1....................proved - incomplete [shostak](0.10 s)
atan2_cos_sin.........................proved - incomplete [shostak](0.89 s)
sin_atan2_TCC1........................proved - complete [shostak](0.02 s)
sin_atan2.............................proved - incomplete [shostak](0.74 s)
cos_atan2.............................proved - incomplete [shostak](0.81 s)
Theory totals: 34 formulas, 34 attempted, 34 succeeded (4.46 s)
Proof summary for theory trig_approx
sin_term_TCC1........................proved - complete [shostak]( 0.09 s)
sin_term_next........................proved - complete [shostak]( 0.55 s)
sin_term_neg.........................proved - complete [shostak]( 0.42 s)
sin_terms_alternate..................proved - complete [shostak]( 0.52 s)
sin_term_nonzero.....................proved - complete [shostak]( 0.19 s)
sin_term_zero........................proved - complete [shostak]( 0.03 s)
sin_term_gt0.........................proved - complete [shostak]( 0.62 s)
sin_term_lt0.........................proved - complete [shostak]( 0.06 s)
sin_tends_to_0.......................proved - complete [shostak]( 0.68 s)
cos_term_TCC1........................proved - complete [shostak]( 0.07 s)
cos_term_next........................proved - complete [shostak]( 0.93 s)
cos_term_neg.........................proved - complete [shostak]( 0.20 s)
cos_terms_alternate..................proved - complete [shostak]( 0.50 s)
cos_term_nonzero.....................proved - complete [shostak]( 0.17 s)
cos_term_zero........................proved - complete [shostak]( 0.04 s)
cos_term_gt0.........................proved - complete [shostak]( 0.43 s)
cos_term_lt0.........................proved - complete [shostak]( 0.48 s)
cos_tends_to_0.......................proved - complete [shostak]( 0.56 s)
sin_term_deriv_TCC1..................proved - complete [shostak]( 0.02 s)
sin_term_deriv_TCC2..................proved - complete [shostak]( 0.03 s)
sin_term_deriv.......................proved - complete [shostak]( 0.64 s)
cos_term_deriv_TCC1..................proved - complete [shostak]( 0.03 s)
cos_term_deriv.......................proved - complete [shostak]( 0.44 s)
sin_approx_TCC1......................proved - complete [shostak]( 0.47 s)
sin_approx_a0........................proved - complete [shostak]( 0.23 s)
sin_approx_neg.......................proved - complete [shostak]( 0.64 s)
sin_approx_next......................proved - complete [shostak]( 0.85 s)
sin_approx_eq........................proved - complete [shostak]( 0.24 s)
sin_approx_sin.......................proved - incomplete [shostak]( 1.23 s)
cos_approx_a0........................proved - complete [shostak]( 0.20 s)
cos_approx_neg.......................proved - complete [shostak]( 0.35 s)
cos_approx_cos.......................proved - incomplete [shostak]( 0.75 s)
cos_approx_next......................proved - complete [shostak]( 0.64 s)
cos_approx_eq........................proved - complete [shostak]( 0.24 s)
sin_approx_deriv.....................proved - complete [shostak]( 0.23 s)
cos_approx_deriv_TCC1................proved - complete [shostak]( 0.03 s)
cos_approx_deriv.....................proved - complete [shostak]( 0.54 s)
sin_lb_neg...........................proved - complete [shostak]( 0.12 s)
sin_ub_neg...........................proved - complete [shostak]( 0.04 s)
sin_lb_a0............................proved - complete [shostak]( 0.09 s)
sin_ub_a0............................proved - complete [shostak]( 0.07 s)
sin_lb_ub............................proved - complete [shostak]( 0.13 s)
sin_lb_inc...........................proved - complete [shostak]( 0.87 s)
sin_ub_dec...........................proved - complete [shostak]( 0.95 s)
sin_lb_lt............................proved - incomplete [shostak]( 0.83 s)
sin_ub_lt............................proved - incomplete [shostak]( 0.94 s)
sin_lb_gt............................proved - complete [shostak]( 1.83 s)
sin_ub_gt............................proved - complete [shostak]( 0.98 s)
sin_lb...............................proved - incomplete [shostak]( 0.70 s)
sin_ub...............................proved - incomplete [shostak]( 0.10 s)
sin_bounds...........................proved - incomplete [shostak]( 0.11 s)
sin_lb_gt0...........................proved - complete [shostak]( 0.70 s)
cos_lb_neg...........................proved - complete [shostak]( 0.08 s)
cos_ub_neg...........................proved - complete [shostak]( 0.07 s)
cos_lb_a0............................proved - complete [shostak]( 0.09 s)
cos_ub_a0............................proved - complete [shostak]( 0.08 s)
cos_lb_ub............................proved - complete [shostak]( 0.12 s)
cos_lb_inc...........................proved - complete [shostak]( 0.96 s)
cos_ub_dec...........................proved - complete [shostak]( 0.97 s)
cos_lb_lt............................proved - incomplete [shostak]( 1.12 s)
cos_ub_lt............................proved - incomplete [shostak]( 0.99 s)
cos_lb_gt............................proved - complete [shostak]( 1.15 s)
cos_ub_gt............................proved - complete [shostak]( 2.20 s)
cos_lb...............................proved - incomplete [shostak]( 0.36 s)
cos_ub...............................proved - incomplete [shostak]( 0.32 s)
cos_bounds...........................proved - incomplete [shostak]( 0.11 s)
sin_lb_deriv_TCC1....................proved - complete [shostak]( 0.03 s)
sin_lb_deriv_TCC2....................proved - complete [shostak]( 0.02 s)
sin_lb_deriv.........................proved - complete [shostak]( 0.60 s)
sin_ub_deriv.........................proved - complete [shostak]( 0.58 s)
cos_lb_deriv.........................proved - complete [shostak]( 0.11 s)
cos_ub_deriv_TCC1....................proved - complete [shostak]( 0.03 s)
cos_ub_deriv_TCC2....................proved - complete [shostak]( 0.03 s)
cos_ub_deriv.........................proved - complete [shostak]( 0.16 s)
cos_lb_nn_strict_decreasing..........proved - incomplete [shostak]( 0.40 s)
cos_lb_np_strict_increasing..........proved - incomplete [shostak]( 0.08 s)
sin_px...............................proved - incomplete [shostak]( 0.70 s)
cos_term_pi_lb.......................proved - incomplete [shostak](12.88 s)
cos_lb_pi2_eps.......................proved - incomplete [shostak]( 0.18 s)
cos_lb_pi2_pos0......................proved - complete [shostak]( 0.50 s)
cos_lb_pi2_pos1......................proved - complete [shostak]( 0.60 s)
cos_lb_pi2_pos2......................proved - complete [shostak]( 0.91 s)
cos_lb_pi2_pos.......................proved - incomplete [shostak]( 0.32 s)
sin_term_pi_lb.......................proved - incomplete [shostak](25.16 s)
sin_lb_pi_not_pos....................proved - complete [shostak]( 0.35 s)
sin_lb_pi_pos........................proved - incomplete [shostak]( 0.39 s)
pi_lb_est_TCC1.......................proved - complete [shostak]( 0.02 s)
pi_lb_est_TCC2.......................proved - incomplete [shostak]( 0.14 s)
pi_lb_est_TCC3.......................proved - incomplete [shostak]( 0.03 s)
pi_lb_est_le.........................proved - incomplete [shostak]( 0.10 s)
sin_lb_pi_est_pos....................proved - incomplete [shostak]( 0.57 s)
sin_lb_pi_range_pos..................proved - incomplete [shostak]( 0.90 s)
cos_ub_nn_strict_decreasing..........proved - incomplete [shostak]( 0.33 s)
cos_ub_np_strict_increasing..........proved - incomplete [shostak]( 0.06 s)
sin_lb_increasing....................proved - incomplete [shostak]( 1.31 s)
sin_ub_increasing....................proved - incomplete [shostak]( 1.41 s)
sin_lb_nn_decreasing.................proved - incomplete [shostak]( 0.32 s)
cos_term_pi_ub.......................proved - incomplete [shostak]( 5.69 s)
cos_ub_pi2_neg.......................proved - incomplete [shostak]( 0.38 s)
pi_ub_est_TCC1.......................proved - complete [shostak]( 0.02 s)
pi_ub_est_TCC2.......................proved - incomplete [shostak]( 0.26 s)
pi_ub_est_TCC3.......................proved - incomplete [shostak]( 0.18 s)
sin_ub_nn_decreasing.................proved - incomplete [shostak]( 0.42 s)
Theory totals: 103 formulas, 103 attempted, 103 succeeded (87.59 s)
Proof summary for theory exp_term
exp_term_TCC1.........................proved - complete [shostak](0.02 s)
exp_term_power_TCC1...................proved - complete [shostak](0.03 s)
exp_term_power........................proved - complete [shostak](1.29 s)
exp_term_decr.........................proved - complete [shostak](0.41 s)
tends_to_0?_TCC1......................proved - complete [shostak](0.02 s)
exp_tends_to_0........................proved - complete [shostak](3.21 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (4.98 s)
Proof summary for theory sincos
noa_nnreal_lt_pi2.....................proved - incomplete [shostak](0.06 s)
noa_real_lt_pi2.......................proved - incomplete [shostak](0.08 s)
noa_posreal_lt_pi.....................proved - incomplete [shostak](0.05 s)
noa_nnreal_pi4_to_pi..................proved - incomplete [shostak](0.11 s)
noa_posreal_pi2_to_pi.................proved - incomplete [shostak](0.09 s)
noa_nnreal_lt_pi4.....................proved - incomplete [shostak](0.07 s)
noa_mpi4_to_pi4.......................proved - incomplete [shostak](0.07 s)
conn_nnreal_lt_p2.....................proved - incomplete [shostak](0.03 s)
conn_nnreal_pi4_to_pi.................proved - incomplete [shostak](0.03 s)
conn_posreal_pi2_to_pi................proved - incomplete [shostak](0.03 s)
conn_nnreal_lt_pi4....................proved - incomplete [shostak](0.03 s)
deriv_domain_nnreal_lt_pi2............proved - incomplete [shostak](0.16 s)
deriv_domain_real_abs_lt_pi2..........proved - incomplete [shostak](0.06 s)
deriv_domain_posreal_pi2_to_pi........proved - incomplete [shostak](0.17 s)
deriv_domain_posreal_lt_pi............proved - incomplete [shostak](0.04 s)
deriv_domain_nnreal_pi4_to_pi.........proved - incomplete [shostak](0.16 s)
deriv_domain_nnreal_lt_pi4............proved - incomplete [shostak](0.15 s)
deriv_domain_mpi4_to_pi4..............proved - incomplete [shostak](0.06 s)
cos_ub................................proved - incomplete [shostak](0.03 s)
sin_ub................................proved - incomplete [shostak](0.63 s)
cos_lb................................proved - incomplete [shostak](5.78 s)
sin_lb................................proved - incomplete [shostak](4.83 s)
cos_pos_bnds..........................proved - incomplete [shostak](0.08 s)
sin_pos_bnds..........................proved - incomplete [shostak](0.08 s)
sin_convergence_TCC1..................proved - complete [shostak](0.02 s)
sin_convergence_TCC2..................proved - complete [shostak](0.02 s)
sin_convergence.......................proved - incomplete [shostak](1.29 s)
sin_derivable.........................proved - incomplete [shostak](0.03 s)
sin_derivable_fun.....................proved - incomplete [shostak](0.03 s)
deriv_sin_fun_TCC1....................proved - incomplete [shostak](0.02 s)
deriv_sin_fun.........................proved - incomplete [shostak](0.07 s)
cos_convergence.......................proved - incomplete [shostak](0.49 s)
cos_derivable.........................proved - incomplete [shostak](0.04 s)
cos_derivable_fun.....................proved - incomplete [shostak](0.03 s)
deriv_cos_fun_TCC1....................proved - incomplete [shostak](0.02 s)
deriv_cos_fun.........................proved - incomplete [shostak](0.06 s)
sin_continuous........................proved - incomplete [shostak](0.03 s)
cos_continuous........................proved - incomplete [shostak](0.03 s)
sin_cont_fun..........................proved - incomplete [shostak](0.03 s)
cos_cont_fun..........................proved - incomplete [shostak](0.02 s)
nderiv_sin_fun........................proved - incomplete [shostak](0.57 s)
nderiv_cos_fun........................proved - incomplete [shostak](0.41 s)
--> --------------------
--> maximum size reached
--> --------------------
[ Dauer der Verarbeitung: 1.160 Sekunden
]
|
|
