| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: seq_extras.pvs Sprache: PVS
|
Untersuchungsergebnis.summary Download desMT940 {MT940[291] Hlasm[1509] Haskell[1909]}zum Wurzelverzeichnis wechseln *** *** top (17:32:10 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 prime_factorization prime_factorization...................proved - complete [shostak](0.41 s) prime_factors.........................proved - incomplete [shostak](-.51 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (-0.09 s) Proof summary for theory product_perm_lems swap_TCC1.............................proved - complete [shostak](0.01 s) swap_len..............................proved - complete [shostak](0.02 s) swap_eq_arg...........................proved - complete [shostak](0.09 s) swap_symm.............................proved - complete [shostak](0.08 s) prod_swap_prep_TCC1...................proved - complete [shostak](0.02 s) prod_swap_prep........................proved - complete [shostak](0.17 s) prod_swap_prep2_TCC1..................proved - complete [shostak](0.02 s) prod_swap_prep2.......................proved - complete [shostak](0.09 s) product_swap..........................proved - complete [shostak](1.58 s) swap_is_permutation...................proved - complete [shostak](0.25 s) product_permutation...................proved - incomplete [shostak](2.48 s) length_sort...........................proved - incomplete [shostak](0.17 s) product_sort..........................proved - incomplete [shostak](0.18 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (5.14 s) Proof summary for theory unique_factorization FTL_sym_TCC1..........................proved - complete [shostak](0.17 s) FTL_sym_TCC2..........................proved - complete [shostak](0.16 s) FTL_sym...............................proved - incomplete [shostak](1.32 s) FTL_prep..............................proved - incomplete [shostak](0.75 s) Fundamental_Theorem_Arithmetic........proved - incomplete [shostak](0.10 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.50 s) Proof summary for theory unique_scaf gcd_primes_TCC1.......................proved - complete [shostak](0.04 s) gcd_primes............................proved - complete [shostak](0.30 s) len1..................................proved - complete [shostak](0.14 s) len3..................................proved - complete [shostak](0.02 s) ordered_list_of_primes_caret..........proved - complete [shostak](0.16 s) olop..................................proved - incomplete [shostak](0.64 s) product_len_eq........................proved - complete [shostak](0.24 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.53 s) Proof summary for theory infinite_primes prime_divides.........................proved - incomplete [shostak](0.11 s) divides_product.......................proved - complete [shostak](0.17 s) primes_infinite.......................proved - incomplete [shostak](0.46 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.74 s) Proof summary for theory sqrt_two even_or_odd...........................proved - complete [shostak](0.05 s) two_divides_sq_TCC1...................proved - complete [shostak](0.03 s) two_divides_sq........................proved - complete [shostak](0.34 s) sqrt2_is_irrational...................proved - complete [shostak](0.29 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.70 s) Proof summary for theory eq_mod eq_mod_equiv..........................proved - complete [shostak](0.16 s) eq_mod_mult...........................proved - complete [shostak](0.19 s) eq_mod_rem............................proved - complete [shostak](0.11 s) gcd_is_1_TCC1.........................proved - complete [shostak](0.03 s) gcd_is_1..............................proved - complete [shostak](0.11 s) Euclids_30............................proved - complete [shostak](0.32 s) eq_mod_cancel.........................proved - complete [shostak](0.16 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.07 s) Proof summary for theory primes_sum_squares sum_of_two_squares?_TCC1..............proved - complete [shostak](0.01 s) sots_int?_TCC1........................proved - complete [shostak](0.01 s) sots_int_def..........................proved - complete [shostak](0.24 s) Brahmagupta_Fibonacci.................proved - complete [shostak](0.61 s) prime_divides.........................proved - complete [shostak](0.65 s) sots_div_prime_closed_TCC1............proved - complete [shostak](0.06 s) sots_div_prime_closed_TCC2............proved - complete [shostak](0.12 s) sots_div_prime_closed.................proved - complete [shostak](9.41 s) sots_div_quot_factor_TCC1.............proved - complete [shostak](0.06 s) sots_div_quot_factor_TCC2.............proved - complete [shostak](0.08 s) sots_div_quot_factor..................proved - incomplete [shostak](0.92 s) rel_prime_sos_factor_TCC1.............proved - complete [shostak](0.01 s) rel_prime_sos_factor_TCC2.............proved - complete [shostak](0.01 s) rel_prime_sos_factor_TCC3.............proved - complete [shostak](0.02 s) rel_prime_sos_factor..................proved - incomplete [shostak](7.21 s) fermat_prime_sos_finite_set...........proved - incomplete [shostak](1.91 s) involution_odd_has_fixedpoint.........proved - complete [shostak](0.63 s) involution_one_fixedpoint_odd.........proved - complete [shostak](1.60 s) involution_fermat_set_one_fp_invol_TCC1...proved - complete [shostak](0.07 s) involution_fermat_set_one_fp_invol_TCC2...proved - complete [shostak](0.08 s) involution_fermat_set_one_fp_invol_TCC3...proved - complete [shostak](0.09 s) involution_fermat_set_one_fp_invol_TCC4...proved - complete [shostak](0.08 s) involution_fermat_set_one_fp_invol_TCC5...proved - complete [shostak](0.07 s) involution_fermat_set_one_fp_invol....proved - complete [shostak](2.41 s) invol_fermat_TCC1.....................proved - complete [shostak](0.33 s) invol_fermat_TCC2.....................proved - complete [shostak](0.33 s) invol_fermat_TCC3.....................proved - complete [shostak](0.34 s) invol_fermat_one_fp...................proved - complete [shostak](0.64 s) fermat_prime_mod_4_TCC1...............proved - complete [shostak](0.10 s) fermat_prime_mod_4....................proved - incomplete [shostak](1.20 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (29.28 s) Proof summary for theory chinese_remainder chinese_remainder_base_TCC1...........proved - complete [shostak](0.00 s) chinese_remainder_base................proved - complete [shostak](0.88 s) chinese_remainder_TCC1................proved - complete [shostak](0.03 s) chinese_remainder.....................proved - complete [shostak](1.39 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (2.30 s) Proof summary for theory fermats_little_theorem prime_divides_choose_TCC1.............proved - complete [shostak](0.03 s) prime_divides_choose..................proved - complete [shostak](0.20 s) Fermats_Little_TCC1...................proved - complete [shostak](0.01 s) Fermats_Little........................proved - complete [shostak](2.44 s) fermats_little_theorem_TCC1...........proved - complete [shostak](0.01 s) fermats_little_theorem................proved - complete [shostak](2.25 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (4.94 s) Grand Totals: 81 proofs, 81 attempted, 81 succeeded (48.11 s) [ zur Elbe Produktseite wechseln0.121Quellennavigators ] |