|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
open_sets.prf
Sprache: SML
Haftungsausschluß.summary KontaktMT940 {MT940[526] Hlasm[1444] Haskell[1746]}diese Dinge liegen außhalb unserer Verantwortung
***
*** top (16:29:0 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
trig_basic_ax.trig_phase_TCC1.........proved - by mapping [shostak](0.04 s)
trig_basic_ax.sin_range...............proved - by mapping [shostak](0.01 s)
trig_basic_ax.cos_range...............proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_TCC1................proved - by mapping [shostak](0.00 s)
trig_basic_ax.cos2....................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin2....................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_0...................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_pi2.................proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_0_TCC1..............proved - by mapping [shostak](0.01 s)
trig_basic_ax.tan_0...................proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_neg_TCC1............proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_neg.................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_cos.................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_shift...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_shift...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.neg_cos.................proved - by mapping [Untried]( n/a s)
trig_basic_ax.neg_sin.................proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_pi_TCC1.............proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_pi..................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_3pi2................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_3pi2................proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_2pi_TCC1............proved - by mapping [shostak](0.01 s)
trig_basic_ax.tan_2pi.................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_minus...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_plus................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_minus...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_pi_minus............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_pi_minus............proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_plus_TCC1...........proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_plus................proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_minus_TCC1..........proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_minus...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.pythagorean.............proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_2a..................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_2a..................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_2a_cos..............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_2a_sin..............proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_2a_TCC1.............proved - by mapping [shostak](0.01 s)
trig_basic_ax.tan_2a..................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_period..............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_period..............proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_period_TCC1.........proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_period..............proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_k_pi................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_2k_pi...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_k_pi................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_k_pi2...............proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_k_pi_TCC1...........proved - by mapping [shostak](0.00 s)
trig_basic_ax.tan_k_pi................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_eq_0................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_eq_0_2pi............proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_eq_0_2pi............proved - by mapping [Untried]( n/a s)
trig_basic_ax.tan_eq_0................proved - by mapping [Untried]( n/a s)
trig_basic_ax.sin_eq_1................proved - by mapping [Untried]( n/a s)
trig_basic_ax.cos_eq_1................proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_cos_pi4............proved - by mapping [Untried]( n/a s)
trig_values_ax.cos_pi4................proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_pi4................proved - by mapping [Untried]( n/a s)
trig_values_ax.cos_3pi4...............proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_3pi4...............proved - by mapping [Untried]( n/a s)
trig_values_ax.tan_pi4_TCC1...........proved - by mapping [shostak](0.01 s)
trig_values_ax.tan_pi4................proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_pi3_cos_pi6........proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_pi6_cos_pi3........proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_pi6................proved - by mapping [Untried]( n/a s)
trig_values_ax.cos_pi6................proved - by mapping [Untried]( n/a s)
trig_values_ax.tan_pi6_TCC1...........proved - by mapping [shostak](0.00 s)
trig_values_ax.tan_pi6................proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_pi3................proved - by mapping [Untried]( n/a s)
trig_values_ax.cos_pi3................proved - by mapping [Untried]( n/a s)
trig_values_ax.tan_pi3_TCC1...........proved - by mapping [shostak](0.00 s)
trig_values_ax.tan_pi3................proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_2pi3...............proved - by mapping [Untried]( n/a s)
trig_values_ax.cos_2pi3...............proved - by mapping [Untried]( n/a s)
trig_values_ax.tan_2pi3_TCC1..........proved - by mapping [shostak](0.01 s)
trig_values_ax.tan_2pi3...............proved - by mapping [Untried]( n/a s)
trig_values_ax.cos_5pi4...............proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_5pi4...............proved - by mapping [Untried]( n/a s)
trig_values_ax.sin_cos_5pi4...........proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_gt_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_ge_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_ge_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_lt_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_lt_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_le_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_le_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_gt_0_TCC1............proved - by mapping [shostak](0.00 s)
trig_ineq_ax.tan_gt_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_lt_0_TCC1............proved - by mapping [shostak](0.00 s)
trig_ineq_ax.tan_lt_0.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_pi2_def..............proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_npi_def..............proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_ge_0_3pi2............proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_increasing_imp.......proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_increasing...........proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_decreasing...........proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_increasing...........proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_decreasing...........proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_increasing_imp_TCC1...proved - by mapping [shostak](0.01 s)
trig_ineq_ax.tan_increasing_imp_TCC2...proved - by mapping [shostak](0.00 s)
trig_ineq_ax.tan_increasing_imp.......proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_increasing_TCC1......proved - by mapping [shostak](0.00 s)
trig_ineq_ax.tan_increasing_TCC2......proved - by mapping [shostak](0.00 s)
trig_ineq_ax.tan_increasing...........proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_incr.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_decr.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_incr.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.cos_decr.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.tan_incr.................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_gt...................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_lt...................proved - by mapping [Untried]( n/a s)
trig_ineq_ax.sin_ge...................proved - by mapping [Untried]( n/a s)
Theory totals: 112 formulas, 112 attempted, 112 succeeded (0.11 s)
Proof summary for theory trig_basic
pi_TCC1...............................proved - complete [shostak](0.14 s)
trig_phase_TCC1.......................proved - complete [shostak](0.03 s)
sin_range.............................proved - complete [shostak](0.01 s)
cos_range.............................proved - complete [shostak](0.00 s)
tan_TCC1..............................proved - complete [shostak](0.01 s)
cos2..................................proved - complete [shostak](0.04 s)
sin2..................................proved - complete [shostak](0.03 s)
sin_0.................................proved - complete [shostak](0.02 s)
cos_pi2...............................proved - complete [shostak](0.06 s)
tan_0_TCC1............................proved - complete [shostak](0.01 s)
tan_0.................................proved - complete [shostak](0.01 s)
tan_neg_TCC1..........................proved - complete [shostak](0.01 s)
tan_neg...............................proved - complete [shostak](0.03 s)
sin_cos...............................proved - complete [shostak](0.05 s)
sin_shift.............................proved - complete [shostak](0.05 s)
cos_shift.............................proved - complete [shostak](0.03 s)
neg_cos...............................proved - complete [shostak](0.09 s)
neg_sin...............................proved - complete [shostak](0.09 s)
tan_pi_TCC1...........................proved - complete [shostak](0.01 s)
tan_pi................................proved - complete [shostak](0.03 s)
sin_3pi2..............................proved - complete [shostak](0.06 s)
cos_3pi2..............................proved - complete [shostak](0.06 s)
tan_2pi_TCC1..........................proved - complete [shostak](0.01 s)
tan_2pi...............................proved - complete [shostak](0.04 s)
sin_minus.............................proved - complete [shostak](0.07 s)
cos_plus..............................proved - complete [shostak](0.10 s)
cos_minus.............................proved - complete [shostak](0.06 s)
sin_pi_minus..........................proved - complete [shostak](0.06 s)
cos_pi_minus..........................proved - complete [shostak](0.07 s)
tan_plus_TCC1.........................proved - complete [shostak](0.03 s)
tan_plus..............................proved - complete [shostak](0.12 s)
tan_minus_TCC1........................proved - complete [shostak](0.05 s)
tan_minus.............................proved - complete [shostak](0.10 s)
pythagorean...........................proved - complete [shostak](0.13 s)
sin_2a................................proved - complete [shostak](0.06 s)
cos_2a................................proved - complete [shostak](0.05 s)
cos_2a_cos............................proved - complete [shostak](0.09 s)
cos_2a_sin............................proved - complete [shostak](0.05 s)
tan_2a_TCC1...........................proved - complete [shostak](0.04 s)
tan_2a................................proved - complete [shostak](0.06 s)
sin_period............................proved - complete [shostak](0.32 s)
cos_period............................proved - complete [shostak](0.12 s)
tan_period_TCC1.......................proved - complete [shostak](0.24 s)
tan_period............................proved - complete [shostak](0.26 s)
sin_k_pi..............................proved - complete [shostak](0.18 s)
cos_2k_pi.............................proved - complete [shostak](0.09 s)
cos_k_pi..............................proved - complete [shostak](0.22 s)
sin_k_pi2.............................proved - complete [shostak](0.09 s)
tan_k_pi_TCC1.........................proved - complete [shostak](0.05 s)
tan_k_pi..............................proved - complete [shostak](0.05 s)
cos_eq_0..............................proved - complete [shostak](0.14 s)
sin_eq_0_2pi..........................proved - complete [shostak](0.09 s)
cos_eq_0_2pi..........................proved - complete [shostak](0.15 s)
tan_eq_0..............................proved - complete [shostak](0.08 s)
sin_eq_1..............................proved - complete [shostak](0.43 s)
cos_eq_1..............................proved - complete [shostak](0.16 s)
Theory totals: 56 formulas, 56 attempted, 56 succeeded (4.68 s)
Proof summary for theory trig_values
sin_cos_pi4...........................proved - complete [shostak](0.04 s)
cos_pi4...............................proved - complete [shostak](0.23 s)
sin_pi4...............................proved - complete [shostak](0.04 s)
cos_3pi4..............................proved - complete [shostak](0.17 s)
sin_3pi4..............................proved - complete [shostak](0.16 s)
tan_pi4_TCC1..........................proved - complete [shostak](0.04 s)
tan_pi4...............................proved - complete [shostak](0.04 s)
sin_pi3_cos_pi6.......................proved - complete [shostak](0.03 s)
sin_pi6_cos_pi3.......................proved - complete [shostak](0.04 s)
sin_pi6...............................proved - complete [shostak](0.22 s)
cos_pi6...............................proved - complete [shostak](0.49 s)
tan_pi6_TCC1..........................proved - complete [shostak](0.02 s)
tan_pi6...............................proved - complete [shostak](0.05 s)
sin_pi3...............................proved - complete [shostak](0.02 s)
cos_pi3...............................proved - complete [shostak](0.02 s)
tan_pi3_TCC1..........................proved - complete [shostak](0.02 s)
tan_pi3...............................proved - complete [shostak](0.05 s)
sin_2pi3..............................proved - complete [shostak](0.10 s)
cos_2pi3..............................proved - complete [shostak](0.12 s)
tan_2pi3_TCC1.........................proved - complete [shostak](0.14 s)
tan_2pi3..............................proved - complete [shostak](0.07 s)
cos_5pi4..............................proved - complete [shostak](0.14 s)
sin_5pi4..............................proved - complete [shostak](0.16 s)
sin_cos_5pi4..........................proved - complete [shostak](0.06 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (2.47 s)
Proof summary for theory trig_ineq
sin_gt_0..............................proved - complete [shostak](0.05 s)
sin_ge_0..............................proved - complete [shostak](0.02 s)
cos_ge_0..............................proved - complete [shostak](0.06 s)
sin_lt_0..............................proved - complete [shostak](0.06 s)
cos_lt_0..............................proved - complete [shostak](0.07 s)
sin_le_0..............................proved - complete [shostak](0.05 s)
cos_le_0..............................proved - complete [shostak](0.07 s)
tan_gt_0_TCC1.........................proved - complete [shostak](0.06 s)
tan_gt_0..............................proved - complete [shostak](0.05 s)
tan_lt_0_TCC1.........................proved - complete [shostak](0.06 s)
tan_lt_0..............................proved - complete [shostak](0.04 s)
tan_pi2_def...........................proved - complete [shostak](0.04 s)
tan_npi_def...........................proved - complete [shostak](0.03 s)
cos_ge_0_3pi2.........................proved - complete [shostak](0.15 s)
sin_increasing_imp....................proved - complete [shostak](0.16 s)
sin_increasing........................proved - complete [shostak](0.05 s)
sin_decreasing........................proved - complete [shostak](0.23 s)
cos_increasing........................proved - complete [shostak](0.19 s)
cos_decreasing........................proved - complete [shostak](0.17 s)
tan_increasing_imp_TCC1...............proved - complete [shostak](0.01 s)
tan_increasing_imp_TCC2...............proved - complete [shostak](0.01 s)
tan_increasing_imp....................proved - complete [shostak](0.26 s)
tan_increasing_TCC1...................proved - complete [shostak](0.00 s)
tan_increasing_TCC2...................proved - complete [shostak](0.01 s)
tan_increasing........................proved - complete [shostak](0.05 s)
sin_incr..............................proved - complete [shostak](0.04 s)
sin_decr..............................proved - complete [shostak](0.08 s)
cos_incr..............................proved - complete [shostak](0.03 s)
cos_decr..............................proved - complete [shostak](0.03 s)
tan_incr..............................proved - complete [shostak](0.02 s)
sin_gt................................proved - complete [shostak](0.13 s)
sin_lt................................proved - complete [shostak](0.12 s)
sin_ge................................proved - complete [shostak](0.05 s)
Theory totals: 33 formulas, 33 attempted, 33 succeeded (2.38 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 - complete [shostak](0.08 s)
cos_minus_2pi.........................proved - complete [shostak](0.08 s)
tan_minus_2pi_TCC1....................proved - complete [shostak](0.04 s)
tan_minus_2pi_TCC2....................proved - complete [shostak](0.01 s)
tan_minus_2pi.........................proved - complete [shostak](0.05 s)
sin_minus_3pi2........................proved - complete [shostak](0.09 s)
cos_minus_3pi2........................proved - complete [shostak](0.09 s)
tan_minus_3pi2_TCC1...................proved - complete [shostak](0.11 s)
tan_minus_3pi2_TCC2...................proved - complete [shostak](0.01 s)
tan_minus_3pi2........................proved - complete [shostak](0.07 s)
sin_minus_pi..........................proved - complete [shostak](0.06 s)
cos_minus_pi..........................proved - complete [shostak](0.05 s)
tan_minus_pi_TCC1.....................proved - complete [shostak](0.03 s)
tan_minus_pi..........................proved - complete [shostak](0.04 s)
sin_minus_pi2.........................proved - complete [shostak](0.08 s)
cos_minus_pi2.........................proved - complete [shostak](0.07 s)
tan_minus_pi2_TCC1....................proved - complete [shostak](0.04 s)
tan_minus_pi2.........................proved - complete [shostak](0.06 s)
sin_2pi_minus.........................proved - complete [shostak](0.08 s)
cos_2pi_minus.........................proved - complete [shostak](0.09 s)
tan_2pi_minus_TCC1....................proved - complete [shostak](0.04 s)
tan_2pi_minus.........................proved - complete [shostak](0.06 s)
sin_3pi2_minus........................proved - complete [shostak](0.10 s)
cos_3pi2_minus........................proved - complete [shostak](0.10 s)
tan_3pi2_minus_TCC1...................proved - complete [shostak](0.09 s)
tan_3pi2_minus........................proved - complete [shostak](0.07 s)
sin_pi_minus..........................proved - complete [shostak](0.06 s)
cos_pi_minus..........................proved - complete [shostak](0.07 s)
tan_pi_minus_TCC1.....................proved - complete [shostak](0.03 s)
tan_pi_minus..........................proved - complete [shostak](0.05 s)
sin_pi2_minus.........................proved - complete [shostak](0.07 s)
cos_pi2_minus.........................proved - complete [shostak](0.09 s)
tan_pi2_minus_TCC1....................proved - complete [shostak](0.05 s)
tan_pi2_minus.........................proved - complete [shostak](0.07 s)
sin_times_cos.........................proved - complete [shostak](0.09 s)
cos_times_cos.........................proved - complete [shostak](0.08 s)
sin_times_sin.........................proved - complete [shostak](0.08 s)
sin_sum...............................proved - complete [shostak](0.09 s)
sin_diff..............................proved - complete [shostak](0.09 s)
cos_sum...............................proved - complete [shostak](0.25 s)
cos_diff..............................proved - complete [shostak](0.24 s)
tan_diff_TCC1.........................proved - complete [shostak](0.01 s)
tan_diff..............................proved - complete [shostak](0.13 s)
sq_sin................................proved - complete [shostak](0.07 s)
sq_cos................................proved - complete [shostak](0.09 s)
sin_half_zeroes.......................proved - complete [shostak](0.06 s)
cos_half_zeroes.......................proved - complete [shostak](0.08 s)
cos_half_zeroes2......................proved - complete [shostak](0.05 s)
sq_tan_TCC1...........................proved - complete [shostak](0.04 s)
sq_tan................................proved - complete [shostak](0.17 s)
sin_half_TCC1.........................proved - complete [shostak](0.02 s)
sin_half_TCC2.........................proved - complete [shostak](0.04 s)
sin_half..............................proved - complete [shostak](0.14 s)
cos_half_TCC1.........................proved - complete [shostak](0.05 s)
cos_half_TCC2.........................proved - complete [shostak](0.06 s)
cos_half_TCC3.........................proved - complete [shostak](0.06 s)
cos_half..............................proved - complete [shostak](0.29 s)
tan_half_TCC1.........................proved - complete [shostak](0.07 s)
tan_half_TCC2.........................proved - complete [shostak](0.04 s)
tan_half..............................proved - complete [shostak](0.12 s)
tan_half2_TCC1........................proved - complete [shostak](0.03 s)
tan_half2.............................proved - complete [shostak](0.09 s)
sin_3a................................proved - complete [shostak](0.23 s)
cos_3a................................proved - complete [shostak](0.19 s)
sin_eq_sin............................proved - complete [shostak](0.52 s)
cos_eq_cos............................proved - complete [shostak](0.36 s)
tan_eq_tan............................proved - complete [shostak](0.20 s)
sin_cos_eq............................proved - complete [shostak](0.44 s)
sin_eq_cos............................proved - complete [shostak](0.18 s)
tan_eq_1..............................proved - complete [shostak](0.02 s)
sin_eq_pm1............................proved - complete [shostak](0.28 s)
cos_eq_pm1............................proved - complete [shostak](0.23 s)
sin_plus_cos..........................proved - complete [shostak](0.13 s)
spc_tan_prep..........................proved - complete [shostak](0.40 s)
sin_plus_cos_atan2_TCC1...............proved - complete [shostak](0.01 s)
sin_plus_cos_atan2....................proved - complete [shostak](0.49 s)
Theory totals: 76 formulas, 76 attempted, 76 succeeded (8.46 s)
Proof summary for theory atan2
atan2_TCC1............................proved - complete [shostak](0.01 s)
atan2_TCC2............................proved - complete [shostak](0.02 s)
atan2_TCC3............................proved - complete [shostak](0.01 s)
atan2_0_2pi_TCC1......................proved - complete [shostak](0.01 s)
atan2_0_2pi_TCC2......................proved - complete [shostak](0.06 s)
atan2_0_2pi_TCC3......................proved - complete [shostak](0.01 s)
atan2_0_2pi_TCC4......................proved - complete [shostak](0.01 s)
atan2_0_2pi...........................proved - complete [shostak](0.31 s)
atan2_ge_0_lt_2pi_TCC1................proved - complete [shostak](0.01 s)
atan2_ge_0_lt_2pi.....................proved - complete [shostak](0.12 s)
nnreal_lt_2pi_TCC1....................proved - complete [shostak](0.05 s)
atan2_TCC4............................proved - complete [shostak](0.01 s)
atan2_cancel_pos_TCC1.................proved - complete [shostak](0.07 s)
atan2_cancel_pos......................proved - complete [shostak](0.21 s)
atan2_cancel_neg_TCC1.................proved - complete [shostak](0.07 s)
atan2_cancel_neg......................proved - complete [shostak](0.42 s)
atan2_swap_pos_TCC1...................proved - complete [shostak](0.03 s)
atan2_swap_pos_TCC2...................proved - complete [shostak](0.01 s)
atan2_swap_pos_TCC3...................proved - complete [shostak](0.01 s)
atan2_swap_pos_TCC4...................proved - complete [shostak](0.06 s)
atan2_swap_pos........................proved - complete [shostak](0.36 s)
atan2_swap_neg_TCC1...................proved - complete [shostak](0.04 s)
atan2_swap_neg_TCC2...................proved - complete [shostak](0.01 s)
atan2_swap_neg_TCC3...................proved - complete [shostak](0.00 s)
atan2_swap_neg_TCC4...................proved - complete [shostak](0.06 s)
atan2_swap_neg........................proved - complete [shostak](0.43 s)
atan2_swap_zero_TCC1..................proved - complete [shostak](0.01 s)
atan2_swap_zero_TCC2..................proved - complete [shostak](0.04 s)
atan2_swap_zero.......................proved - complete [shostak](0.16 s)
atan2_cos_sin_TCC1....................proved - complete [shostak](0.07 s)
sin_atan2_TCC1........................proved - complete [shostak](0.01 s)
Theory totals: 31 formulas, 31 attempted, 31 succeeded (2.70 s)
Proof summary for theory atan
real_abs_lt_pi2_TCC1..................proved - complete [shostak](0.03 s)
acot_TCC1.............................proved - complete [shostak](0.06 s)
acot_neg..............................proved - complete [shostak](0.05 s)
atan_minus_TCC1.......................proved - complete [shostak](0.04 s)
atan_minus_TCC2.......................proved - complete [shostak](0.04 s)
atan_minus_TCC3.......................proved - complete [shostak](0.10 s)
atan_plus_TCC1........................proved - complete [shostak](0.04 s)
atan_plus_TCC2........................proved - complete [shostak](0.03 s)
atan_plus_TCC3........................proved - complete [shostak](0.02 s)
atan_plus.............................proved - complete [shostak](0.22 s)
atan_sub_swap_TCC1....................proved - complete [shostak](0.00 s)
atan_sub_swap_TCC2....................proved - complete [shostak](0.01 s)
atan_sub_swap_TCC3....................proved - complete [shostak](0.07 s)
atan_sub_swap.........................proved - complete [shostak](0.23 s)
atan_1................................proved - complete [shostak](0.25 s)
pi_bnds...............................proved - complete [shostak](0.17 s)
atan_series_term_TCC1.................proved - complete [shostak](0.04 s)
atan_series_n_TCC1....................proved - complete [shostak](0.01 s)
atan_series_n_TCC2....................proved - complete [shostak](0.00 s)
atan_series_n_TCC3....................proved - complete [shostak](0.02 s)
atan_series_TCC1......................proved - complete [shostak](0.04 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (1.46 s)
Proof summary for theory trig_approx
sin_term_TCC1........................proved - complete [shostak]( 0.06 s)
sin_term_next........................proved - complete [shostak]( 0.52 s)
sin_term_neg.........................proved - complete [shostak]( 0.38 s)
sin_terms_alternate..................proved - complete [shostak]( 0.46 s)
sin_term_nonzero.....................proved - complete [shostak]( 0.16 s)
sin_term_zero........................proved - complete [shostak]( 0.01 s)
sin_term_gt0.........................proved - complete [shostak]( 0.55 s)
sin_term_lt0.........................proved - complete [shostak]( 0.04 s)
sin_tends_to_0.......................proved - complete [shostak]( 0.69 s)
cos_term_TCC1........................proved - complete [shostak]( 0.04 s)
cos_term_next........................proved - complete [shostak]( 0.88 s)
cos_term_neg.........................proved - complete [shostak]( 0.18 s)
cos_terms_alternate..................proved - complete [shostak]( 0.46 s)
cos_term_nonzero.....................proved - complete [shostak]( 0.16 s)
cos_term_zero........................proved - complete [shostak]( 0.01 s)
cos_term_gt0.........................proved - complete [shostak]( 0.36 s)
cos_term_lt0.........................proved - complete [shostak]( 0.40 s)
cos_tends_to_0.......................proved - complete [shostak]( 0.56 s)
sin_approx_TCC1......................proved - complete [shostak]( 0.00 s)
sin_approx_a0........................proved - complete [shostak]( 0.18 s)
sin_approx_neg.......................proved - complete [shostak]( 0.58 s)
sin_approx_next......................proved - complete [shostak]( 0.79 s)
sin_approx_eq........................proved - complete [shostak]( 0.22 s)
sin_approx_sin.......................proved - complete [shostak]( 0.82 s)
cos_approx_a0........................proved - complete [shostak]( 0.17 s)
cos_approx_neg.......................proved - complete [shostak]( 0.31 s)
cos_approx_cos.......................proved - complete [shostak]( 0.70 s)
cos_approx_next......................proved - complete [shostak]( 0.59 s)
cos_approx_eq........................proved - complete [shostak]( 0.22 s)
sin_lb_neg...........................proved - complete [shostak]( 0.09 s)
sin_ub_neg...........................proved - complete [shostak]( 0.02 s)
sin_lb_a0............................proved - complete [shostak]( 0.06 s)
sin_ub_a0............................proved - complete [shostak]( 0.05 s)
sin_lb_ub............................proved - complete [shostak]( 0.11 s)
sin_lb_inc...........................proved - complete [shostak]( 0.79 s)
sin_ub_dec...........................proved - complete [shostak]( 0.88 s)
sin_lb_lt............................proved - complete [shostak]( 0.76 s)
sin_ub_lt............................proved - complete [shostak]( 0.89 s)
sin_lb_gt............................proved - complete [shostak]( 1.65 s)
sin_ub_gt............................proved - complete [shostak]( 0.89 s)
sin_lb...............................proved - complete [shostak]( 0.64 s)
sin_ub...............................proved - complete [shostak]( 0.06 s)
sin_bounds...........................proved - complete [shostak]( 0.08 s)
sin_lb_gt0...........................proved - complete [shostak]( 0.66 s)
cos_lb_neg...........................proved - complete [shostak]( 0.06 s)
cos_ub_neg...........................proved - complete [shostak]( 0.05 s)
cos_lb_a0............................proved - complete [shostak]( 0.07 s)
cos_ub_a0............................proved - complete [shostak]( 0.05 s)
cos_lb_ub............................proved - complete [shostak]( 0.09 s)
cos_lb_inc...........................proved - complete [shostak]( 0.88 s)
cos_ub_dec...........................proved - complete [shostak]( 0.87 s)
cos_lb_lt............................proved - complete [shostak]( 1.03 s)
cos_ub_lt............................proved - complete [shostak]( 0.94 s)
cos_lb_gt............................proved - complete [shostak]( 1.07 s)
cos_ub_gt............................proved - complete [shostak]( 2.01 s)
cos_lb...............................proved - complete [shostak]( 0.31 s)
cos_ub...............................proved - complete [shostak]( 0.28 s)
cos_bounds...........................proved - complete [shostak]( 0.09 s)
cos_lb_np_strict_increasing..........proved - complete [shostak]( 0.04 s)
sin_px...............................proved - complete [shostak]( 0.64 s)
cos_term_pi_lb.......................proved - complete [shostak](12.04 s)
cos_lb_pi2_eps.......................proved - complete [shostak]( 0.16 s)
cos_lb_pi2_pos0......................proved - complete [shostak]( 0.45 s)
cos_lb_pi2_pos1......................proved - complete [shostak]( 0.57 s)
cos_lb_pi2_pos2......................proved - complete [shostak]( 0.85 s)
cos_lb_pi2_pos.......................proved - complete [shostak]( 0.28 s)
Theory totals: 66 formulas, 66 attempted, 66 succeeded (41.01 s)
Proof summary for theory sincos
sin_derivable_TCC1....................proved - complete [shostak](0.01 s)
sin_derivable_TCC2....................proved - complete [shostak](0.00 s)
sin_derivable_fun.....................proved - complete [shostak](0.01 s)
deriv_sin_fun_TCC1....................proved - complete [shostak](0.00 s)
cos_derivable_fun.....................proved - complete [shostak](0.00 s)
deriv_cos_fun_TCC1....................proved - complete [shostak](0.01 s)
sin_continuous_fun....................proved - complete [shostak](0.00 s)
cos_continuous_fun....................proved - complete [shostak](0.01 s)
sin_taylors_TCC1......................proved - complete [shostak](0.06 s)
sin_taylors_TCC2......................proved - complete [shostak](0.05 s)
sin_taylors...........................proved - complete [shostak](1.21 s)
cos_taylors_TCC1......................proved - complete [shostak](0.06 s)
cos_taylors_TCC2......................proved - complete [shostak](0.05 s)
cos_taylors...........................proved - complete [shostak](0.17 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.63 s)
Proof summary for theory sincos_def
cos_ub................................proved - complete [shostak](0.01 s)
cos_pos_bnds..........................proved - complete [shostak](0.05 s)
sin_pos_bnds..........................proved - complete [shostak](0.06 s)
sin_series_term_TCC1..................proved - complete [shostak](0.04 s)
sin_series_n_TCC1.....................proved - complete [shostak](0.01 s)
cos_series_term_TCC1..................proved - complete [shostak](0.00 s)
sin_series_TCC1.......................proved - complete [shostak](0.04 s)
cos_series_TCC1.......................proved - complete [shostak](0.05 s)
tan_atan_TCC1.........................proved - complete [shostak](0.04 s)
atan_tan_TCC1.........................proved - complete [shostak](0.05 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.36 s)
Proof summary for theory taylor_help
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory asin
real_abs_le_pi2_TCC1..................proved - complete [shostak](0.03 s)
asin_TCC1.............................proved - complete [shostak](0.03 s)
asin_TCC2.............................proved - complete [shostak](0.13 s)
asin_TCC3.............................proved - complete [shostak](0.06 s)
asin_TCC4.............................proved - complete [shostak](0.19 s)
asin_TCC5.............................proved - complete [shostak](0.05 s)
asin_neg_restrict_TCC1................proved - complete [shostak](0.08 s)
asin_neg_restrict_TCC2................proved - complete [shostak](0.00 s)
asin_neg_restrict.....................proved - complete [shostak](0.35 s)
asin_pos_restrict_TCC1................proved - complete [shostak](0.05 s)
asin_pos_restrict_TCC2................proved - complete [shostak](0.01 s)
asin_pos_restrict.....................proved - complete [shostak](0.37 s)
asin_0................................proved - complete [shostak](0.01 s)
asin_sqrt_half_TCC1...................proved - complete [shostak](0.09 s)
asin_sqrt_half........................proved - complete [shostak](0.16 s)
asin_1................................proved - complete [shostak](0.01 s)
asin_neg_TCC1.........................proved - complete [shostak](0.00 s)
asin_neg..............................proved - complete [shostak](0.15 s)
asin_minus1...........................proved - complete [shostak](0.01 s)
asin_minus_sqrt_half_TCC1.............proved - complete [shostak](0.08 s)
asin_minus_sqrt_half..................proved - complete [shostak](0.06 s)
asin_strict_increasing................proved - complete [shostak](1.44 s)
asin_bij..............................proved - complete [shostak](0.99 s)
asin_diff_TCC1........................proved - complete [shostak](0.01 s)
asin_diff_TCC2........................proved - complete [shostak](0.02 s)
asin_diff_TCC3........................proved - complete [shostak](0.28 s)
asin_diff.............................proved - complete [shostak](3.01 s)
asin_pos_bnds_TCC1....................proved - complete [shostak](0.17 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (7.85 s)
Proof summary for theory acos
nnreal_le_pi_TCC1.....................proved - complete [shostak](0.00 s)
acos_TCC1.............................proved - complete [shostak](0.05 s)
acos_neg_TCC1.........................proved - complete [shostak](0.01 s)
acos_neg..............................proved - complete [shostak](0.04 s)
acos_0................................proved - complete [shostak](0.05 s)
acos_sqrt_half_TCC1...................proved - complete [shostak](0.06 s)
acos_sqrt_half........................proved - complete [shostak](0.03 s)
acos_1................................proved - complete [shostak](0.03 s)
acos_minus1...........................proved - complete [shostak](0.04 s)
acos_minus_sqrt_half_TCC1.............proved - complete [shostak](0.04 s)
acos_minus_sqrt_half..................proved - complete [shostak](0.06 s)
acos_strict_decreasing................proved - complete [shostak](0.05 s)
acos_bij..............................proved - complete [shostak](0.12 s)
acos_sum_TCC1.........................proved - complete [shostak](0.02 s)
acos_sum_TCC2.........................proved - complete [shostak](0.05 s)
acos_sum_TCC3.........................proved - complete [shostak](0.28 s)
acos_sum..............................proved - complete [shostak](9.34 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (10.27 s)
Proof summary for theory exp_term
exp_term_TCC1.........................proved - complete [shostak](0.00 s)
exp_term_power_TCC1...................proved - complete [shostak](0.01 s)
exp_term_power........................proved - complete [shostak](1.23 s)
exp_term_decr.........................proved - complete [shostak](0.40 s)
tends_to_0?_TCC1......................proved - complete [shostak](0.00 s)
exp_tends_to_0........................proved - complete [shostak](3.02 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (4.65 s)
Proof summary for theory atan_approx
atan_pos_le1_ub_lt....................proved - complete [shostak](0.55 s)
atan_pos_le1_lb_lt....................proved - complete [shostak](0.57 s)
atan_pos_le1_lb_inc...................proved - complete [shostak](0.66 s)
atan_pos_le1_ub_dec...................proved - complete [shostak](1.71 s)
pi_lbn_lt.............................proved - complete [shostak](0.12 s)
pi_lbn_LT.............................proved - complete [shostak](0.10 s)
pi_lb_pos.............................proved - complete [shostak](0.21 s)
pi_ub_pos.............................proved - complete [shostak](0.01 s)
pi_bounds0............................proved - complete [shostak](0.25 s)
pi_bounds2............................proved - complete [shostak](0.62 s)
pi_bound..............................proved - complete [shostak](0.01 s)
pi_lb_inc.............................proved - complete [shostak](0.06 s)
pi_ub_dec.............................proved - complete [shostak](0.06 s)
atan_pos_bounds_TCC1..................proved - complete [shostak](0.02 s)
atan_pos_bounds.......................proved - complete [shostak](0.12 s)
atan_lb_TCC1..........................proved - complete [shostak](0.01 s)
atan_lb_TCC2..........................proved - complete [shostak](0.01 s)
atan_bounds...........................proved - complete [shostak](0.06 s)
atan_pos_lb_inc.......................proved - complete [shostak](0.08 s)
atan_pos_ub_dec.......................proved - complete [shostak](0.08 s)
pi_lb_diff............................proved - complete [shostak](2.02 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (7.34 s)
Proof summary for theory tan_approx
tan_lb_ub_TCC1........................proved - complete [shostak](0.01 s)
tan_ub_lb_TCC1........................proved - complete [shostak](0.12 s)
tan_lb_ub_neg_TCC1....................proved - complete [shostak](0.01 s)
tan_lb_ub_neg.........................proved - complete [shostak](0.03 s)
tan_ub_lb_neg_TCC1....................proved - complete [shostak](0.02 s)
tan_ub_lb_neg.........................proved - complete [shostak](0.03 s)
tan_lb_lb_neg.........................proved - complete [shostak](0.03 s)
tan_ub_ub_neg.........................proved - complete [shostak](0.03 s)
tan_bounds_0_pi2_TCC1.................proved - complete [shostak](0.04 s)
tan_bounds_0_pi2_TCC2.................proved - complete [shostak](0.05 s)
tan_bounds_0_pi2_TCC3.................proved - complete [shostak](0.03 s)
tan_bounds_0_pi2......................proved - complete [shostak](1.29 s)
tan_bounds_npi2_0_TCC1................proved - complete [shostak](0.03 s)
tan_bounds_npi2_0_TCC2................proved - complete [shostak](0.04 s)
tan_bounds_npi2_0_TCC3................proved - complete [shostak](0.03 s)
tan_bounds_npi2_0.....................proved - complete [shostak](0.10 s)
tan_bounds_pi2_pi_TCC1................proved - complete [shostak](0.03 s)
tan_bounds_pi2_pi_TCC2................proved - complete [shostak](0.03 s)
tan_bounds_pi2_pi_TCC3................proved - complete [shostak](0.04 s)
tan_bounds_pi2_pi.....................proved - complete [shostak](1.35 s)
tan_bounds_npi_npi2_TCC1..............proved - complete [shostak](0.04 s)
tan_bounds_npi_npi2_TCC2..............proved - complete [shostak](0.03 s)
tan_bounds_npi_npi2_TCC3..............proved - complete [shostak](0.03 s)
tan_bounds_npi_npi2...................proved - complete [shostak](0.10 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (3.55 s)
Proof summary for theory law_cosines
distance_refl.........................proved - complete [shostak](0.00 s)
distance_symm.........................proved - complete [shostak](0.17 s)
distance_trans........................proved - complete [shostak](0.02 s)
distance_scale........................proved - complete [shostak](0.25 s)
distance_rot..........................proved - complete [shostak](0.46 s)
Law_Cosines...........................proved - complete [shostak](1.37 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.27 s)
Proof summary for theory trig_degree
rad_deg...............................proved - complete [shostak](0.04 s)
deg_rad...............................proved - complete [shostak](0.05 s)
tand_TCC1.............................proved - complete [shostak](0.03 s)
sq_sin_cos_d_one......................proved - complete [shostak](0.06 s)
sind_bounds...........................proved - complete [shostak](1.40 s)
cosd_bounds...........................proved - complete [shostak](0.78 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.36 s)
Proof summary for theory trig_inverses
atan_prep.............................proved - complete [shostak](0.22 s)
tan_atan_TCC1.........................proved - complete [shostak](0.01 s)
atan_tan_TCC1.........................proved - complete [shostak](0.02 s)
arcsin_TCC1...........................proved - complete [shostak](0.00 s)
arccos_TCC1...........................proved - complete [shostak](0.01 s)
arctan_prep...........................proved - complete [shostak](0.14 s)
arctan_TCC1...........................proved - complete [shostak](0.00 s)
tan_arctan_TCC1.......................proved - complete [shostak](0.01 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.41 s)
Proof summary for theory trig_rew
tr_rew1...............................proved - complete [shostak](0.00 s)
tr_rew2...............................proved - complete [shostak](0.01 s)
tr_rew3...............................proved - complete [shostak](0.00 s)
tr_rew4...............................proved - complete [shostak](0.01 s)
tr_rew5_TCC1..........................proved - complete [shostak](0.00 s)
tr_rew5...............................proved - complete [shostak](0.01 s)
tr_rew6...............................proved - complete [shostak](0.00 s)
tr_rew7...............................proved - complete [shostak](0.00 s)
tr_rew8_TCC1..........................proved - complete [shostak](0.01 s)
tr_rew8...............................proved - complete [shostak](0.00 s)
tr_rew9...............................proved - complete [shostak](0.03 s)
tr_rew10..............................proved - complete [shostak](0.04 s)
tr_rew11..............................proved - complete [shostak](0.00 s)
tr_rew12..............................proved - complete [shostak](0.00 s)
tr_rew13_TCC1.........................proved - complete [shostak](0.00 s)
tr_rew13..............................proved - complete [shostak](0.01 s)
tr_rew14..............................proved - complete [shostak](0.00 s)
tr_rew15..............................proved - complete [shostak](0.01 s)
tr_rew16..............................proved - complete [shostak](0.01 s)
tr_rew17..............................proved - complete [shostak](0.00 s)
tr_rew20_TCC1.........................proved - complete [shostak](0.02 s)
tr_rew20..............................proved - complete [shostak](0.01 s)
tr_rew22..............................proved - complete [shostak](0.01 s)
tr_rew23..............................proved - complete [shostak](0.00 s)
tr_rew24_TCC1.........................proved - complete [shostak](0.01 s)
tr_rew24..............................proved - complete [shostak](0.00 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (0.19 s)
Proof summary for theory atan_values
atan0.................................proved - complete [shostak](0.10 s)
atan1.................................proved - complete [shostak](0.09 s)
atan_1sqrt3...........................proved - complete [shostak](0.09 s)
atan_sqrt3............................proved - complete [shostak](0.08 s)
atan_m1sqrt3..........................proved - complete [shostak](0.08 s)
atan_msqrt3...........................proved - complete [shostak](0.05 s)
atan_gt_0.............................proved - complete [shostak](0.08 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.58 s)
Proof summary for theory atan2_props
atan2_is_0............................proved - complete [shostak](0.18 s)
atan2_is_pi2..........................proved - complete [shostak](0.15 s)
atan2_is_pi...........................proved - complete [shostak](0.15 s)
atan2_is_3pi2.........................proved - complete [shostak](0.14 s)
atan2_quad1...........................proved - complete [shostak](0.18 s)
atan2_quad2...........................proved - complete [shostak](0.22 s)
atan2_quad3...........................proved - complete [shostak](0.20 s)
atan2_quad4...........................proved - complete [shostak](0.19 s)
atan2_0x..............................proved - complete [shostak](0.06 s)
atan2_x0_TCC1.........................proved - complete [shostak](0.00 s)
atan2_x0..............................proved - complete [shostak](0.01 s)
atan2_11..............................proved - complete [shostak](0.12 s)
atan2_m11.............................proved - complete [shostak](0.21 s)
atan2_1m1.............................proved - complete [shostak](0.20 s)
atan2_m1m1............................proved - complete [shostak](0.17 s)
atan2_1sqrt3..........................proved - complete [shostak](0.08 s)
atan2_sqrt3_TCC1......................proved - complete [shostak](0.01 s)
atan2_sqrt3...........................proved - complete [shostak](0.06 s)
atan2_m1sqrt3.........................proved - complete [shostak](0.11 s)
atan2_sqrt3m1_TCC1....................proved - complete [shostak](0.01 s)
atan2_sqrt3m1.........................proved - complete [shostak](0.12 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (2.59 s)
Proof summary for theory jatan2
jatan2_TCC1...........................proved - complete [shostak](0.02 s)
jatan2_TCC2...........................proved - complete [shostak](0.01 s)
t1....................................proved - complete [shostak](0.01 s)
t2....................................proved - complete [shostak](0.07 s)
t3....................................proved - complete [shostak](0.01 s)
t4....................................proved - complete [shostak](0.08 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.20 s)
Proof summary for theory to2pi
to2pi_TCC1............................proved - complete [shostak](0.31 s)
to2pi_id..............................proved - complete [shostak](0.15 s)
to2pi_period..........................proved - complete [shostak](0.18 s)
sin_id_to2pi..........................proved - complete [shostak](0.13 s)
cos_id_to2pi..........................proved - complete [shostak](0.13 s)
to2pi_to2pi...........................proved - complete [shostak](0.15 s)
to2pi_to2pi_sub.......................proved - complete [shostak](0.14 s)
to2pi_neg.............................proved - complete [shostak](0.16 s)
to2pi_equal...........................proved - complete [shostak](0.21 s)
to2pi_to2pi_add.......................proved - complete [shostak](0.14 s)
to2pi_closed_diff.....................proved - complete [shostak](0.07 s)
to2pi_eq..............................proved - complete [shostak](0.09 s)
to2pi_sep.............................proved - complete [shostak](0.26 s)
sin_gt_to2pi..........................proved - complete [shostak](0.22 s)
sin_lt_to2pi..........................proved - complete [shostak](0.23 s)
sin_ge_to2pi..........................proved - complete [shostak](0.11 s)
cos_pos_to2pi.........................proved - complete [shostak](0.18 s)
cos_nneg_to2pi........................proved - complete [shostak](0.16 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (3.06 s)
Proof summary for theory deriv_sincos
deriv_domain..........................proved - complete [shostak](0.00 s)
sin_continuous........................proved - complete [shostak](0.23 s)
cos_continuous........................proved - complete [shostak](0.23 s)
sin_derivable_TCC1....................proved - complete [shostak](0.00 s)
sin_derivable_TCC2....................proved - complete [shostak](0.01 s)
sin_derivable.........................proved - complete [shostak](0.19 s)
cos_derivable.........................proved - complete [shostak](0.20 s)
deriv_sin_TCC1........................proved - complete [shostak](0.01 s)
deriv_sin.............................proved - complete [shostak](0.53 s)
deriv_cos_TCC1........................proved - complete [shostak](0.01 s)
deriv_cos.............................proved - complete [shostak](0.52 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.94 s)
Proof summary for theory integral_sincos
IMP_deriv_sincos_TCC1.................proved - complete [shostak](0.00 s)
IMP_deriv_sincos_TCC2.................proved - complete [shostak](0.00 s)
sin_Integrable........................proved - complete [shostak](0.05 s)
cos_Integrable........................proved - complete [shostak](0.05 s)
Integral_sin_TCC1.....................proved - complete [shostak](0.01 s)
Integral_sin..........................proved - complete [shostak](0.15 s)
Integral_cos_TCC1.....................proved - complete [shostak](0.01 s)
Integral_cos..........................proved - complete [shostak](0.16 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.43 s)
Proof summary for theory integral_indef_sincos
derivable_sin_lin_TCC1................proved - complete [shostak](0.01 s)
derivable_sin_lin_TCC2................proved - complete [shostak](0.01 s)
derivable_sin_lin.....................proved - complete [shostak](0.17 s)
derivable_cos_lin.....................proved - complete [shostak](0.18 s)
deriv_sin_lin_TCC1....................proved - complete [shostak](0.13 s)
deriv_sin_lin.........................proved - complete [shostak](0.45 s)
deriv_cos_lin_TCC1....................proved - complete [shostak](0.13 s)
deriv_cos_lin.........................proved - complete [shostak](0.45 s)
cos_lin_integrable_TCC1...............proved - complete [shostak](0.01 s)
cos_lin_integrable....................proved - complete [shostak](0.16 s)
sin_lin_integrable....................proved - complete [shostak](0.18 s)
integral_sin_TCC1.....................proved - complete [shostak](0.05 s)
integral_sin_TCC2.....................proved - complete [shostak](0.01 s)
integral_sin_TCC3.....................proved - complete [shostak](0.00 s)
integral_sin..........................proved - complete [shostak](0.26 s)
integral_cos_TCC1.....................proved - complete [shostak](0.04 s)
integral_cos..........................proved - complete [shostak](0.18 s)
Integral_sin_TCC1.....................proved - complete [shostak](0.10 s)
Integral_sin..........................proved - complete [shostak](0.38 s)
Integral_cos_TCC1.....................proved - complete [shostak](0.11 s)
Integral_cos..........................proved - complete [shostak](0.34 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (3.37 s)
Grand Totals: 677 proofs, 677 attempted, 677 succeeded (116.33 s)
[ Verzeichnis aufwärts0.241unsichere Verbindung
]
|
|
|
|
|
|
