products/sources/formale Sprachen/PVS/summaries/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: prelude_sets_aux.prf   Sprache: Unknown

Spracherkennung für: .summary vermutete Sprache: Hlasm {Hlasm[446] Haskell[893] BAT[927]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]

*** 
*** 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)

[ Dauer der Verarbeitung: 0.108 Sekunden  ]