*** 
*** top (22:1:41 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 complex_topology
    IMP_metric_space_TCC1.................proved - complete   [shostak](0.61 s)
    complex_is_complete...................proved - complete   [shostak](1.08 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.68 s)

 Proof summary for theory complex_measurable
    complex_measurable_TCC1...............proved - complete   [shostak](0.09 s)
    complex_measurable_def................proved - complete   [shostak](0.06 s)
    constant_is_complex_measurable........proved - complete   [shostak](0.09 s)
    scal_complex_measurable...............proved - incomplete [shostak](0.42 s)
    sum_complex_measurable................proved - incomplete [shostak](0.08 s)
    opp_complex_measurable................proved - incomplete [shostak](0.19 s)
    diff_complex_measurable...............proved - incomplete [shostak](-1.99 s)
    const_measurable......................proved - complete   [shostak](0.07 s)
    abs_complex_measurable................proved - incomplete [shostak](0.44 s)
    sq_complex_measurable.................proved - incomplete [shostak](0.32 s)
    prod_complex_measurable...............proved - incomplete [shostak](0.25 s)
    abs_expt_measurable...................proved - incomplete [shostak](0.08 s)
    pointwise_complex_measurable..........proved - incomplete [shostak](0.40 s)
    Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.49 s)

 Proof summary for theory complex_measure_theory
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    cal_N_TCC1............................proved - complete   [shostak](0.13 s)
    cal_N_is_measurable...................proved - complete   [shostak](0.11 s)
    cal_N_def.............................proved - complete   [shostak](0.26 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.54 s)

 Proof summary for theory complex_integral
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    integrable_TCC1.......................proved - incomplete [shostak](0.10 s)
    integral_TCC1.........................proved - incomplete [shostak](0.07 s)
    integral_TCC2.........................proved - incomplete [shostak](0.07 s)
    integrable_def........................proved - complete   [shostak](0.07 s)
    Re_integral...........................proved - incomplete [shostak](0.07 s)
    Im_integral...........................proved - incomplete [shostak](0.07 s)
    integrable_is_measurable..............proved - incomplete [shostak](0.08 s)
    cal_N_is_measurable...................proved - incomplete [shostak](0.11 s)
    integrable_add........................proved - incomplete [shostak](0.42 s)
    integrable_scal.......................proved - incomplete [shostak](0.16 s)
    integrable_opp........................proved - incomplete [shostak](0.09 s)
    integrable_diff.......................proved - incomplete [shostak](0.08 s)
    integrable_abs........................proved - incomplete [shostak](0.51 s)
    integral_add..........................proved - incomplete [shostak](0.17 s)
    integral_scal.........................proved - incomplete [shostak](0.35 s)
    integral_opp..........................proved - incomplete [shostak](0.69 s)
    integral_diff.........................proved - incomplete [shostak](0.55 s)
    integral_abs..........................proved - incomplete [shostak](2.50 s)
    Theory totals: 19 formulas, 19 attempted, 19 succeeded (6.19 s)

 Proof summary for theory p_integrable_def
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    p_integrable?_TCC1....................proved - complete   [shostak](0.08 s)
    p_integrable_TCC1.....................proved - incomplete [shostak](0.17 s)
    cal_N_is_p_integrable.................proved - incomplete [shostak](0.17 s)
    norm_TCC1.............................proved - incomplete [shostak](0.08 s)
    norm_TCC2.............................proved - incomplete [shostak](0.09 s)
    norm_TCC3.............................proved - incomplete [shostak](0.13 s)
    norm_TCC4.............................proved - incomplete [shostak](0.08 s)
    norm_TCC5.............................proved - incomplete [shostak](0.13 s)
    norm_eq_0.............................proved - incomplete [shostak](0.35 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (1.33 s)

 Proof summary for theory young
    youngs_aux_TCC1.......................proved - complete   [shostak](0.05 s)
    youngs_aux............................proved - incomplete [shostak](1.75 s)
    youngs_inequality_TCC1................proved - complete   [shostak](0.07 s)
    youngs_inequality_TCC2................proved - complete   [shostak](0.06 s)
    youngs_inequality.....................proved - incomplete [shostak](2.14 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (4.07 s)

 Proof summary for theory holder_scaf
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    q_TCC1................................proved - complete   [shostak](0.03 s)
    f_TCC1................................proved - complete   [shostak](0.11 s)
    g_TCC1................................proved - complete   [shostak](0.23 s)
    holder_aux............................proved - incomplete [shostak](4.15 s)
    holder_judge1.........................proved - incomplete [shostak](0.13 s)
    holder_judge2.........................proved - incomplete [shostak](0.22 s)
    holder_scaf...........................proved - incomplete [shostak](0.12 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (5.02 s)

 Proof summary for theory minkowski_scaf
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    minkowski_scaf........................proved - incomplete [shostak](3.93 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (3.97 s)

 Proof summary for theory p_integrable
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    scal_p_integrable.....................proved - incomplete [shostak](0.28 s)
    sum_p_integrable......................proved - incomplete [shostak](0.08 s)
    opp_p_integrable......................proved - incomplete [shostak](0.10 s)
    diff_p_integrable.....................proved - incomplete [shostak](0.31 s)
    norm_scal.............................proved - incomplete [shostak](0.45 s)
    norm_add..............................proved - incomplete [shostak](0.08 s)
    norm_opp..............................proved - incomplete [shostak](0.13 s)
    norm_diff.............................proved - incomplete [shostak](0.21 s)
    Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.68 s)

 Proof summary for theory essentially_bounded
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    essentially_bounded_TCC1..............proved - complete   [shostak](0.16 s)
    essential_bound_TCC1..................proved - complete   [shostak](0.13 s)
    essential_bound_TCC2..................proved - complete   [shostak](0.15 s)
    essential_bound_def1..................proved - complete   [shostak](0.14 s)
    essential_bound_def2..................proved - incomplete [shostak](1.46 s)
    scal_essentially_bounded..............proved - incomplete [shostak](0.32 s)
    add_essentially_bounded...............proved - incomplete [shostak](0.30 s)
    opp_essentially_bounded...............proved - incomplete [shostak](0.65 s)
    diff_essentially_bounded..............proved - incomplete [shostak](0.16 s)
    prod_essentially_bounded..............proved - incomplete [shostak](0.31 s)
    essential_bound_scal..................proved - incomplete [shostak](0.40 s)
    essential_bound_add...................proved - incomplete [shostak](0.27 s)
    essential_bound_opp...................proved - incomplete [shostak](0.22 s)
    essential_bound_diff..................proved - incomplete [shostak](1.09 s)
    essential_bound_eq_0..................proved - incomplete [shostak](0.18 s)
    essential_bound_prod..................proved - incomplete [shostak](0.30 s)
    holder_judge_infty_1..................proved - incomplete [shostak](0.32 s)
    holder_judge_infty_2..................proved - incomplete [shostak](0.70 s)
    holder_infty_1........................proved - incomplete [shostak](0.36 s)
    holder_infty_2........................proved - incomplete [shostak](0.22 s)
    Theory totals: 21 formulas, 21 attempted, 21 succeeded (7.86 s)

 Proof summary for theory essential_bound_complete_scaf
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    essential_bound_complete_scaf.........proved - incomplete [shostak](5.07 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (5.11 s)

 Proof summary for theory cal_L_inf
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    cal_L_infty_TCC1......................proved - complete   [shostak](0.13 s)
    cal_L_infty_is_essentially_bounded....proved - complete   [shostak](0.46 s)
    scal_cal_L_infty......................proved - incomplete [shostak](0.07 s)
    add_cal_L_infty.......................proved - incomplete [shostak](0.07 s)
    opp_cal_L_infty.......................proved - incomplete [shostak](0.07 s)
    diff_cal_L_infty......................proved - incomplete [shostak](0.07 s)
    prod_cal_L_infty......................proved - incomplete [shostak](0.07 s)
    inf_norm_scal.........................proved - incomplete [shostak](0.40 s)
    inf_norm_add..........................proved - incomplete [shostak](0.28 s)
    inf_norm_opp..........................proved - incomplete [shostak](0.07 s)
    inf_norm_diff.........................proved - incomplete [shostak](0.08 s)
    inf_norm_eq_0.........................proved - incomplete [shostak](0.51 s)
    inf_norm_prod.........................proved - incomplete [shostak](0.29 s)
    holder_infty_1........................proved - incomplete [shostak](0.07 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (2.69 s)

 Proof summary for theory complex_finite_measures
    mu_TCC1...............................proved - complete   [shostak](0.04 s)
    q_integrable_is_p_integrable..........proved - incomplete [shostak](0.81 s)
    essentially_bounded_is_p_integrable...proved - incomplete [shostak](0.32 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.16 s)

 Proof summary for theory cal_L_complex
    mu_TCC1...............................proved - complete   [shostak](0.05 s)
    cal_L_complex_infty_TCC1..............proved - complete   [shostak](0.17 s)
    cal_L_complex_infty_TCC2..............proved - complete   [shostak](0.10 s)
    cal_L_complex_infty_is_essentially_bounded...proved - complete   [shostak](0.05 s)
    cal_L_complex_TCC1....................proved - incomplete [shostak](0.12 s)
    cal_L_complex_TCC2....................proved - incomplete [shostak](0.12 s)
    cal_L_complex_is_p_integrable.........proved - complete   [shostak](0.05 s)
    cal_L_complex_1_def...................proved - incomplete [shostak](0.45 s)
    scal_cal_L............................proved - incomplete [shostak](0.06 s)
    sum_cal_L.............................proved - incomplete [shostak](0.05 s)
    opp_cal_L.............................proved - incomplete [shostak](0.05 s)
    diff_cal_L............................proved - incomplete [shostak](0.06 s)
    prod_cal_L_TCC1.......................proved - complete   [shostak](0.04 s)
    prod_cal_L_TCC2.......................proved - complete   [shostak](0.05 s)
    prod_cal_L............................proved - incomplete [shostak](0.14 s)
    scal_cal_L_infty......................proved - incomplete [shostak](0.06 s)
    sum_cal_L_infty.......................proved - incomplete [shostak](0.06 s)
    opp_cal_L_infty.......................proved - incomplete [shostak](0.06 s)
    diff_cal_L_infty......................proved - incomplete [shostak](0.05 s)
    prod_cal_L_infty......................proved - incomplete [shostak](0.06 s)
    prod_cal_L_1_infty....................proved - incomplete [shostak](0.05 s)
    prod_cal_L_infty_1....................proved - incomplete [shostak](0.06 s)
    scal_cal_L_fm.........................proved - incomplete [shostak](0.05 s)
    sum_cal_L_fm..........................proved - incomplete [shostak](0.06 s)
    opp_cal_L_fm..........................proved - incomplete [shostak](0.05 s)
    diff_cal_L_fm.........................proved - incomplete [shostak](0.05 s)
    prod_cal_L_fm.........................proved - incomplete [shostak](0.11 s)
    scal_cal_L_infty_fm...................proved - incomplete [shostak](0.05 s)
    sum_cal_L_infty_fm....................proved - incomplete [shostak](0.06 s)
    opp_cal_L_infty_fm....................proved - incomplete [shostak](0.05 s)
    diff_cal_L_infty_fm...................proved - incomplete [shostak](0.05 s)
    prod_cal_L_infty_fm...................proved - incomplete [shostak](0.05 s)
    prod_cal_L_1_infty_fm.................proved - incomplete [shostak](0.05 s)
    prod_cal_L_infty_1_fm.................proved - incomplete [shostak](0.05 s)
    Theory totals: 34 formulas, 34 attempted, 34 succeeded (2.65 s)

 Proof summary for theory cal_L_real
    mu_TCC1...............................proved - complete   [shostak](0.05 s)
    cal_L_real_infty_TCC1.................proved - complete   [shostak](0.15 s)
    cal_L_real_infty_TCC2.................proved - complete   [shostak](0.17 s)
    cal_L_real_TCC1.......................proved - incomplete [shostak](0.09 s)
    cal_L_real_TCC2.......................proved - incomplete [shostak](0.10 s)
    cal_L_real_1_def......................proved - incomplete [shostak](0.07 s)
    scal_cal_LR...........................proved - incomplete [shostak](0.08 s)
    sum_cal_LR............................proved - incomplete [shostak](0.07 s)
    opp_cal_LR............................proved - incomplete [shostak](0.05 s)
    diff_cal_LR...........................proved - incomplete [shostak](0.07 s)
    prod_cal_LR_TCC1......................proved - complete   [shostak](0.04 s)
    prod_cal_LR_TCC2......................proved - complete   [shostak](0.05 s)
    prod_cal_LR...........................proved - incomplete [shostak](0.14 s)
    scal_cal_L_inftyR.....................proved - incomplete [shostak](0.11 s)
    sum_cal_L_inftyR......................proved - incomplete [shostak](0.06 s)
    opp_cal_L_inftyR......................proved - incomplete [shostak](0.06 s)
    diff_cal_L_inftyR.....................proved - incomplete [shostak](0.06 s)
    prod_cal_L_inftyR.....................proved - incomplete [shostak](0.12 s)
    prod_cal_L_1_inftyR...................proved - incomplete [shostak](0.11 s)
    prod_cal_L_infty_1R...................proved - incomplete [shostak](0.11 s)
    scal_cal_L_fmR........................proved - incomplete [shostak](0.06 s)
    sum_cal_L_fmR.........................proved - incomplete [shostak](0.05 s)
    opp_cal_L_fmR.........................proved - incomplete [shostak](0.05 s)
    diff_cal_L_fmR........................proved - incomplete [shostak](0.04 s)
    prod_cal_L_fmR........................proved - incomplete [shostak](0.12 s)
    scal_cal_L_infty_fmR..................proved - incomplete [shostak](0.05 s)
    sum_cal_L_infty_fmR...................proved - incomplete [shostak](0.05 s)
    opp_cal_L_infty_fmR...................proved - incomplete [shostak](0.05 s)
    diff_cal_L_infty_fmR..................proved - incomplete [shostak](0.05 s)
    prod_cal_L_infty_fmR..................proved - incomplete [shostak](0.05 s)
    prod_cal_L_1_infty_fmR................proved - incomplete [shostak](0.06 s)
    prod_cal_L_infty_1_fmR................proved - incomplete [shostak](0.06 s)
    Theory totals: 32 formulas, 32 attempted, 32 succeeded (2.45 s)

Grand Totals: 179 proofs, 179 attempted, 179 succeeded (46.91 s)