*** 
*** top (22:54:31 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 continuous_functions_aux
    continuous_lr_def.....................proved - complete   [shostak](-.87 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (-0.87 s)

 Proof summary for theory probability_measure
    trivial_probability_measure_TCC1......proved - complete   [shostak](0.05 s)
    probability_measure_TCC1..............proved - complete   [shostak](0.17 s)
    probability_measure_is_finite_measure...proved - complete   [shostak](0.19 s)
    random_variable_TCC1..................proved - complete   [shostak](0.13 s)
    P_fullset.............................proved - complete   [shostak](0.02 s)
    P_convergence.........................proved - complete   [shostak](0.06 s)
    P_emptyset............................proved - complete   [shostak](0.03 s)
    P_disjointunion.......................proved - complete   [shostak](0.11 s)
    P_complement..........................proved - complete   [shostak](0.25 s)
    P_union...............................proved - complete   [shostak](0.44 s)
    P_intersection........................proved - complete   [shostak](0.12 s)
    P_difference..........................proved - complete   [shostak](0.02 s)
    P_subset..............................proved - complete   [shostak](0.13 s)
    P_subset_le...........................proved - complete   [shostak](0.06 s)
    P_IUnion..............................proved - complete   [shostak](0.08 s)
    P_IIntersection.......................proved - complete   [shostak](0.04 s)
    P0_intersection.......................proved - complete   [shostak](0.05 s)
    P0_union..............................proved - complete   [shostak](0.08 s)
    P1_intersection.......................proved - complete   [shostak](0.28 s)
    P1_union..............................proved - complete   [shostak](0.12 s)
    measure_to_df_TCC1....................proved - incomplete [shostak](0.13 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (2.57 s)

 Proof summary for theory probability_space
    zero_TCC1.............................proved - complete   [shostak](0.02 s)
    one_TCC1..............................proved - complete   [shostak](0.01 s)
    lesseqp_TCC1..........................proved - incomplete [shostak](0.02 s)
    lessp_TCC1............................proved - incomplete [shostak](0.13 s)
    equal_TCC1............................proved - incomplete [shostak](0.41 s)
    lessp_TCC2............................proved - incomplete [shostak](0.13 s)
    lesseqp_TCC2..........................proved - incomplete [shostak](0.02 s)
    notequal_TCC1.........................proved - incomplete [shostak](0.24 s)
    complement_le1........................proved - incomplete [shostak](0.03 s)
    complement_lt1........................proved - incomplete [shostak](0.02 s)
    complement_eq.........................proved - incomplete [shostak](0.02 s)
    complement_lt2........................proved - incomplete [shostak](0.03 s)
    complement_le2........................proved - incomplete [shostak](0.03 s)
    complement_ne.........................proved - incomplete [shostak](0.03 s)
    plus_TCC1.............................proved - incomplete [shostak](0.13 s)
    plus_TCC2.............................proved - incomplete [shostak](0.05 s)
    difference_TCC1.......................proved - incomplete [shostak](0.14 s)
    difference_TCC2.......................proved - incomplete [shostak](0.02 s)
    divide_TCC1...........................proved - incomplete [shostak](0.18 s)
    independent?_TCC1.....................proved - complete   [shostak](0.20 s)
    borel_independence....................proved - complete   [shostak](0.08 s)
    partial_sum_is_random_variable_TCC1...proved - complete   [shostak](0.01 s)
    partial_sum_is_random_variable........proved - incomplete [shostak](0.14 s)
    distribution_function_TCC1............proved - incomplete [shostak](0.04 s)
    invert_distribution...................proved - incomplete [shostak](0.05 s)
    interval_distribution.................proved - incomplete [shostak](0.21 s)
    limit_distribution_TCC1...............proved - incomplete [shostak](0.21 s)
    limit_distribution....................proved - incomplete [shostak](0.58 s)
    distribution_0........................proved - incomplete [shostak](0.20 s)
    distribution_1........................proved - incomplete [shostak](0.13 s)
    distribution_increasing...............proved - incomplete [shostak](0.04 s)
    distribution_right_continuous.........proved - incomplete [shostak](0.47 s)
    Theory totals: 32 formulas, 32 attempted, 32 succeeded (4.03 s)

 Proof summary for theory conditional
    P_TCC1................................proved - complete   [shostak](0.02 s)
    P_TCC2................................proved - complete   [shostak](0.25 s)
    conditional_complement................proved - complete   [shostak](0.59 s)
    conditional_partition_TCC1............proved - complete   [shostak](0.03 s)
    conditional_partition.................proved - complete   [shostak](0.52 s)
    bayes_theorem_TCC1....................proved - complete   [shostak](0.07 s)
    bayes_theorem.........................proved - complete   [shostak](0.27 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.76 s)

 Proof summary for theory expectation
    E_zero_TCC1...........................proved - incomplete [shostak](0.04 s)
    E_zero................................proved - incomplete [shostak](0.04 s)
    E_one_TCC1............................proved - incomplete [shostak](0.24 s)
    E_one.................................proved - incomplete [shostak](0.08 s)
    E_phi_TCC1............................proved - incomplete [shostak](0.07 s)
    E_phi.................................proved - incomplete [shostak](0.04 s)
    E_add.................................proved - incomplete [shostak](0.05 s)
    E_scal................................proved - incomplete [shostak](0.04 s)
    E_opp.................................proved - incomplete [shostak](0.05 s)
    E_diff................................proved - incomplete [shostak](0.05 s)
    E_nonneg..............................proved - incomplete [shostak](0.04 s)
    markov_inequality_TCC1................proved - incomplete [shostak](0.06 s)
    markov_inequality.....................proved - incomplete [shostak](1.08 s)
    markov_inequality_alt.................proved - incomplete [shostak](0.16 s)
    Theory totals: 14 formulas, 14 attempted, 14 succeeded (2.04 s)

Grand Totals: 75 proofs, 75 attempted, 75 succeeded (9.53 s)