| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: seq_pigeon.pvs Sprache: PVS
|
Untersuchungsergebnis.summary Download desMT940 {MT940[489] Hlasm[1457] Haskell[1799]}zum Wurzelverzeichnis wechseln *** *** top (18:55:23 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 complex_types real_complex..........................proved - complete [shostak](0.07 s) i_not_real............................proved - complete [shostak](0.08 s) unique_characterization...............proved - complete [shostak](0.35 s) real_is_complex.......................proved - complete [shostak](0.01 s) Re_TCC1...............................proved - complete [shostak](0.10 s) Im_TCC1...............................proved - complete [shostak](0.12 s) Re_def................................proved - complete [shostak](0.13 s) Im_def................................proved - complete [shostak](0.11 s) closed_plus...........................proved - complete [shostak](0.33 s) closed_neg............................proved - complete [shostak](0.25 s) closed_minus..........................proved - complete [shostak](0.03 s) closed_times..........................proved - complete [shostak](0.61 s) closed_divides........................proved - complete [shostak](0.81 s) complex_plus_complex_is_complex.......proved - complete [shostak](0.00 s) complex_minus_complex_is_complex......proved - complete [shostak](0.01 s) complex_times_complex_is_complex......proved - complete [shostak](0.01 s) complex_div_nzcomplex_is_complex......proved - complete [shostak](0.01 s) minus_complex_is_complex..............proved - complete [shostak](0.02 s) nzcomplex_times_nzcomplex_is_nzcomplex...proved - complete [shostak](0.06 s) nzcomplex_div_nzcomplex_is_nzcomplex...proved - complete [shostak](0.06 s) minus_nzcomplex_is_nzcomplex..........proved - complete [shostak](0.05 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (3.20 s) Proof summary for theory number_fields_bis number_fields_left_identity_add.......proved - complete [shostak](0.00 s) number_fields_right_identity_add......proved - complete [shostak](0.01 s) number_fields_left_identity_mult......proved - complete [shostak](0.00 s) number_fields_right_identity_mult.....proved - complete [shostak](0.01 s) number_fields_negate_is_left_inverse...proved - complete [shostak](0.01 s) number_fields_negate_is_right_inverse...proved - complete [shostak](0.00 s) both_sides_plus1......................proved - complete [shostak](0.01 s) both_sides_plus2......................proved - complete [shostak](0.00 s) both_sides_minus1.....................proved - complete [shostak](0.00 s) both_sides_minus2.....................proved - complete [shostak](0.26 s) number_fields_negate_negate...........proved - complete [shostak](0.02 s) zero_times1...........................proved - complete [shostak](0.10 s) zero_times2...........................proved - complete [shostak](0.02 s) nznum_times_nznum_is_nznum............proved - complete [shostak](0.17 s) minus_nznum_is_nznum..................proved - complete [shostak](0.03 s) zero_times3...........................proved - complete [shostak](0.04 s) neg_times_neg.........................proved - complete [shostak](0.31 s) zero_is_neg_zero......................proved - complete [shostak](0.01 s) both_sides_times1.....................proved - complete [shostak](0.43 s) both_sides_times2.....................proved - complete [shostak](0.04 s) inv_ne_0..............................proved - complete [shostak](0.02 s) nznum_div_nznum_is_nznum..............proved - complete [shostak](0.06 s) both_sides_div1.......................proved - complete [shostak](0.03 s) both_sides_div2.......................proved - complete [shostak](0.11 s) times_plus............................proved - complete [shostak](0.51 s) times_div1............................proved - complete [shostak](0.05 s) times_div2............................proved - complete [shostak](0.09 s) div_eq_zero...........................proved - complete [shostak](0.04 s) div_simp..............................proved - complete [shostak](0.04 s) div_cancel1...........................proved - complete [shostak](0.06 s) div_cancel2...........................proved - complete [shostak](0.06 s) div_cancel3...........................proved - complete [shostak](0.07 s) div_cancel4...........................proved - complete [shostak](0.05 s) cross_mult............................proved - complete [shostak](0.07 s) div_times.............................proved - complete [shostak](0.22 s) add_div...............................proved - complete [shostak](0.17 s) minus_div1............................proved - complete [shostak](0.39 s) minus_div2............................proved - complete [shostak](0.18 s) div_distributes.......................proved - complete [shostak](0.12 s) div_distributes_minus.................proved - complete [shostak](0.02 s) div_div1..............................proved - complete [shostak](0.06 s) div_div2..............................proved - complete [shostak](0.10 s) idem_add_is_zero......................proved - complete [shostak](0.07 s) nonzero_times1........................proved - complete [shostak](0.03 s) nonzero_times2........................proved - complete [shostak](0.04 s) nonzero_times3........................proved - complete [shostak](0.04 s) idem_mult.............................proved - complete [shostak](0.17 s) number_fields_negative_times..........proved - complete [shostak](0.14 s) number_fields_times_negative..........proved - complete [shostak](0.09 s) number_fields_neg1_times..............proved - complete [shostak](0.04 s) Theory totals: 50 formulas, 50 attempted, 50 succeeded (4.60 s) Proof summary for theory polar argrng_TCC1...........................proved - complete [shostak](0.06 s) abs_TCC1..............................proved - complete [shostak](0.34 s) abs_def...............................proved - complete [shostak](0.26 s) abs_real_rew..........................proved - complete [shostak](0.09 s) abs_imag_rew..........................proved - complete [shostak](0.14 s) abs_nzcomplex.........................proved - complete [shostak](0.12 s) abs_nz_iff_nz.........................proved - complete [shostak](0.08 s) abs_is_0..............................proved - complete [shostak](0.17 s) abs_neg...............................proved - complete [shostak](0.04 s) abs_mult..............................proved - complete [shostak](0.25 s) abs_inv_TCC1..........................proved - complete [shostak](0.01 s) abs_inv...............................proved - complete [shostak](0.14 s) abs_div...............................proved - complete [shostak](0.10 s) abs_triangle..........................proved - complete [shostak](4.52 s) abs_triangle_minus....................proved - complete [shostak](0.05 s) abs_abs...............................proved - complete [shostak](0.86 s) abs_i.................................proved - complete [shostak](0.17 s) arg_TCC1..............................proved - complete [shostak](0.05 s) arg_TCC2..............................proved - complete [shostak](0.21 s) arg_TCC3..............................proved - complete [shostak](0.06 s) arg_TCC4..............................proved - complete [shostak](0.17 s) arg_is_0_nz...........................proved - complete [shostak](0.16 s) arg_is_0..............................proved - complete [shostak](0.12 s) arg_is_pi2............................proved - complete [shostak](0.16 s) arg_is_pi.............................proved - complete [shostak](0.16 s) arg_is_mpi2...........................proved - complete [shostak](0.22 s) arg_lt_0..............................proved - complete [shostak](0.23 s) arg_p_lt_pi...........................proved - complete [shostak](0.21 s) arg_gt_0..............................proved - complete [shostak](0.09 s) arg_div_abs...........................proved - complete [shostak](0.51 s) Re_cos_abs1...........................proved - complete [shostak](0.18 s) Im_sin_abs1...........................proved - complete [shostak](1.16 s) arg_nnreal............................proved - complete [shostak](0.11 s) arg_nreal.............................proved - complete [shostak](0.11 s) arg_i.................................proved - complete [shostak](0.09 s) arg_neg...............................proved - complete [shostak](0.45 s) arg_mult..............................proved - complete [shostak](1.52 s) arg_inv...............................proved - complete [shostak](0.27 s) arg_div...............................proved - complete [shostak](0.35 s) arg_from_polar........................proved - complete [shostak](1.96 s) idempotent_rectangular................proved - complete [shostak](0.04 s) idempotent_polar......................proved - complete [shostak](1.93 s) Theory totals: 42 formulas, 42 attempted, 42 succeeded (17.87 s) Proof summary for theory arithmetic complex_is_Re_Im......................proved - complete [shostak](0.10 s) complex_is_0_Re_Im....................proved - complete [shostak](0.11 s) complex_is_ne_0_Re_Im.................proved - complete [shostak](0.06 s) complex_diff_eq_0.....................proved - complete [shostak](0.05 s) sq_abs_def............................proved - complete [shostak](0.17 s) conjugate_nz..........................proved - complete [shostak](0.15 s) sq_abs_realpred.......................proved - complete [shostak](0.16 s) nz_sq_abs_pos_TCC1....................proved - complete [shostak](0.03 s) nz_sq_abs_pos.........................proved - complete [shostak](0.65 s) sq_abs_nonneg_TCC1....................proved - complete [shostak](0.02 s) sq_abs_nonneg.........................proved - complete [shostak](0.03 s) Re_real...............................proved - complete [shostak](0.07 s) Im_real...............................proved - complete [shostak](0.05 s) Re_imag...............................proved - complete [shostak](0.08 s) Im_imag...............................proved - complete [shostak](0.06 s) Re_neg................................proved - complete [shostak](0.19 s) Im_neg................................proved - complete [shostak](0.19 s) Re_plus...............................proved - complete [shostak](0.29 s) Im_plus...............................proved - complete [shostak](0.33 s) Re_minus..............................proved - complete [shostak](0.12 s) Im_minus..............................proved - complete [shostak](0.13 s) Re_times..............................proved - complete [shostak](0.31 s) Im_times..............................proved - complete [shostak](0.36 s) Re_div_TCC1...........................proved - complete [shostak](0.03 s) Re_div................................proved - complete [shostak](1.29 s) Im_div................................proved - complete [shostak](0.71 s) plus_conjugate........................proved - complete [shostak](0.05 s) minus_conjugate.......................proved - complete [shostak](0.08 s) conjugate_plus........................proved - complete [shostak](0.13 s) conjugate_neg.........................proved - complete [shostak](0.34 s) conjugate_minus.......................proved - complete [shostak](0.03 s) conjugate_times.......................proved - complete [shostak](0.26 s) conjugate_inv_TCC1....................proved - complete [shostak](0.01 s) conjugate_inv.........................proved - complete [shostak](0.54 s) conjugate_div.........................proved - complete [shostak](0.04 s) Theory totals: 35 formulas, 35 attempted, 35 succeeded (7.18 s) Proof summary for theory number_fields_sq sq_nz_pos.............................proved - complete [shostak](0.03 s) sq_rew................................proved - complete [shostak](0.01 s) sq_neg................................proved - complete [shostak](0.00 s) sq_times..............................proved - complete [shostak](0.03 s) sq_plus...............................proved - complete [shostak](0.08 s) sq_minus..............................proved - complete [shostak](0.09 s) sq_neg_minus..........................proved - complete [shostak](0.05 s) sq_0..................................proved - complete [shostak](0.00 s) sq_1..................................proved - complete [shostak](0.00 s) sq_eq_0...............................proved - complete [shostak](0.03 s) sq_div................................proved - complete [shostak](0.03 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.34 s) Proof summary for theory exp exp_TCC1..............................proved - complete [shostak](0.19 s) exp_real..............................proved - complete [shostak](0.19 s) exp_imag..............................proved - complete [shostak](0.21 s) abs_exp_imag..........................proved - complete [shostak](1.13 s) arg_exp_real..........................proved - complete [shostak](0.06 s) arg_exp_imag..........................proved - complete [shostak](0.51 s) exp_0.................................proved - complete [shostak](0.18 s) exp_1.................................proved - complete [shostak](0.19 s) exp_i_pi..............................proved - complete [shostak](0.14 s) exp_plus..............................proved - complete [shostak](0.59 s) exp_negate............................proved - complete [shostak](0.71 s) exp_minus.............................proved - complete [shostak](0.11 s) exp_periodicity.......................proved - complete [shostak](0.45 s) abs_exp...............................proved - complete [shostak](0.39 s) ln_TCC1...............................proved - complete [shostak](0.01 s) ln_1..................................proved - complete [shostak](0.16 s) ln_e..................................proved - complete [shostak](0.21 s) ln_exp................................proved - complete [shostak](0.69 s) exp_ln................................proved - complete [shostak](0.15 s) ln_mult...............................proved - complete [shostak](0.39 s) ln_inv................................proved - complete [shostak](0.63 s) ln_div................................proved - complete [shostak](0.51 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (7.77 s) Proof summary for theory trig_aux sin_cos_eq_0..........................proved - complete [shostak](0.05 s) eq_iff_periodic.......................proved - complete [shostak](0.28 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.34 s) Proof summary for theory complex_sqrt sqrt_TCC1.............................proved - complete [shostak](0.04 s) sqrt_nz_is_nz.........................proved - complete [shostak](0.25 s) sqrt_nnz..............................proved - complete [shostak](0.24 s) sqrt_npz_TCC1.........................proved - complete [shostak](0.01 s) sqrt_npz..............................proved - complete [shostak](0.59 s) sqrt_0................................proved - complete [shostak](0.05 s) sqrt_1................................proved - complete [shostak](0.17 s) sqrt_neg1.............................proved - complete [shostak](0.05 s) sqrt_eq_0.............................proved - complete [shostak](0.01 s) sqrt_sq_TCC1..........................proved - complete [shostak](0.03 s) sqrt_sq...............................proved - complete [shostak](0.37 s) sq_sqrt...............................proved - complete [shostak](3.05 s) sqrt_times............................proved - complete [shostak](2.27 s) sqrt_neg..............................proved - complete [shostak](0.30 s) sqrt_inv..............................proved - complete [shostak](0.96 s) sqrt_div..............................proved - complete [shostak](0.48 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (8.87 s) Proof summary for theory complex_field fullset_is_field......................proved - complete [shostak](0.58 s) IMP_field_TCC1........................proved - complete [shostak](0.60 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.18 s) Proof summary for theory complex_sets difference_TCC1.......................proved - complete [shostak](0.02 s) plus_TCC1.............................proved - complete [shostak](0.03 s) difference_TCC2.......................proved - complete [shostak](0.02 s) Arg_TCC1..............................proved - complete [shostak](0.09 s) Arg_def...............................proved - complete [shostak](0.46 s) Arg_mult..............................proved - complete [shostak](0.58 s) Arg_inv...............................proved - complete [shostak](0.31 s) Arg_div...............................proved - complete [shostak](0.14 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.66 s) Grand Totals: 209 proofs, 209 attempted, 209 succeeded (53.00 s) [ zur Elbe Produktseite wechseln0.129Quellennavigators ] |