Untersuchungsergebnis.summary Download desMT940 {MT940[324] Hlasm[1568] Haskell[1928]}zum Wurzelverzeichnis wechseln
***
*** top (20:40:44 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 partial_function_props
member_dom............................proved - complete [shostak](0.19 s)
member_graph..........................proved - complete [shostak](0.18 s)
graph_eq..............................proved - complete [shostak](-.51 s)
graph_is_graph?.......................proved - complete [shostak](0.16 s)
graph_from_graph......................proved - complete [shostak](0.28 s)
from_graph_graph_TCC1.................proved - complete [shostak](0.13 s)
from_graph_graph......................proved - complete [shostak](0.22 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.64 s)
Proof summary for theory scott
down_is_closed........................proved - complete [shostak](0.18 s)
scott_empty...........................proved - complete [shostak](0.26 s)
scott_full............................proved - complete [shostak](0.23 s)
scott_union...........................proved - complete [shostak](0.20 s)
scott_Intersection....................proved - complete [shostak](0.22 s)
scott_topology........................proved - complete [shostak](0.29 s)
scott_open_sets_is_topology...........proved - complete [shostak](0.14 s)
closed_is_lower.......................proved - complete [shostak](0.16 s)
open_is_upper.........................proved - complete [shostak](0.22 s)
closure_is_down.......................proved - complete [shostak](0.32 s)
order_iff_closure.....................proved - complete [shostak](0.15 s)
order_iff_subset......................proved - complete [shostak](0.31 s)
scott_is_T0...........................proved - complete [shostak](0.22 s)
scott_hausdorff.......................proved - complete [shostak](0.45 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (3.36 s)
Proof summary for theory scott_continuity
lub_set_image.........................proved - complete [shostak](0.21 s)
directed_image_TCC1...................proved - complete [shostak](0.15 s)
directed_image........................proved - complete [shostak](0.19 s)
lub_image_TCC1........................proved - complete [shostak](0.14 s)
lub_image.............................proved - complete [shostak](0.20 s)
lub_image_increasing_TCC1.............proved - complete [shostak](0.14 s)
lub_image_increasing_TCC2.............proved - complete [shostak](0.16 s)
lub_image_increasing..................proved - complete [shostak](0.45 s)
scott_continuous_def..................proved - complete [shostak](0.75 s)
scott_continuous_is_continuous........proved - complete [shostak](0.14 s)
continuous_is_scott_continuous........proved - complete [shostak](0.14 s)
continuous_is_increasing..............proved - complete [shostak](0.14 s)
continuous_is_lub_preserving..........proved - complete [shostak](0.15 s)
pointwise_complete....................proved - complete [shostak](2.35 s)
scott_continuous_dcpo.................proved - complete [shostak](4.30 s)
IMP_scott_TCC1........................proved - complete [shostak](1.19 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (10.81 s)
Proof summary for theory fun_preds_partial
strict_increasing_is_increasing.......proved - complete [shostak](0.14 s)
strict_decreasing_is_decreasing.......proved - complete [shostak](0.15 s)
strict_monotonic_is_monotonic.........proved - complete [shostak](0.14 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.43 s)
Proof summary for theory pointwise_orders_aux
continuous_pointwise_preserves_directed_complete_partial_order...proved - complete [shostak](0.14 s)
continuous_pointwise_preserves_pointed_directed_complete_partial_order...proved - complete [shostak](0.78 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.92 s)
Proof summary for theory scott_identity_continuity
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory scott_composition_continuity
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory fixpoints
unique_bottom.........................proved - complete [shostak](0.16 s)
bottom_TCC1...........................proved - complete [shostak](0.14 s)
bottom_le.............................proved - complete [shostak](0.14 s)
le_bottom.............................proved - complete [shostak](0.16 s)
nonempty_T............................proved - complete [shostak](0.21 s)
IMP_monoid_TCC1.......................proved - complete [shostak](-.61 s)
lub_add_bottom_TCC1...................proved - complete [shostak](0.22 s)
lub_add_bottom........................proved - complete [shostak](0.24 s)
increasing_phi_n......................proved - complete [shostak](0.19 s)
increasing_power......................proved - complete [shostak](0.19 s)
fix_approx_nonempty...................proved - complete [shostak](0.50 s)
fix_approx_chain......................proved - complete [shostak](0.72 s)
ne_chain_is_directed..................proved - complete [shostak](0.67 s)
lub_emptyset_TCC1.....................proved - complete [shostak](0.16 s)
lub_emptyset..........................proved - complete [shostak](0.18 s)
fix_TCC1..............................proved - complete [shostak](0.16 s)
member_FIX............................proved - complete [shostak](0.14 s)
fix_is_least..........................proved - complete [shostak](0.23 s)
fix_le................................proved - complete [shostak](0.25 s)
fix_in_FIX............................proved - complete [shostak](3.31 s)
nonempty_FIX..........................proved - complete [shostak](2.72 s)
fix_prop..............................proved - complete [shostak](2.72 s)
fixpoint_contraction..................proved - complete [shostak](2.83 s)
Theory totals: 23 formulas, 23 attempted, 23 succeeded (15.63 s)
Proof summary for theory admissible
IMP_scott_TCC1........................proved - complete [shostak](2.41 s)
admissible_pred?_TCC1.................proved - complete [shostak](3.07 s)
admissible_pred?_TCC2.................proved - complete [shostak](3.09 s)
admissible_pred_TCC1..................proved - complete [shostak](3.05 s)
fixpoint_induction....................proved - complete [shostak](3.12 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (14.73 s)
Proof summary for theory dual_fixpoints
IMP_scott_continuity_TCC1.............proved - complete [shostak](4.86 s)
dual_fixpoint_induction...............proved - complete [shostak](1.94 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (6.80 s)
Proof summary for theory scott_product
product_order_TCC1....................proved - complete [shostak](0.18 s)
IMP_scott_TCC1........................proved - complete [shostak](0.14 s)
IMP_scott_TCC2........................proved - complete [shostak](0.13 s)
IMP_scott_TCC3........................proved - complete [shostak](0.28 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.73 s)
Grand Totals: 76 proofs, 76 attempted, 76 succeeded (54.07 s)
[ zur Elbe Produktseite wechseln0.138Quellennavigators
]
