Untersuchungsergebnis.summary Download desHlasm {Hlasm[446] Haskell[893] BAT[927]}zum Wurzelverzeichnis wechseln
***
*** top (16:16:14 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 relational_choice
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory relation_implication
rel_impl_extensionality...............proved - complete [shostak](0.03 s)
lemma_double_impl.....................proved - complete [shostak](0.01 s)
rel_impl_is_partial_order.............proved - complete [shostak](0.04 s)
double_impl_is_equivalence............proved - complete [shostak](0.03 s)
turnstile_TCC1........................proved - complete [shostak](0.09 s)
models_TCC1...........................proved - complete [shostak](0.11 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.31 s)
Proof summary for theory relational_choice_properties
fun_choice_impl_description...........proved - complete [shostak](0.06 s)
fun_choice_impl_rel_unique_choice.....proved - complete [shostak](0.04 s)
fun_choice_impl_rel_choice............proved - complete [shostak](0.04 s)
fun_choice_impl_rel_choice_impl_description_rel_choice...proved - complete [shostak](0.07 s)
fun_choice_impl_rel_choice_and_description_rel_choice...proved - complete [shostak](0.02 s)
fun_choice_impl_rel_unique_choice_impl_description_rel_choice...proved - complete [shostak](0.08 s)
fun_choice_impl_rel_unique_choice_and_description_rel_choice...proved - complete [shostak](0.02 s)
description_rel_unique_choice_imp_funct_choice...proved - complete [shostak](0.05 s)
description_rel_and_rel_unique_choice_imp_funct_choice...proved - complete [shostak](0.03 s)
rel_choice_and_proof_irrel_imp_guarded_rel_choice...proved - complete [shostak](0.04 s)
relx_choice_indep_of_premises_imp_guarded_rel_choice...proved - complete [shostak](0.06 s)
fun_choice_equiv_rel_unique_param_desc...proved - complete [shostak](0.02 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.51 s)
Grand Totals: 18 proofs, 18 attempted, 18 succeeded (0.82 s)
[ zur Elbe Produktseite wechseln0.105Quellennavigators
]
