|
***
*** 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 [shostak](0.04 s)
nonempty_equivClass_iff_extended_equiv_classT_non_empty...proved - complete [shostak](0.17 s)
nonempty_equivClass_iff_extended_equiv_classU_non_empty...proved - complete [shostak](0.16 s)
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_classes
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_classes
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.17 Sekunden
(vorverarbeitet)
]
|
