| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: inverse_fun_ms_continuous.prf Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: Hlasm {Hlasm[429] Haskell[851] BAT[873]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (16:16:17 2/25/2014) *** Generated by proveit - ProofLite-6.0.7 (2/28/14) *** Trusted Oracles *** MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit *** Proof summary for theory top Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory relation_extension rel_extension_is_equivalence..........proved - complete [shostak](0.08 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s) Proof summary for theory relation_extension_props extended_equiv_class_non_empty........proved - complete [shostak](0.03 s) nonempty_equivClass_impl_extended_equiv_class_non_empty...proved - complete [shosta nonempty_equivClass_iff_extended_equiv_classT_non_empty...proved - complete [shosta nonempty_equivClass_iff_extended_equiv_classU_non_empty...proved - complete [shosta proj_tuple_1_equiv_class_representative...proved - complete [shostak](0.01 s) proj_tuple_2_equiv_class_representative...proved - complete [shostak](0.02 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.45 s) Proof summary for theory relation_inverse_image equivClass_is_nonempty................proved - complete [shostak](0.02 s) equivClass_equal_is_nonempty..........proved - complete [shostak](0.01 s) inverse_image_of_equivalence..........proved - complete [shostak](0.02 s) preserves_eqv_of_inv_image............proved - complete [shostak](0.03 s) inverse_image_of_equality.............proved - complete [shostak](0.02 s) image_inverse_eq_is_eq_kernel.........proved - complete [shostak](0.03 s) inv_img_surj_impl_codom_eq............proved - complete [shostak](0.05 s) right_inv_inv_finv_image_impl_codom_eq...proved - complete [shostak](0.06 s) surjective_eqv_image_inv_rel_codomain...proved - complete [shostak](0.03 s) right_inv_inv_finv_image_eq_codom_eq...proved - complete [shostak](0.05 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.32 s) Proof summary for theory relation_inverse_extension le_U_induces_equivalence..............proved - complete [shostak](0.04 s) le_T_induces_equivalence..............proved - complete [shostak](0.03 s) rel_inv_extension_is_equivalence......proved - complete [shostak](0.07 s) rel_extension_IFF_rel_ext.............proved - complete [shostak](0.06 s) rel_inv_extension2_is_equivalence.....proved - complete [shostak](0.07 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.26 s) Proof summary for theory rr_rel g_conistent_with_RR...................proved - complete [shostak](0.04 s) f_conistent_with_RR...................proved - complete [shostak](0.05 s) RR_functional_conditional_equal_RR2...proved - complete [shostak](0.13 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.21 s) Proof summary for theory simplest_examples Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory singleton_example relations_equality_TCC1...............proved - complete [shostak](0.03 s) relations_equality_TCC2...............proved - complete [shostak](0.02 s) relations_equality....................proved - complete [shostak](0.06 s) relations_equality2...................proved - complete [shostak](0.09 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.20 s) Proof summary for theory finite_nats_trivial T1_TCC1...............................proved - complete [shostak](0.01 s) U1_TCC1...............................proved - complete [shostak](0.02 s) g1_TCC1...............................proved - complete [shostak](0.01 s) e1_TCC1...............................proved - complete [shostak](0.06 s) relations_equality_TCC1...............proved - complete [shostak](0.05 s) relations_equality_TCC2...............proved - complete [shostak](0.13 s) relations_equality....................proved - complete [shostak](0.20 s) relations_equality2...................proved - complete [shostak](0.27 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.75 s) Proof summary for theory infinite_to_infinite_trivial relations_equality_TCC1...............proved - complete [shostak](0.12 s) relations_equality_TCC2...............proved - complete [shostak](0.03 s) relations_equality....................proved - complete [shostak](0.14 s) relations_equality2...................proved - complete [shostak](0.19 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.48 s) Proof summary for theory finite_to_infinite relations_equality_TCC1...............proved - complete [shostak](0.03 s) relations_equality_TCC2...............proved - complete [shostak](0.05 s) relations_equality....................proved - complete [shostak](0.08 s) relations_equality2...................proved - complete [shostak](0.15 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.31 s) Proof summary for theory infinite_to_finite_finite_equival_finite_equival_classes relations_equality_TCC1...............proved - complete [shostak](0.05 s) relations_equality_TCC2...............proved - complete [shostak](0.04 s) relations_equality....................proved - complete [shostak](0.15 s) relations_equality2...................proved - complete [shostak](0.25 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.50 s) Proof summary for theory infinite_to_finite_infinite_equival_finite_equival_classes U8_TCC1...............................proved - complete [shostak](0.01 s) relations_equality_TCC1...............proved - complete [shostak](0.11 s) relations_equality_TCC2...............proved - complete [shostak](0.11 s) relations_equality....................proved - complete [shostak](0.62 s) relations_equality2...................proved - complete [shostak](0.54 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.39 s) Proof summary for theory infinite_to_infinite_infinite_equival_infinite_equival_clas e9_TCC1...............................proved - complete [shostak](0.01 s) relations_equality_TCC1...............proved - complete [shostak](0.04 s) relations_equality_TCC2...............proved - complete [shostak](0.04 s) relations_equality....................proved - complete [shostak](0.06 s) relations_equality2...................proved - complete [shostak](0.13 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.29 s) Proof summary for theory infinite_to_infinite_infinite_equival_finite_equival_classe relations_equality_TCC1...............proved - complete [shostak](0.03 s) relations_equality_TCC2...............proved - complete [shostak](0.12 s) relations_equality....................proved - complete [shostak](0.28 s) relations_equality2...................proved - complete [shostak](0.41 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.85 s) Proof summary for theory finite_to_infinite_finite_equival_infinite_equival_classes T11_TCC1..............................proved - complete [shostak](0.01 s) relations_equality_TCC1...............proved - complete [shostak](0.10 s) relations_equality_TCC2...............proved - complete [shostak](0.11 s) relations_equality....................proved - complete [shostak](0.55 s) relations_equality2...................proved - complete [shostak](0.79 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.56 s) Grand Totals: 68 proofs, 68 attempted, 68 succeeded (7.64 s) [ Dauer der Verarbeitung: 0.173 Sekunden ] |