Quelle  scott.summary   Sprache: unbekannt

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