| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: library.scala Sprache: Scala
|
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[311] Hlasm[1449] Haskell[1855]}zum Wurzelverzeichnis wechseln *** *** top (21:1:1 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 list_props_aux length_is_0...........................proved - complete [shostak](0.06 s) append_is_null........................proved - complete [shostak](0.05 s) append_eq1............................proved - complete [shostak](0.08 s) append_eq2............................proved - complete [shostak](-.82 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (-0.63 s) Proof summary for theory State Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory AExp A_TCC1................................proved - complete [shostak](0.05 s) A_TCC2................................proved - complete [shostak](0.04 s) A_TCC3................................proved - complete [shostak](0.05 s) A_TCC4................................proved - complete [shostak](0.05 s) A_TCC5................................proved - complete [shostak](0.04 s) A_TCC6................................proved - complete [shostak](0.04 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.27 s) Proof summary for theory BExp B_TCC1................................proved - complete [shostak](0.05 s) B_TCC2................................proved - complete [shostak](0.05 s) B_TCC3................................proved - complete [shostak](0.05 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.15 s) Proof summary for theory Stm Stm_measure_TCC1......................proved - complete [shostak](0.06 s) Stm_measure_TCC2......................proved - complete [shostak](0.04 s) Stm_measure_TCC3......................proved - complete [shostak](0.06 s) Stm_measure_TCC4......................proved - complete [shostak](0.06 s) Stm_measure_TCC5......................proved - complete [shostak](0.06 s) IMP_measure_induction_TCC1............proved - complete [shostak](0.04 s) structural_induction..................proved - complete [shostak](0.29 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.61 s) Proof summary for theory Cont sq_le_def.............................proved - complete [shostak](0.13 s) partial_order_sq_le...................proved - complete [shostak](0.08 s) lub_graph_TCC1........................proved - complete [shostak](0.04 s) lub_graph_TCC2........................proved - complete [shostak](0.14 s) lub_graph.............................proved - complete [shostak](0.48 s) sq_le_dcpo............................proved - complete [shostak](0.55 s) sq_le_pdcpo...........................proved - complete [shostak](0.05 s) sq_le_bottom..........................proved - complete [shostak](0.05 s) sq_le_least...........................proved - complete [shostak](0.06 s) sq_le_conditional.....................proved - complete [shostak](0.09 s) apply_continuous......................proved - complete [shostak](3.72 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (5.38 s) Proof summary for theory direct SS_TCC1...............................proved - complete [shostak](0.14 s) SS_TCC2...............................proved - complete [shostak](0.14 s) SS_TCC3...............................proved - complete [shostak](0.17 s) SS_TCC4...............................proved - complete [shostak](0.15 s) SS_TCC5...............................proved - complete [shostak](0.15 s) SS_TCC6...............................proved - complete [shostak](0.15 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.90 s) Proof summary for theory continuation IMP_fixpoints_TCC1....................proved - complete [shostak](3.81 s) identity_continuous...................proved - complete [shostak](4.75 s) composition_continuous................proved - complete [shostak](4.91 s) assign_continuous.....................proved - complete [shostak](4.75 s) conditional_continuous................proved - complete [shostak](5.81 s) composition_conditional...............proved - complete [shostak](4.75 s) SS_TCC1...............................proved - complete [shostak](3.82 s) SS_TCC2...............................proved - complete [shostak](4.83 s) SS_TCC3...............................proved - complete [shostak](4.88 s) SS_TCC4...............................proved - complete [shostak](4.80 s) SS_TCC5...............................proved - complete [shostak](4.81 s) SS_TCC6...............................proved - complete [shostak](4.82 s) SS_TCC7...............................proved - complete [shostak](4.89 s) SS_TCC8...............................proved - complete [shostak](4.84 s) SS_TCC9...............................proved - complete [shostak](4.87 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (71.36 s) Proof summary for theory congruence IMP_admissible_TCC1..................proved - complete [shostak](10.36 s) P_bottom_TCC1........................proved - complete [shostak]( 5.36 s) P_bottom.............................proved - complete [shostak]( 4.09 s) IMP_scott_continuity_TCC1............proved - complete [shostak]( 2.55 s) admissible_P.........................proved - complete [shostak](11.78 s) continuation_direct..................proved - complete [shostak]( 7.07 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (41.21 s) Proof summary for theory sos step_TCC1.............................proved - complete [shostak](4.11 s) tr_TCC1...............................proved - complete [shostak](4.08 s) tr_TCC2...............................proved - complete [shostak](4.04 s) tr_TCC3...............................proved - complete [shostak](4.01 s) tr_add................................proved - complete [shostak](4.22 s) tr_eq.................................proved - complete [shostak](4.04 s) tr_split..............................proved - complete [shostak](4.27 s) tr_partial............................proved - complete [shostak](4.10 s) tr_deterministic......................proved - complete [shostak](3.12 s) SS_TCC1...............................proved - complete [shostak](4.06 s) SS_deterministic......................proved - complete [shostak](4.09 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (44.14 s) Proof summary for theory direct_sos sos_le_direct........................proved - complete [shostak](19.98 s) direct_le_sos........................proved - complete [shostak](19.28 s) direct_eq_sos........................proved - complete [shostak](16.55 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (55.81 s) Proof summary for theory compiler CA_TCC1...............................proved - complete [shostak](0.07 s) CA_TCC2...............................proved - complete [shostak](0.07 s) CA_TCC3...............................proved - complete [shostak](0.07 s) CA_TCC4...............................proved - complete [shostak](0.07 s) CA_TCC5...............................proved - complete [shostak](0.08 s) CA_TCC6...............................proved - complete [shostak](0.07 s) CB_TCC1...............................proved - complete [shostak](0.06 s) CB_TCC2...............................proved - complete [shostak](0.07 s) CB_TCC3...............................proved - complete [shostak](0.07 s) CS_TCC1...............................proved - complete [shostak](0.08 s) CS_TCC2...............................proved - complete [shostak](0.07 s) CS_TCC3...............................proved - complete [shostak](0.09 s) CS_TCC4...............................proved - complete [shostak](0.08 s) CS_TCC5...............................proved - complete [shostak](0.08 s) nonnull_CA............................proved - complete [shostak](0.17 s) nonnull_CB............................proved - complete [shostak](0.21 s) nonnull_CS............................proved - complete [shostak](0.13 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (1.54 s) Proof summary for theory Instruction Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory am check2_TCC1...........................proved - complete [shostak](0.06 s) step_TCC1.............................proved - complete [shostak](0.05 s) step_TCC2.............................proved - complete [shostak](0.07 s) step_TCC3.............................proved - complete [shostak](0.05 s) step_TCC4.............................proved - complete [shostak](0.07 s) step_TCC5.............................proved - complete [shostak](0.06 s) step_TCC6.............................proved - complete [shostak](0.06 s) tr_TCC1...............................proved - complete [shostak](0.08 s) tr_TCC2...............................proved - complete [shostak](0.07 s) step_append...........................proved - complete [shostak](0.95 s) tr_add................................proved - complete [shostak](0.18 s) tr_eq.................................proved - complete [shostak](0.08 s) code_partial..........................proved - complete [shostak](2.12 s) code_split............................proved - complete [shostak](1.28 s) M_TCC1................................proved - complete [shostak](0.05 s) M_deterministic.......................proved - complete [shostak](0.27 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (5.51 s) Proof summary for theory bisimulation correct_AExp..........................proved - complete [shostak](0.97 s) correct_BExp..........................proved - complete [shostak](1.26 s) eq_AExp...............................proved - complete [shostak](0.18 s) AExp_steps............................proved - complete [shostak](-.54 s) AExp_e................................proved - complete [shostak](1.43 s) eq_BExp...............................proved - complete [shostak](0.20 s) BExp_steps............................proved - complete [shostak](0.09 s) BExp_e................................proved - complete [shostak](3.82 s) tilde_TCC1............................proved - complete [shostak](0.06 s) tilde_TCC2............................proved - complete [shostak](0.06 s) sos_step..............................proved - complete [shostak](1.51 s) sos_steps.............................proved - complete [shostak](0.28 s) am_step1..............................proved - complete [shostak](1.97 s) am_steps..............................proved - complete [shostak](0.66 s) bisimulation..........................proved - complete [shostak](0.47 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (12.43 s) Proof summary for theory axiomatic inference_tree?_TCC1..................proved - complete [shostak](0.05 s) inference_tree?_TCC2..................proved - complete [shostak](0.06 s) inference_tree?_TCC3..................proved - complete [shostak](0.08 s) inference_tree?_TCC4..................proved - complete [shostak](0.08 s) inference_tree?_TCC5..................proved - complete [shostak](0.05 s) inference_tree?_TCC6..................proved - complete [shostak](0.06 s) inference_tree?_TCC7..................proved - complete [shostak](0.08 s) inference_tree?_TCC8..................proved - complete [shostak](0.08 s) inference_tree?_TCC9..................proved - complete [shostak](0.06 s) inference_tree?_TCC10.................proved - complete [shostak](0.05 s) inference_tree?_TCC11.................proved - complete [shostak](0.06 s) inference_tree?_TCC12.................proved - complete [shostak](0.05 s) inference_tree_TCC1...................proved - complete [shostak](0.04 s) wlp_is_precondition...................proved - complete [shostak](5.22 s) wlp_is_weakest........................proved - complete [shostak](5.21 s) soundness.............................proved - complete [shostak](4.99 s) completeness..........................proved - complete [shostak](6.18 s) sound_and_complete....................proved - complete [shostak](5.21 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (27.61 s) Proof summary for theory natural depth_TCC1............................proved - complete [shostak](4.03 s) depth_TCC2............................proved - complete [shostak](4.02 s) depth_TCC3............................proved - complete [shostak](4.03 s) derivation_tree?_TCC1.................proved - complete [shostak](4.04 s) derivation_tree?_TCC2.................proved - complete [shostak](4.03 s) derivation_tree?_TCC3.................proved - complete [shostak](4.04 s) derivation_tree?_TCC4.................proved - complete [shostak](4.04 s) derivation_tree?_TCC5.................proved - complete [shostak](4.03 s) derivation_tree?_TCC6.................proved - complete [shostak](4.04 s) derivation_tree_TCC1..................proved - complete [shostak](3.98 s) dt_eq.................................proved - complete [shostak](6.65 s) SS_TCC1...............................proved - complete [shostak](4.00 s) SS_deterministic......................proved - complete [shostak](4.09 s) natural_le_sos........................proved - complete [shostak](1.34 s) sos_le_natural........................proved - complete [shostak](1.02 s) natural_eq_sos........................proved - complete [shostak](0.07 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (57.44 s) Grand Totals: 154 proofs, 154 attempted, 154 succeeded (323.72 s) [ Verzeichnis aufwärts1.419unsichere Verbindung ] |