Quelle  sets_aux.summary   Sprache: unbekannt

*** 
*** top (17:29:56 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 fun_below_props
    cartesian_bijection...................proved - complete   [shostak](-.37 s)
    empty_domain1.........................proved - complete   [shostak](0.02 s)
    empty_domain2.........................proved - complete   [shostak](0.01 s)
    empty_range...........................proved - complete   [shostak](0.02 s)
    funset_bijection_TCC1.................proved - complete   [shostak](0.01 s)
    funset_bijection......................proved - complete   [shostak](0.80 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.49 s)

 Proof summary for theory power_sets
    B_TCC1................................proved - complete   [shostak](0.03 s)
    card_B................................proved - complete   [shostak](0.19 s)
    powerset_bijection....................proved - complete   [shostak](0.84 s)
    finite_powerset_bijection.............proved - incomplete [shostak](0.06 s)
    card_powerset.........................proved - incomplete [shostak](0.13 s)
    elem_finite_powerset..................proved - complete   [shostak](0.01 s)
    finite_subset_of_powerset.............proved - complete   [shostak](0.03 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.28 s)

 Proof summary for theory set_of_functions
    empty_finite_domain1..................proved - complete   [shostak](0.03 s)
    empty_finite_domain2..................proved - complete   [shostak](0.04 s)
    empty_finite_range....................proved - complete   [shostak](0.04 s)
    finite_funset_bijection1..............proved - incomplete [shostak](0.34 s)
    finite_funset_bijection2_TCC1.........proved - complete   [shostak](0.02 s)
    finite_funset_bijection2..............proved - incomplete [shostak](0.04 s)
    finite_funset.........................proved - incomplete [shostak](0.04 s)
    funset_TCC1...........................proved - incomplete [shostak](0.01 s)
    card_funset_TCC1......................proved - complete   [shostak](0.04 s)
    card_funset...........................proved - incomplete [shostak](0.13 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.73 s)

 Proof summary for theory bits
    bounding_bits_has_least...............proved - complete   [shostak](0.35 s)
    bit_decoding_TCC1.....................proved - complete   [shostak](0.31 s)
    bit_decoding_TCC2.....................proved - complete   [shostak](0.24 s)
    bit_decoding_TCC3.....................proved - complete   [shostak](0.33 s)
    bit_decoding_TCC4.....................proved - complete   [shostak](0.24 s)
    bit_decoding_has_greatest.............proved - incomplete [shostak](0.24 s)
    bit_decoding_max1_TCC1................proved - incomplete [shostak](0.02 s)
    bit_decoding_max1.....................proved - incomplete [shostak](1.03 s)
    bit_decoding_max2_TCC1................proved - complete   [shostak](0.01 s)
    bit_decoding_max2.....................proved - incomplete [shostak](1.10 s)
    bit_decoding_max3.....................proved - incomplete [shostak](0.56 s)
    bit_encoding_TCC1.....................proved - incomplete [shostak](0.21 s)
    bit_encoding_TCC2.....................proved - incomplete [shostak](0.25 s)
    bit_encoding_member1..................proved - incomplete [shostak](0.32 s)
    bit_encoding_member2..................proved - incomplete [shostak](0.87 s)
    bit_encoding_member3_TCC1.............proved - incomplete [shostak](0.37 s)
    bit_encoding_member3..................proved - incomplete [shostak](0.63 s)
    decoding_encoding_max_TCC1............proved - incomplete [shostak](0.37 s)
    decoding_encoding_max.................proved - incomplete [shostak](0.52 s)
    decoding_encoding_empty...............proved - incomplete [shostak](0.27 s)
    decoding_encoding_remove..............proved - incomplete [shostak](0.74 s)
    encoding_decoding.....................proved - incomplete [shostak](1.22 s)
    decoding_encoding.....................proved - incomplete [shostak](1.46 s)
    encoding_bijection....................proved - incomplete [shostak](0.37 s)
    decoding_bijection....................proved - incomplete [shostak](0.37 s)
    encoding_decoding_inverse.............proved - incomplete [shostak](0.27 s)
    decoding_encoding_inverse.............proved - incomplete [shostak](0.27 s)
    Theory totals: 27 formulas, 27 attempted, 27 succeeded (12.93 s)

 Proof summary for theory card_comp
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory card_comp_props
    card_lt_surj..........................proved - complete   [shostak](0.72 s)
    card_ge_surj..........................proved - complete   [shostak](1.30 s)
    card_lt_le............................proved - complete   [shostak](0.01 s)
    card_gt_ge............................proved - complete   [shostak](0.01 s)
    card_lt_gt............................proved - complete   [shostak](0.01 s)
    card_le_ge............................proved - complete   [shostak](0.01 s)
    card_gt_lt............................proved - complete   [shostak](0.01 s)
    card_ge_le............................proved - complete   [shostak](0.00 s)
    card_lt_ge............................proved - complete   [shostak](0.01 s)
    card_le_gt............................proved - complete   [shostak](0.01 s)
    card_eq_le_ge.........................proved - complete   [shostak](0.91 s)
    card_le_lt_eq.........................proved - complete   [shostak](0.22 s)
    card_ge_gt_eq.........................proved - complete   [shostak](0.02 s)
    card_lt_neq_ngt.......................proved - complete   [shostak](0.01 s)
    card_gt_neq_nlt.......................proved - complete   [shostak](0.12 s)
    card_lt_anticommutative...............proved - complete   [shostak](0.01 s)
    card_le_antisymmetric.................proved - complete   [shostak](0.01 s)
    card_eq_symmetric.....................proved - complete   [shostak](0.82 s)
    card_ge_antisymmetric.................proved - complete   [shostak](0.01 s)
    card_gt_anticommutative...............proved - complete   [shostak](0.01 s)
    card_lt_trichotomous..................proved - complete   [shostak](0.01 s)
    card_le_dichotomous...................proved - complete   [shostak](0.01 s)
    card_ge_dichotomous...................proved - complete   [shostak](0.01 s)
    card_gt_trichotomous..................proved - complete   [shostak](0.01 s)
    Theory totals: 24 formulas, 24 attempted, 24 succeeded (4.27 s)

 Proof summary for theory card_comp_set
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory card_comp_set_props
    card_lt_surj..........................proved - complete   [shostak](0.73 s)
    card_ge_surj..........................proved - complete   [shostak](1.32 s)
    card_lt_le............................proved - complete   [shostak](0.02 s)
    card_gt_ge............................proved - complete   [shostak](0.02 s)
    card_lt_gt............................proved - complete   [shostak](0.01 s)
    card_le_ge............................proved - complete   [shostak](0.02 s)
    card_gt_lt............................proved - complete   [shostak](0.01 s)
    card_ge_le............................proved - complete   [shostak](0.02 s)
    card_lt_ge............................proved - complete   [shostak](0.02 s)
    card_le_gt............................proved - complete   [shostak](0.03 s)
    card_eq_le_ge.........................proved - complete   [shostak](0.43 s)
    card_le_lt_eq.........................proved - complete   [shostak](0.03 s)
    card_ge_gt_eq.........................proved - complete   [shostak](0.04 s)
    card_lt_neq_ngt.......................proved - complete   [shostak](0.02 s)
    card_gt_neq_nlt.......................proved - complete   [shostak](0.03 s)
    card_lt_anticommutative...............proved - complete   [shostak](0.02 s)
    card_le_antisymmetric.................proved - complete   [shostak](0.02 s)
    card_eq_symmetric.....................proved - complete   [shostak](0.83 s)
    card_ge_antisymmetric.................proved - complete   [shostak](0.03 s)
    card_gt_anticommutative...............proved - complete   [shostak](0.02 s)
    card_lt_trichotomous..................proved - complete   [shostak](0.02 s)
    card_le_dichotomous...................proved - complete   [shostak](0.02 s)
    card_ge_dichotomous...................proved - complete   [shostak](0.31 s)
    card_gt_trichotomous..................proved - complete   [shostak](0.02 s)
    Theory totals: 24 formulas, 24 attempted, 24 succeeded (4.05 s)

 Proof summary for theory card_comp_set_transitive
    card_lt_transitive....................proved - complete   [shostak](0.32 s)
    card_lt_le_transitive.................proved - complete   [shostak](0.32 s)
    card_lt_eq_transitive.................proved - complete   [shostak](0.32 s)
    card_le_lt_transitive.................proved - complete   [shostak](0.32 s)
    card_eq_lt_transitive.................proved - complete   [shostak](0.33 s)
    card_le_transitive....................proved - complete   [shostak](0.32 s)
    card_le_eq_transitive.................proved - complete   [shostak](0.32 s)
    card_eq_le_transitive.................proved - complete   [shostak](0.33 s)
    card_eq_transitive....................proved - complete   [shostak](0.32 s)
    card_eq_ge_transitive.................proved - complete   [shostak](0.73 s)
    card_ge_eq_transitive.................proved - complete   [shostak](0.73 s)
    card_ge_transitive....................proved - complete   [shostak](0.32 s)
    card_eq_gt_transitive.................proved - complete   [shostak](0.73 s)
    card_ge_gt_transitive.................proved - complete   [shostak](0.32 s)
    card_gt_eq_transitive.................proved - complete   [shostak](0.73 s)
    card_gt_ge_transitive.................proved - complete   [shostak](0.32 s)
    card_gt_transitive....................proved - complete   [shostak](0.43 s)
    Theory totals: 17 formulas, 17 attempted, 17 succeeded (7.22 s)

 Proof summary for theory card_comp_transitive
    card_lt_transitive....................proved - complete   [shostak](0.31 s)
    card_lt_le_transitive.................proved - complete   [shostak](0.30 s)
    card_lt_eq_transitive.................proved - complete   [shostak](0.31 s)
    card_le_lt_transitive.................proved - complete   [shostak](0.31 s)
    card_eq_lt_transitive.................proved - complete   [shostak](0.30 s)
    card_le_transitive....................proved - complete   [shostak](0.31 s)
    card_le_eq_transitive.................proved - complete   [shostak](0.31 s)
    card_eq_le_transitive.................proved - complete   [shostak](0.31 s)
    card_eq_transitive....................proved - complete   [shostak](0.30 s)
    card_eq_ge_transitive.................proved - complete   [shostak](0.71 s)
    card_ge_eq_transitive.................proved - complete   [shostak](0.71 s)
    card_ge_transitive....................proved - complete   [shostak](0.31 s)
    card_eq_gt_transitive.................proved - complete   [shostak](0.71 s)
    card_ge_gt_transitive.................proved - complete   [shostak](0.30 s)
    card_gt_eq_transitive.................proved - complete   [shostak](0.71 s)
    card_gt_ge_transitive.................proved - complete   [shostak](0.30 s)
    card_gt_transitive....................proved - complete   [shostak](0.31 s)
    Theory totals: 17 formulas, 17 attempted, 17 succeeded (6.83 s)

 Proof summary for theory card_finite
    card_less_than........................proved - complete   [shostak](1.92 s)
    card_less_than_equal..................proved - complete   [shostak](1.93 s)
    card_equal............................proved - complete   [shostak](0.63 s)
    card_greater_than_equal...............proved - complete   [shostak](0.32 s)
    card_greater_than.....................proved - complete   [shostak](0.33 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (5.13 s)

 Proof summary for theory card_power
    card_power............................proved - complete   [shostak](0.02 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s)

 Proof summary for theory card_power_set
    card_power............................proved - complete   [shostak](0.07 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.07 s)

 Proof summary for theory card_sets_lemmas
    empty_card_le.........................proved - complete   [shostak](0.24 s)
    nonempty_card_lt......................proved - complete   [shostak](1.58 s)
    full_card_le..........................proved - complete   [shostak](0.24 s)
    add_card_le...........................proved - complete   [shostak](0.25 s)
    remove_card_ge........................proved - complete   [shostak](0.26 s)
    subset_card_le........................proved - complete   [shostak](0.56 s)
    strict_subset_card_lt.................proved - complete   [shostak](0.02 s)
    union_card_le1........................proved - complete   [shostak](0.24 s)
    union_card_le2........................proved - complete   [shostak](0.25 s)
    intersection_card_le1.................proved - complete   [shostak](0.26 s)
    intersection_card_le2.................proved - complete   [shostak](0.26 s)
    difference_card_le....................proved - complete   [shostak](0.25 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (4.41 s)

 Proof summary for theory card_single
    card_lt_is_irreflexive................proved - complete   [shostak](0.02 s)
    card_le_is_reflexive..................proved - complete   [shostak](0.03 s)
    card_eq_is_reflexive..................proved - complete   [shostak](0.02 s)
    card_ge_is_reflexive..................proved - complete   [shostak](0.03 s)
    card_gt_is_irreflexive................proved - complete   [shostak](0.03 s)
    card_lt_is_antisymmetric..............proved - complete   [shostak](0.01 s)
    card_eq_is_symmetric..................proved - complete   [shostak](0.02 s)
    card_gt_is_antisymmetric..............proved - complete   [shostak](0.02 s)
    card_lt_is_transitive.................proved - complete   [shostak](0.02 s)
    card_le_is_transitive.................proved - complete   [shostak](0.03 s)
    card_eq_is_transitive.................proved - complete   [shostak](0.03 s)
    card_ge_is_transitive.................proved - complete   [shostak](0.03 s)
    card_gt_is_transitive.................proved - complete   [shostak](0.03 s)
    card_le_is_dichotomous................proved - complete   [shostak](0.03 s)
    card_ge_is_dichotomous................proved - complete   [shostak](0.04 s)
    card_eq_is_equivalence................proved - complete   [shostak](0.04 s)
    Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.44 s)

 Proof summary for theory card_function
    infinite_bijection....................proved - complete   [shostak](0.05 s)
    finite_bijection......................proved - complete   [shostak](0.05 s)
    infinite_injection....................proved - complete   [shostak](0.04 s)
    finite_injection......................proved - complete   [shostak](0.01 s)
    infinite_surjection...................proved - complete   [shostak](0.05 s)
    finite_surjection.....................proved - complete   [shostak](0.01 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.22 s)

 Proof summary for theory cardinal
    cardinal_member.......................proved - complete   [shostak](0.02 s)
    cardinal_closed.......................proved - complete   [shostak](0.05 s)
    cardinal_empty........................proved - complete   [shostak](0.79 s)
    cardinal_finite.......................proved - complete   [shostak](0.11 s)
    cardinal_finite_card_TCC1.............proved - complete   [shostak](0.02 s)
    cardinal_finite_card..................proved - complete   [shostak](0.04 s)
    cardinal_equality.....................proved - complete   [shostak](0.08 s)
    cardinal_lt...........................proved - complete   [shostak](0.08 s)
    cardinal_le...........................proved - complete   [shostak](0.08 s)
    cardinal_eq...........................proved - complete   [shostak](0.05 s)
    cardinal_ge...........................proved - complete   [shostak](0.09 s)
    cardinal_gt...........................proved - complete   [shostak](0.09 s)
    cardinal_card_lt......................proved - complete   [shostak](0.32 s)
    cardinal_card_le......................proved - complete   [shostak](0.32 s)
    cardinal_card_eq......................proved - complete   [shostak](0.32 s)
    cardinal_card_ge......................proved - complete   [shostak](0.32 s)
    cardinal_card_gt......................proved - complete   [shostak](0.32 s)
    cardinal_lt_gt........................proved - complete   [shostak](0.03 s)
    cardinal_le_ge........................proved - complete   [shostak](0.02 s)
    cardinal_lt_le........................proved - complete   [shostak](0.05 s)
    cardinal_le_lt........................proved - complete   [shostak](0.03 s)
    cardinal_eq_lg........................proved - complete   [shostak](0.04 s)
    cardinal_ge_gt........................proved - complete   [shostak](0.03 s)
    cardinal_gt_ge........................proved - complete   [shostak](0.04 s)
    cardinal_lt_not_ge....................proved - complete   [shostak](0.02 s)
    cardinal_le_not_gt....................proved - complete   [shostak](0.02 s)
    cardinal_eq_not_lg....................proved - complete   [shostak](0.04 s)
    cardinal_ge_not_lt....................proved - complete   [shostak](0.03 s)
    cardinal_gt_not_le....................proved - complete   [shostak](0.03 s)
    cardinal_lt_strict_total_order........proved - complete   [shostak](0.06 s)
    cardinal_le_total_order...............proved - complete   [shostak](0.08 s)
    cardinal_ge_total_order...............proved - complete   [shostak](0.08 s)
    cardinal_gt_strict_total_order........proved - complete   [shostak](0.06 s)
    cardinal_lt_le_transitive.............proved - complete   [shostak](0.03 s)
    cardinal_le_lt_transitive.............proved - complete   [shostak](0.03 s)
    cardinal_ge_gt_transitive.............proved - complete   [shostak](0.03 s)
    cardinal_gt_ge_transitive.............proved - complete   [shostak](0.03 s)
    cardinal_empty_least..................proved - complete   [shostak](0.05 s)
    cardinal_full_greatest................proved - complete   [shostak](0.05 s)
    Theory totals: 39 formulas, 39 attempted, 39 succeeded (3.99 s)

 Proof summary for theory countability
    countable_set_TCC1....................proved - complete   [shostak](0.08 s)
    countably_infinite_countable..........proved - complete   [shostak](0.80 s)
    countably_infinite_subset.............proved - complete   [shostak](0.60 s)
    countable_subset......................proved - complete   [shostak](0.69 s)
    countable_type_is_countably_infinite...proved - complete   [shostak](0.22 s)
    countable_full........................proved - complete   [shostak](1.27 s)
    countably_infinite_full...............proved - complete   [shostak](4.55 s)
    uncountable_full......................proved - complete   [shostak](0.06 s)
    countable_type_set....................proved - complete   [shostak](0.38 s)
    countably_infinite_type_set...........proved - complete   [shostak](0.53 s)
    uncountably_infinite_type_set.........proved - complete   [shostak](0.07 s)
    countable_complement..................proved - complete   [shostak](0.06 s)
    countably_infinite_complement.........proved - complete   [shostak](0.06 s)
    Theory totals: 13 formulas, 13 attempted, 13 succeeded (9.35 s)

 Proof summary for theory countable_image
    countable_image.......................proved - complete   [shostak](0.08 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)

 Proof summary for theory infinite_image
    infinite_image........................proved - complete   [shostak](0.07 s)
    infinite_injective_image..............proved - complete   [shostak](0.05 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s)

 Proof summary for theory countable_props
    infinite_countably_infinite...........proved - complete   [shostak](0.03 s)
    countably_infinite_add................proved - complete   [shostak](0.19 s)
    countable_add.........................proved - complete   [shostak](0.13 s)
    countably_infinite_remove.............proved - complete   [shostak](0.35 s)
    countable_remove......................proved - complete   [shostak](0.12 s)
    countably_infinite_rest...............proved - complete   [shostak](0.08 s)
    countable_rest........................proved - complete   [shostak](0.08 s)
    countable_intersection1...............proved - complete   [shostak](0.42 s)
    countable_intersection2...............proved - complete   [shostak](0.08 s)
    countably_infinite_difference.........proved - complete   [shostak](0.21 s)
    countable_difference..................proved - complete   [shostak](0.74 s)
    finite_countable......................proved - complete   [shostak](0.71 s)
    infinite_uncountable..................proved - complete   [shostak](0.26 s)
    countably_infinite_subset_exists......proved - complete   [shostak](0.16 s)
    countably_infinite_strict_subset_exists...proved - complete   [shostak](0.42 s)
    countable_card........................proved - complete   [shostak](1.37 s)
    countably_infinite_union1.............proved - complete   [shostak](0.63 s)
    countably_infinite_union2.............proved - complete   [shostak](0.13 s)
    countable_union.......................proved - complete   [shostak](0.15 s)
    countably_infinite_def................proved - complete   [shostak](0.12 s)
    countable_emptyset....................proved - complete   [shostak](0.12 s)
    countable_singleton...................proved - complete   [shostak](0.13 s)
    card_le_finite........................proved - complete   [shostak](0.09 s)
    card_ge_infinite......................proved - complete   [shostak](0.09 s)
    card_eq_countably_infinite............proved - complete   [shostak](0.50 s)
    card_le_countable.....................proved - complete   [shostak](0.50 s)
    card_ge_uncountable...................proved - complete   [shostak](0.49 s)
    countably_infinite_subset_union.......proved - complete   [shostak](1.94 s)
    countable_finite_subset_union.........proved - complete   [shostak](0.79 s)
    infinite_countable_union..............proved - complete   [shostak](0.23 s)
    infinite_countable_difference.........proved - complete   [shostak](0.10 s)
    Theory totals: 31 formulas, 31 attempted, 31 succeeded (11.34 s)

 Proof summary for theory infinite_nat_def
    infinite_def..........................proved - complete   [shostak](0.38 s)
    infinite_def2.........................proved - complete   [shostak](0.05 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.43 s)

 Proof summary for theory countable_set
    int_to_nat_TCC1.......................proved - complete   [shostak](0.05 s)
    int_to_nat_TCC2.......................proved - complete   [shostak](0.03 s)
    nat_to_int_TCC1.......................proved - complete   [shostak](0.05 s)
    nat_to_int_TCC2.......................proved - complete   [shostak](0.10 s)
    int_to_nat_bijective..................proved - complete   [shostak](0.16 s)
    nat_to_int_bijective..................proved - complete   [shostak](0.18 s)
    countable_family_nat..................proved - incomplete [shostak](0.01 s)
    intset_to_natset_bijective............proved - complete   [shostak](0.38 s)
    countable_family_int..................proved - incomplete [shostak](0.02 s)
    tuple_to_natset_TCC1..................proved - complete   [shostak](0.14 s)
    countable_nat_tuple...................proved - incomplete [shostak](0.11 s)
    tuple_to_intset_TCC1..................proved - complete   [shostak](0.12 s)
    countable_int_tuple...................proved - incomplete [shostak](0.11 s)
    countable_rat.........................proved - incomplete [shostak](0.12 s)
    Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.57 s)

 Proof summary for theory countable_setofsets
    countable_union1......................proved - incomplete [shostak](0.80 s)
    countable_union2......................proved - complete   [shostak](0.74 s)
    countable_intersection................proved - complete   [shostak](1.08 s)
    countable_finite_subsets..............proved - incomplete [shostak](0.18 s)
    countably_infinite_finite_subsets.....proved - incomplete [shostak](0.86 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (3.65 s)

 Proof summary for theory countable_types
    nat_rational..........................proved - incomplete [shostak](0.17 s)
    nat_nonzero_rational..................proved - incomplete [shostak](0.07 s)
    nat_nonneg_rat........................proved - incomplete [shostak](0.29 s)
    nat_nonpos_rat........................proved - incomplete [shostak](0.09 s)
    nat_negrat............................proved - incomplete [shostak](0.08 s)
    nat_posrat............................proved - incomplete [shostak](0.12 s)
    nat_integer...........................proved - complete   [shostak](0.01 s)
    nat_nonzero_integer...................proved - complete   [shostak](0.23 s)
    nat_upfrom............................proved - complete   [shostak](0.08 s)
    nat_above.............................proved - complete   [shostak](0.10 s)
    nat_nonpos_int........................proved - complete   [shostak](0.07 s)
    nat_negint............................proved - complete   [shostak](0.07 s)
    nat_posint............................proved - complete   [shostak](0.07 s)
    nat_even_int..........................proved - complete   [shostak](0.17 s)
    nat_odd_int...........................proved - complete   [shostak](0.21 s)
    Theory totals: 15 formulas, 15 attempted, 15 succeeded (1.82 s)

 Proof summary for theory infinite_card
    finite_card_eq........................proved - complete   [shostak](0.82 s)
    infinite_card_eq......................proved - complete   [shostak](0.01 s)
    infinite_card_le......................proved - complete   [shostak](0.42 s)
    infinite_card_ge......................proved - complete   [shostak](0.41 s)
    finite_card_le........................proved - complete   [shostak](0.41 s)
    finite_card_ge........................proved - complete   [shostak](0.42 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.49 s)

 Proof summary for theory infinite_sets
    infinite_add_card.....................proved - complete   [shostak](0.05 s)
    infinite_remove_card..................proved - complete   [shostak](0.06 s)
    finite_infinite_lt....................proved - complete   [shostak](0.69 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.79 s)

 Proof summary for theory sets_lemmas_extra
    disjoint_commutative..................proved - complete   [shostak](0.01 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.01 s)

 Proof summary for theory indexed_sets_aux
    disjoint_indexed_set_TCC1.............proved - complete   [shostak](0.02 s)
    IComplement_IComplement...............proved - complete   [shostak](0.02 s)
    IDemorgan1............................proved - complete   [shostak](0.07 s)
    IDemorgan2............................proved - complete   [shostak](0.08 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.18 s)

 Proof summary for theory countable_indexed_sets
    Union_IUnion..........................proved - complete   [shostak](0.15 s)
    Intersection_IIntersection............proved - complete   [shostak](0.08 s)
    Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.23 s)

 Proof summary for theory nat_indexed_sets
    IUnion_0_def..........................proved - complete   [shostak](0.03 s)
    IUnion_n_def..........................proved - complete   [shostak](-.70 s)
    increasing_indexed_TCC1...............proved - complete   [shostak](0.04 s)
    increasing_IUnion.....................proved - complete   [shostak](0.17 s)
    decreasing_IIntersection..............proved - complete   [shostak](0.17 s)
    disjoint_IUnion.......................proved - complete   [shostak](0.52 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.23 s)

 Proof summary for theory inverse_image_Union
    inverse_image_Union...................proved - complete   [shostak](0.05 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)

 Proof summary for theory countability_aux
    countable_emptyset....................proved - complete   [shostak](0.02 s)
    countable_singleton...................proved - complete   [shostak](0.03 s)
    countable_add.........................proved - complete   [shostak](0.11 s)
    countable_remove......................proved - complete   [shostak](0.06 s)
    countable_intersection1...............proved - complete   [shostak](0.02 s)
    countable_intersection2...............proved - complete   [shostak](0.02 s)
    countable_difference..................proved - complete   [shostak](0.03 s)
    Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.30 s)

 Proof summary for theory cantor_bernstein_schroeder
    Afun_TCC1.............................proved - complete   [shostak](0.02 s)
    Afun_TCC2.............................proved - complete   [shostak](0.01 s)
    Afundef...............................proved - complete   [shostak](0.03 s)
    Afundef2..............................proved - complete   [shostak](0.01 s)
    Afuncomp..............................proved - complete   [shostak](0.13 s)
    Afuneq_TCC1...........................proved - complete   [shostak](0.05 s)
    Afuneq_TCC2...........................proved - complete   [shostak](0.04 s)
    Afuneq................................proved - complete   [shostak](0.23 s)
    Bfun_TCC1.............................proved - complete   [shostak](0.02 s)
    Bfun_TCC2.............................proved - complete   [shostak](0.02 s)
    Bfun_TCC3.............................proved - complete   [shostak](0.01 s)
    Bfundef...............................proved - complete   [shostak](0.01 s)
    Bfundef2..............................proved - complete   [shostak](0.02 s)
    Bfuneq_TCC1...........................proved - complete   [shostak](0.04 s)
    Bfuneq_TCC2...........................proved - complete   [shostak](0.05 s)
    Bfuneq................................proved - complete   [shostak](0.23 s)
    ABfun.................................proved - complete   [shostak](0.09 s)
    BAfun.................................proved - complete   [shostak](0.08 s)
    ABfuneq_TCC1..........................proved - complete   [shostak](0.04 s)
    ABfuneq_TCC2..........................proved - complete   [shostak](0.05 s)
    ABfuneq...............................proved - complete   [shostak](0.23 s)
    ABrel_Arel_equiv......................proved - complete   [shostak](0.24 s)
    ABrel_Brel_equiv......................proved - complete   [shostak](0.33 s)
    Brel_Arel.............................proved - complete   [shostak](0.14 s)
    Arel_Brel.............................proved - complete   [shostak](0.12 s)
    ABrel_Brel............................proved - complete   [shostak](0.11 s)
    Afununique............................proved - complete   [shostak](0.31 s)
    af_fun_TCC1...........................proved - complete   [shostak](0.03 s)
    ag_fun_TCC1...........................proved - complete   [shostak](0.06 s)
    aginj.................................proved - complete   [shostak](0.28 s)
    Arel_union............................proved - complete   [shostak](0.02 s)
    Arel_disjoint.........................proved - complete   [shostak](0.73 s)
    Brel_disjoint.........................proved - complete   [shostak](0.04 s)
    ABrel_union...........................proved - complete   [shostak](0.02 s)
    ABrel_disjoint........................proved - complete   [shostak](0.07 s)
    Cantor_Bernstein_Schroeder............proved - complete   [shostak](0.62 s)
    Theory totals: 36 formulas, 36 attempted, 36 succeeded (4.57 s)

 Proof summary for theory top_choice_facts
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory relational_choice
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory relation_implication
    rel_impl_extensionality...............proved - complete   [shostak](0.02 s)
    lemma_double_impl.....................proved - complete   [shostak](0.01 s)
    rel_impl_is_partial_order.............proved - complete   [shostak](0.04 s)
    double_impl_is_equivalence............proved - complete   [shostak](0.05 s)
    turnstile_TCC1........................proved - complete   [shostak](0.07 s)
    models_TCC1...........................proved - complete   [shostak](0.12 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.31 s)

 Proof summary for theory relational_choice_properties
    fun_choice_impl_description...........proved - complete   [shostak](0.06 s)
    fun_choice_impl_rel_unique_choice.....proved - complete   [shostak](0.04 s)
    fun_choice_impl_rel_choice............proved - complete   [shostak](0.04 s)
    fun_choice_impl_rel_choice_impl_description_rel_choice...proved - complete   [shostak](0.07 s)
    fun_choice_impl_rel_choice_and_description_rel_choice...proved - complete   [shostak](0.03 s)
    fun_choice_impl_rel_unique_choice_impl_description_rel_choice...proved - complete   [shostak](0.08 s)
    fun_choice_impl_rel_unique_choice_and_description_rel_choice...proved - complete   [shostak](0.03 s)
    description_rel_unique_choice_imp_funct_choice...proved - complete   [shostak](0.05 s)
    description_rel_and_rel_unique_choice_imp_funct_choice...proved - complete   [shostak](0.03 s)
    rel_choice_and_proof_irrel_imp_guarded_rel_choice...proved - complete   [shostak](0.05 s)
    relx_choice_indep_of_premises_imp_guarded_rel_choice...proved - complete   [shostak](0.06 s)
    fun_choice_equiv_rel_unique_param_desc...proved - complete   [shostak](0.03 s)
    Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.58 s)

 Proof summary for theory top_refinement_relations
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory relation_extension
    rel_extension_is_equivalence..........proved - complete   [shostak](0.05 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)

 Proof summary for theory relation_extension_props
    extended_equiv_class_non_empty........proved - complete   [shostak](0.03 s)
    nonempty_equivClass_impl_extended_equiv_class_non_empty...proved - complete   [shostak](0.04 s)
    nonempty_equivClass_iff_extended_equiv_classT_non_empty...proved - complete   [shostak](0.16 s)
    nonempty_equivClass_iff_extended_equiv_classU_non_empty...proved - complete   [shostak](0.16 s)
    proj_tuple_1_equiv_class_representative...proved - complete   [shostak](0.02 s)
    proj_tuple_2_equiv_class_representative...proved - complete   [shostak](0.02 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.44 s)

 Proof summary for theory relation_inverse_image
    equivClass_is_nonempty................proved - complete   [shostak](0.02 s)
    equivClass_equal_is_nonempty..........proved - complete   [shostak](0.01 s)
    inverse_image_of_equivalence..........proved - complete   [shostak](0.03 s)
    preserves_eqv_of_inv_image............proved - complete   [shostak](0.02 s)
    inverse_image_of_equality.............proved - complete   [shostak](0.02 s)
    image_inverse_eq_is_eq_kernel.........proved - complete   [shostak](0.02 s)
    inv_img_surj_impl_codom_eq............proved - complete   [shostak](0.05 s)
    right_inv_inv_finv_image_impl_codom_eq...proved - complete   [shostak](0.06 s)
    surjective_eqv_image_inv_rel_codomain...proved - complete   [shostak](0.03 s)
    right_inv_inv_finv_image_eq_codom_eq...proved - complete   [shostak](0.05 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.32 s)

 Proof summary for theory relation_inverse_extension
    le_U_induces_equivalence..............proved - complete   [shostak](0.03 s)
    le_T_induces_equivalence..............proved - complete   [shostak](0.04 s)
    rel_inv_extension_is_equivalence......proved - complete   [shostak](0.06 s)
    rel_extension_IFF_rel_ext.............proved - complete   [shostak](0.05 s)
    rel_inv_extension2_is_equivalence.....proved - complete   [shostak](0.08 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.27 s)

 Proof summary for theory rr_rel
    g_conistent_with_RR...................proved - complete   [shostak](0.04 s)
    f_conistent_with_RR...................proved - complete   [shostak](0.04 s)
    RR_functional_conditional_equal_RR2...proved - complete   [shostak](0.14 s)
    Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.22 s)

 Proof summary for theory simplest_examples
    Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)

 Proof summary for theory singleton_example
    relations_equality_TCC1...............proved - complete   [shostak](0.03 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.02 s)
    relations_equality....................proved - complete   [shostak](0.06 s)
    relations_equality2...................proved - complete   [shostak](0.08 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.19 s)

 Proof summary for theory finite_nats_trivial
    T1_TCC1...............................proved - complete   [shostak](0.02 s)
    U1_TCC1...............................proved - complete   [shostak](0.01 s)
    g1_TCC1...............................proved - complete   [shostak](0.02 s)
    e1_TCC1...............................proved - complete   [shostak](0.06 s)
    relations_equality_TCC1...............proved - complete   [shostak](0.05 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.14 s)
    relations_equality....................proved - complete   [shostak](0.20 s)
    relations_equality2...................proved - complete   [shostak](0.27 s)
    Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.76 s)

 Proof summary for theory infinite_to_infinite_trivial
    relations_equality_TCC1...............proved - complete   [shostak](0.12 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.04 s)
    relations_equality....................proved - complete   [shostak](0.14 s)
    relations_equality2...................proved - complete   [shostak](0.19 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.48 s)

 Proof summary for theory finite_to_infinite
    relations_equality_TCC1...............proved - complete   [shostak](0.04 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.05 s)
    relations_equality....................proved - complete   [shostak](0.07 s)
    relations_equality2...................proved - complete   [shostak](0.15 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.31 s)

 Proof summary for theory infinite_to_finite_finite_equival_finite_equival_classes
    relations_equality_TCC1...............proved - complete   [shostak](0.06 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.04 s)
    relations_equality....................proved - complete   [shostak](0.15 s)
    relations_equality2...................proved - complete   [shostak](0.25 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.50 s)

 Proof summary for theory infinite_to_finite_infinite_equival_finite_equival_classes
    U8_TCC1...............................proved - complete   [shostak](0.01 s)
    relations_equality_TCC1...............proved - complete   [shostak](0.12 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.10 s)
    relations_equality....................proved - complete   [shostak](0.62 s)
    relations_equality2...................proved - complete   [shostak](0.54 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.39 s)

 Proof summary for theory infinite_to_infinite_infinite_equival_infinite_equival_classes
    e9_TCC1...............................proved - complete   [shostak](0.01 s)
    relations_equality_TCC1...............proved - complete   [shostak](0.05 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.05 s)
    relations_equality....................proved - complete   [shostak](0.07 s)
    relations_equality2...................proved - complete   [shostak](0.13 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.30 s)

 Proof summary for theory infinite_to_infinite_infinite_equival_finite_equival_classes
    relations_equality_TCC1...............proved - complete   [shostak](0.04 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.11 s)
    relations_equality....................proved - complete   [shostak](0.28 s)
    relations_equality2...................proved - complete   [shostak](0.42 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.85 s)

 Proof summary for theory finite_to_infinite_finite_equival_infinite_equival_classes
    T11_TCC1..............................proved - complete   [shostak](0.01 s)
    relations_equality_TCC1...............proved - complete   [shostak](0.10 s)
    relations_equality_TCC2...............proved - complete   [shostak](0.12 s)
    relations_equality....................proved - complete   [shostak](0.54 s)
    relations_equality2...................proved - complete   [shostak](0.77 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.54 s)

Grand Totals: 447 proofs, 447 attempted, 447 succeeded (97.82 s)