products/sources/formale Sprachen/PVS/summaries image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei:   Sprache: Unknown

Columbo aufrufen.summary zum Wurzelverzeichnis wechselnMT940 {MT940[691] Hlasm[1259] Haskell[1587]}Datei anzeigen

*** 
*** top (20:4:31 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
*** 
 Proof summary for theory top
    IMP_sylow_theorems_TCC1...............proved - complete   [shostak](0.02 s)
    Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s)

 Proof summary for theory sylow_theorems
    IMP_finite_groups_TCC1...............proved - complete   [shostak]( 0.01 s)
    p_subgroup_sylow?_TCC1...............proved - complete   [shostak]( 0.15 s)
    p_subgroup_sylow?_TCC2...............proved - complete   [shostak]( 0.10 s)
    subgroup_is_factor_TCC1..............proved - complete   [shostak]( 0.12 s)
    subgroup_is_factor_TCC2..............proved - complete   [shostak]( 0.16 s)
    subgroup_is_factor_TCC3..............proved - complete   [shostak]( 0.11 s)
    subgroup_is_factor_TCC4..............proved - complete   [shostak]( 0.21 s)
    subgroup_is_factor...................proved - complete   [shostak]( 4.80 s)
    First_Sylow_Theorem_TCC1.............proved - complete   [shostak]( 0.10 s)
    First_Sylow_Theorem_TCC2.............proved - complete   [shostak]( 0.16 s)
    First_Sylow_Theorem_TCC3.............proved - complete   [shostak]( 0.11 s)
    First_Sylow_Theorem_TCC4.............proved - complete   [shostak]( 0.17 s)
    First_Sylow_Theorem_TCC5.............proved - complete   [shostak]( 0.11 s)
    First_Sylow_Theorem_TCC6.............proved - complete   [shostak]( 0.12 s)
    First_Sylow_Theorem..................proved - incomplete [shostak](19.46 s)
    p_group_is_subgroup_TCC1.............proved - complete   [shostak]( 0.14 s)
    p_group_is_subgroup_TCC2.............proved - complete   [shostak]( 0.17 s)
    p_group_is_subgroup_TCC3.............proved - complete   [shostak]( 0.11 s)
    p_group_is_subgroup..................proved - incomplete [shostak]( 0.66 s)
    p_subgroup_sylow_order_TCC1..........proved - complete   [shostak]( 0.11 s)
    p_subgroup_sylow_order...............proved - incomplete [shostak]( 2.83 s)
    conjugate_is_p_subgroup_sylow_TCC1...proved - complete   [shostak]( 0.49 s)
    conjugate_is_p_subgroup_sylow........proved - incomplete [shostak]( 0.62 s)
    unique_is_normal.....................proved - incomplete [shostak]( 1.03 s)
    Second_Sylow_Theorem_TCC1............proved - complete   [shostak]( 0.10 s)
    Second_Sylow_Theorem_TCC2............proved - complete   [shostak]( 0.49 s)
    Second_Sylow_Theorem.................proved - incomplete [shostak]( 3.21 s)
    Third_Sylow_Theorem_TCC1.............proved - complete   [shostak]( 0.82 s)
    Third_Sylow_Theorem_TCC2.............proved - complete   [shostak]( 0.50 s)
    Third_Sylow_Theorem..................proved - incomplete [shostak]( 8.46 s)
    Theory totals: 30 formulas, 30 attempted, 30 succeeded (45.63 s)

 Proof summary for theory isomorphism_theorems
    G_TCC1................................proved - complete   [shostak](0.06 s)
    GP_TCC1...............................proved - complete   [shostak](0.06 s)
    quotient_subgroup_TCC1................proved - complete   [shostak](0.09 s)
    quotient_subgroup_TCC2................proved - complete   [shostak](0.25 s)
    quotient_subgroup_TCC3................proved - complete   [shostak](0.10 s)
    quotient_subgroup_TCC4................proved - complete   [shostak](0.24 s)
    quotient_subgroup.....................proved - complete   [shostak](-.49 s)
    second_isomorphism_th_aux_TCC1........proved - complete   [shostak](0.27 s)
    second_isomorphism_th_aux_TCC2........proved - complete   [shostak](0.32 s)
    second_isomorphism_th_aux_TCC3........proved - complete   [shostak](0.29 s)
    second_isomorphism_th_aux_TCC4........proved - complete   [shostak](0.43 s)
    second_isomorphism_th_aux.............proved - complete   [shostak](1.88 s)
    second_isomorphism_th_TCC1............proved - complete   [shostak](0.31 s)
    second_isomorphism_th_TCC2............proved - complete   [shostak](0.35 s)
    second_isomorphism_th_TCC3............proved - complete   [shostak](0.29 s)
    second_isomorphism_th_TCC4............proved - complete   [shostak](0.30 s)
    second_isomorphism_th_TCC5............proved - complete   [shostak](0.35 s)
    second_isomorphism_th_TCC6............proved - complete   [shostak](0.35 s)
    second_isomorphism_th_TCC7............proved - complete   [shostak](0.52 s)
    second_isomorphism_th.................proved - complete   [shostak](2.38 s)
    third_isomorphism_th_aux_TCC1.........proved - complete   [shostak](0.12 s)
    third_isomorphism_th_aux_TCC2.........proved - complete   [shostak](0.15 s)
    third_isomorphism_th_aux_TCC3.........proved - complete   [shostak](0.16 s)
    third_isomorphism_th_aux..............proved - complete   [shostak](1.80 s)
    third_isomorphism_th_TCC1.............proved - complete   [shostak](0.28 s)
    third_isomorphism_th_TCC2.............proved - complete   [shostak](0.14 s)
    third_isomorphism_th_TCC3.............proved - complete   [shostak](1.42 s)
    third_isomorphism_th_TCC4.............proved - complete   [shostak](0.12 s)
    third_isomorphism_th_TCC5.............proved - complete   [shostak](1.21 s)
    third_isomorphism_th_TCC6.............proved - complete   [shostak](0.15 s)
    third_isomorphism_th..................proved - complete   [shostak](2.01 s)
    correspondence_theorem................proved - complete   [shostak](2.38 s)
    Theory totals: 32 formulas, 32 attempted, 32 succeeded (18.29 s)

 Proof summary for theory homomorphism_lemmas
    G_TCC1................................proved - complete   [shostak](0.06 s)
    GP_TCC1...............................proved - complete   [shostak](0.07 s)
    natural_homo_TCC1.....................proved - complete   [shostak](0.09 s)
    natural_homo_TCC2.....................proved - complete   [shostak](0.14 s)
    natural_homo..........................proved - complete   [shostak](0.85 s)
    homo_inv_TCC1.........................proved - complete   [shostak](0.09 s)
    homo_inv..............................proved - complete   [shostak](0.16 s)
    kernel_normal.........................proved - complete   [shostak](0.44 s)
    homo_image............................proved - complete   [shostak](0.49 s)
    homo_image_normal_TCC1................proved - complete   [shostak](0.34 s)
    homo_image_normal.....................proved - complete   [shostak](0.55 s)
    homo_inv_image........................proved - complete   [shostak](0.24 s)
    homo_inv_image_normal_TCC1............proved - complete   [shostak](0.21 s)
    homo_inv_image_normal.................proved - complete   [shostak](0.40 s)
    kernel_in_inv_image...................proved - complete   [shostak](0.44 s)
    homo_inv_image_image..................proved - complete   [shostak](0.73 s)
    homo_inv_image_image_cor..............proved - complete   [shostak](0.71 s)
    first_isomorphism_th_TCC1.............proved - complete   [shostak](0.08 s)
    first_isomorphism_th_TCC2.............proved - complete   [shostak](0.26 s)
    first_isomorphism_th_TCC3.............proved - complete   [shostak](0.09 s)
    first_isomorphism_th_TCC4.............proved - complete   [shostak](0.17 s)
    first_isomorphism_th..................proved - complete   [shostak](2.07 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (8.68 s)

 Proof summary for theory products_subgroups
    IMP_normal_subgroups_TCC1.............proved - complete   [shostak](0.01 s)
    HK_subgroup...........................proved - complete   [shostak](0.37 s)
    HK_subgroup_permute...................proved - complete   [shostak](0.39 s)
    H_K_are_subgroups.....................proved - complete   [shostak](0.18 s)
    Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.95 s)

 Proof summary for theory groups_scaf
    IMP_finite_groups_TCC1................proved - complete   [shostak](0.04 s)
    divby_r...............................proved - complete   [shostak](0.11 s)
    subgroup_transitive...................proved - complete   [shostak](0.10 s)
    normal_subgroup_tran..................proved - complete   [shostak](0.11 s)
    subgroup_intersection.................proved - complete   [shostak](0.24 s)
    conjugate_is_subgroup.................proved - complete   [shostak](0.33 s)
    center_is_normal_TCC1.................proved - complete   [shostak](0.10 s)
    center_is_normal......................proved - complete   [shostak](0.36 s)
    abelian_eq_center.....................proved - complete   [shostak](0.14 s)
    order_gt_1............................proved - complete   [shostak](0.14 s)
    order_gt_p............................proved - complete   [shostak](0.15 s)
    exists_diff_one.......................proved - complete   [shostak](0.21 s)
    one_iff_divides.......................proved - complete   [shostak](0.51 s)
    order_power_TCC1......................proved - complete   [shostak](0.15 s)
    order_power_TCC2......................proved - complete   [shostak](0.15 s)
    order_power...........................proved - complete   [shostak](0.75 s)
    coset_power_nat_TCC1..................proved - complete   [shostak](0.09 s)
    coset_power_nat_TCC2..................proved - complete   [shostak](0.11 s)
    coset_power_nat_TCC3..................proved - complete   [shostak](0.16 s)
    coset_power_nat_TCC4..................proved - complete   [shostak](0.16 s)
    coset_power_nat.......................proved - complete   [shostak](0.44 s)
    coset_power_int.......................proved - complete   [shostak](0.52 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (5.06 s)

 Proof summary for theory general_properties
    seq_power_TCC1........................proved - complete   [shostak](0.05 s)
    only_power_p_TCC1.....................proved - complete   [shostak](0.04 s)
    divides_element.......................proved - complete   [shostak](0.08 s)
    divides_rel_primes_TCC1...............proved - complete   [shostak](0.03 s)
    divides_rel_primes....................proved - complete   [shostak](0.35 s)
    divides_product.......................proved - complete   [shostak](0.22 s)
    product_power_TCC1....................proved - complete   [shostak](0.03 s)
    product_power.........................proved - complete   [shostak](0.48 s)
    product_only_power_TCC1...............proved - complete   [shostak](0.04 s)
    product_only_power....................proved - complete   [shostak](1.18 s)
    divides_power.........................proved - complete   [shostak](0.17 s)
    divides_prime_power_TCC1..............proved - complete   [shostak](0.03 s)
    divides_prime_power_TCC2..............proved - complete   [shostak](0.04 s)
    divides_prime_power...................proved - incomplete [shostak](1.02 s)
    gcd_1_TCC1............................proved - complete   [shostak](0.03 s)
    gcd_1.................................proved - complete   [shostak](0.08 s)
    gcd_1_nd_TCC1.........................proved - complete   [shostak](0.04 s)
    gcd_1_nd..............................proved - complete   [shostak](0.12 s)
    gcd_1_ndp.............................proved - complete   [shostak](0.20 s)
    gcd_1_gcd_1_TCC1......................proved - complete   [shostak](0.04 s)
    gcd_1_gcd_1_TCC2......................proved - complete   [shostak](0.05 s)
    gcd_1_gcd_1...........................proved - complete   [shostak](0.06 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (4.39 s)

 Proof summary for theory right_left_cosets
    IMP_lagrange_TCC1.....................proved - complete   [shostak](0.01 s)
    nonempty_left_coset_TCC1..............proved - complete   [shostak](0.12 s)
    nonempty_left_coset...................proved - complete   [shostak](0.11 s)
    left_coset_finite_TCC1................proved - complete   [shostak](0.12 s)
    left_coset_finite.....................proved - complete   [shostak](0.16 s)
    left_coset_correspondence.............proved - complete   [shostak](0.14 s)
    left_coset_correspondence_inv.........proved - complete   [shostak](0.15 s)
    finite_left_coset_correspondence_TCC1...proved - complete   [shostak](0.08 s)
    finite_left_coset_correspondence_TCC2...proved - complete   [shostak](0.12 s)
    finite_left_coset_correspondence_TCC3...proved - complete   [shostak](0.09 s)
    finite_left_coset_correspondence......proved - incomplete [shostak](0.20 s)
    set_left_cosets_full..................proved - complete   [shostak](0.28 s)
    left_cosets_disjoint..................proved - complete   [shostak](0.24 s)
    left_cosets_partition.................proved - complete   [shostak](0.18 s)
    set_right_cosets_full_1...............proved - complete   [shostak](0.29 s)
    right_left_correspondence.............proved - complete   [shostak](0.83 s)
    finite_right_left_correspondence_TCC1...proved - complete   [shostak](0.12 s)
    finite_right_left_correspondence_TCC2...proved - complete   [shostak](0.12 s)
    finite_right_left_correspondence......proved - incomplete [shostak](0.12 s)
    index_TCC1............................proved - complete   [shostak](0.12 s)
    index_gt1.............................proved - complete   [shostak](0.13 s)
    divide_TCC1...........................proved - complete   [shostak](0.10 s)
    divide_TCC2...........................proved - complete   [shostak](0.14 s)
    divide_TCC3...........................proved - complete   [shostak](0.13 s)
    divide_TCC4...........................proved - complete   [shostak](0.09 s)
    divide_TCC5...........................proved - complete   [shostak](0.46 s)
    card_factor_TCC1......................proved - complete   [shostak](0.20 s)
    card_factor_TCC2......................proved - complete   [shostak](0.08 s)
    card_factor...........................proved - complete   [shostak](0.48 s)
    Theory totals: 29 formulas, 29 attempted, 29 succeeded (5.42 s)

 Proof summary for theory p_groups
    IMP_finite_groups_TCC1................proved - complete   [shostak](0.01 s)
    p_group?_TCC1.........................proved - complete   [shostak](0.14 s)
    alt_is_action_TCC1....................proved - complete   [shostak](0.14 s)
    alt_is_action.........................proved - complete   [shostak](0.13 s)
    Fix_iff_subset........................proved - complete   [shostak](0.24 s)
    Fix_iff_subset_cor_TCC1...............proved - complete   [shostak](0.31 s)
    Fix_iff_subset_cor....................proved - incomplete [shostak](0.77 s)
    subgroup_is_p_group_TCC1..............proved - complete   [shostak](0.10 s)
    subgroup_is_p_group...................proved - complete   [shostak](0.52 s)
    p_group_iff_power_TCC1................proved - complete   [shostak](0.10 s)
    p_group_iff_power.....................proved - incomplete [shostak](0.55 s)
    p_divides_index.......................proved - incomplete [shostak](0.52 s)
    factor_cyclic_TCC1....................proved - complete   [shostak](0.20 s)
    factor_cyclic_TCC2....................proved - complete   [shostak](0.13 s)
    factor_cyclic_TCC3....................proved - complete   [shostak](0.19 s)
    factor_cyclic.........................proved - complete   [shostak](0.71 s)
    normalizer_index_TCC1.................proved - complete   [shostak](0.10 s)
    normalizer_index_TCC2.................proved - complete   [shostak](0.28 s)
    normalizer_index_TCC3.................proved - complete   [shostak](0.27 s)
    normalizer_index......................proved - incomplete [shostak](-.02 s)
    subgroup_proper.......................proved - incomplete [shostak](1.08 s)
    burside_theorem_TCC1..................proved - complete   [shostak](0.28 s)
    burside_theorem.......................proved - incomplete [shostak](2.84 s)
    p_square_is_abelian_TCC1..............proved - complete   [shostak](0.10 s)
    p_square_is_abelian...................proved - incomplete [shostak](4.15 s)
    Theory totals: 25 formulas, 25 attempted, 25 succeeded (13.83 s)

 Proof summary for theory normalizer_centralizer
    IMP_normal_subgroups_TCC1.............proved - complete   [shostak](0.01 s)
    normalizer_TCC1.......................proved - complete   [shostak](0.95 s)
    centralizer_TCC1......................proved - complete   [shostak](0.88 s)
    a_by_c_TCC1...........................proved - complete   [shostak](0.47 s)
    CL_TCC1...............................proved - complete   [shostak](0.89 s)
    normalizer_is_subgroup................proved - complete   [shostak](0.62 s)
    subset_of_normalizer..................proved - complete   [shostak](0.85 s)
    normal_in_normalizer_TCC1.............proved - complete   [shostak](0.45 s)
    normal_in_normalizer..................proved - complete   [shostak](0.49 s)
    centralizer_is_subgroup...............proved - complete   [shostak](0.65 s)
    singleton_iff_center..................proved - complete   [shostak](0.73 s)
    a_by_c_is_action......................proved - complete   [shostak](0.51 s)
    Fix_is_center_TCC1....................proved - complete   [shostak](0.49 s)
    Fix_is_center.........................proved - complete   [shostak](0.54 s)
    stabilizer_is_centralizer.............proved - complete   [shostak](0.50 s)
    orbit_is_CL...........................proved - complete   [shostak](0.48 s)
    orbits_is_CLs.........................proved - complete   [shostak](0.49 s)
    orbits_nFix_is_CLs_nc.................proved - complete   [shostak](1.27 s)
    CLs_eq_index_TCC1.....................proved - complete   [shostak](0.62 s)
    CLs_eq_index_TCC2.....................proved - complete   [shostak](1.05 s)
    CLs_eq_index..........................proved - incomplete [shostak](0.95 s)
    class_equation_2_TCC1.................proved - complete   [shostak](0.65 s)
    class_equation_2_TCC2.................proved - complete   [shostak](1.72 s)
    class_equation_2......................proved - incomplete [shostak](1.14 s)
    Theory totals: 24 formulas, 24 attempted, 24 succeeded (17.42 s)

 Proof summary for theory group_action
    IMP_group_TCC1........................proved - complete   [shostak](0.02 s)
    group_action?_TCC1....................proved - complete   [shostak](0.11 s)
    group_action?_TCC2....................proved - complete   [shostak](0.10 s)
    stabilizer_TCC1.......................proved - complete   [shostak](0.53 s)
    orbit_TCC1............................proved - complete   [shostak](0.55 s)
    Fix_TCC1..............................proved - complete   [shostak](0.54 s)
    stabilizer_is_subgroup................proved - complete   [shostak](0.27 s)
    singleton_iff_Fix.....................proved - complete   [shostak](0.27 s)
    empty_iff_eq_Fix......................proved - complete   [shostak](0.14 s)
    orbits_nFix_disj_Fix..................proved - complete   [shostak](0.27 s)
    orbits_is_union.......................proved - complete   [shostak](0.25 s)
    orbit_nonempty........................proved - complete   [shostak](0.13 s)
    orbits_nonempty.......................proved - complete   [shostak](0.10 s)
    set_orbits_is.........................proved - complete   [shostak](0.16 s)
    orbit_is_finite.......................proved - complete   [shostak](0.10 s)
    orbits_disjoint.......................proved - complete   [shostak](0.44 s)
    orbits_partition......................proved - complete   [shostak](0.15 s)
    orbits_nFix_partition.................proved - complete   [shostak](0.18 s)
    orbits_eq_index_aux_TCC1..............proved - complete   [shostak](0.10 s)
    orbits_eq_index_aux...................proved - complete   [shostak](0.53 s)
    orbits_eq_index_TCC1..................proved - complete   [shostak](0.20 s)
    orbits_eq_index_TCC2..................proved - complete   [shostak](0.19 s)
    orbits_eq_index.......................proved - incomplete [shostak](0.32 s)
    counting_formula_TCC1.................proved - complete   [shostak](0.17 s)
    counting_formula......................proved - incomplete [shostak](0.17 s)
    class_equation_TCC1...................proved - complete   [shostak](0.10 s)
    class_equation_TCC2...................proved - complete   [shostak](0.20 s)
    class_equation........................proved - incomplete [shostak](1.02 s)
    Fix_congruence_TCC1...................proved - complete   [shostak](0.10 s)
    Fix_congruence_TCC2...................proved - complete   [shostak](0.14 s)
    Fix_congruence........................proved - incomplete [shostak](1.53 s)
    Theory totals: 31 formulas, 31 attempted, 31 succeeded (9.10 s)

 Proof summary for theory lagrange_index
    IMP_right_left_cosets_TCC1............proved - complete   [shostak](0.02 s)
    Lagrange_index........................proved - incomplete [shostak](0.68 s)
    index_divides.........................proved - incomplete [shostak](0.09 s)
    order_factor_TCC1.....................proved - complete   [shostak](0.22 s)
    order_factor..........................proved - incomplete [shostak](0.41 s)
    Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.42 s)

 Proof summary for theory class_equation_scaf
    card_rest_aux_TCC1....................proved - complete   [shostak](0.21 s)
    card_rest_aux_TCC2....................proved - complete   [shostak](0.22 s)
    card_rest_aux_TCC3....................proved - complete   [shostak](0.25 s)
    card_rest_aux.........................proved - complete   [shostak](0.42 s)
    card_partition_TCC1...................proved - complete   [shostak](0.21 s)
    card_partition_TCC2...................proved - complete   [shostak](1.59 s)
    card_partition........................proved - incomplete [shostak](3.96 s)
    divide_sigma_TCC1.....................proved - complete   [shostak](0.23 s)
    divide_sigma_TCC2.....................proved - incomplete [shostak](5.37 s)
    divide_sigma..........................proved - incomplete [shostak](4.31 s)
    Theory totals: 10 formulas, 10 attempted, 10 succeeded (16.77 s)

 Proof summary for theory cauchy
    IMP_finite_cyclic_groups_TCC1.........proved - complete   [shostak](0.01 s)
    fseq_product_TCC1.....................proved - complete   [shostak](0.10 s)
    fseq_product_TCC2.....................proved - complete   [shostak](0.22 s)
    S_TCC1................................proved - complete   [shostak](0.10 s)
    fseq_product_in.......................proved - complete   [shostak](1.03 s)
    fseq_product_o........................proved - complete   [shostak](-.48 s)
    fseq_product_one......................proved - complete   [shostak](0.89 s)
    fseq_product_power....................proved - complete   [shostak](0.67 s)
    one_in_SE.............................proved - complete   [shostak](0.14 s)
    order_SE..............................proved - complete   [shostak](0.17 s)
    S_bij_set_seq_TCC1....................proved - complete   [shostak](0.09 s)
    S_bij_set_seq_TCC2....................proved - complete   [shostak](0.18 s)
    S_bij_set_seq.........................proved - complete   [shostak](1.35 s)
    S_is_finite...........................proved - incomplete [shostak](0.40 s)
    S_card_TCC1...........................proved - incomplete [shostak](0.10 s)
    S_card................................proved - incomplete [shostak](0.60 s)
    F_TCC1................................proved - complete   [shostak](0.75 s)
    F_1_TCC1..............................proved - complete   [shostak](0.10 s)
    F_1_TCC2..............................proved - complete   [shostak](0.10 s)
    F_2_TCC1..............................proved - complete   [shostak](0.09 s)
    F_o_F12_TCC1..........................proved - complete   [shostak](0.69 s)
    F_o_F12...............................proved - complete   [shostak](0.55 s)
    fs_o_F21..............................proved - complete   [shostak](0.32 s)
    F_in_S................................proved - complete   [shostak](0.71 s)
    F_is_action_TCC1......................proved - complete   [shostak](0.10 s)
    F_is_action_TCC2......................proved - complete   [shostak](0.10 s)
    F_is_action_TCC3......................proved - complete   [shostak](0.10 s)
    F_is_action_TCC4......................proved - complete   [shostak](0.11 s)
    F_is_action...........................proved - complete   [shostak](0.48 s)
    Fixed_subset_TCC1.....................proved - complete   [shostak](0.13 s)
    Fixed_subset_TCC2.....................proved - complete   [shostak](0.10 s)
    Fixed_subset..........................proved - complete   [shostak](0.76 s)
    cauchy................................proved - incomplete [shostak](1.52 s)
    cauchy_cor_TCC1.......................proved - complete   [shostak](0.11 s)
    cauchy_cor............................proved - incomplete [shostak](0.25 s)
    Theory totals: 35 formulas, 35 attempted, 35 succeeded (12.65 s)

 Proof summary for theory zp_group
    Zn_group_TCC1.........................proved - complete   [shostak](0.01 s)
    Zn_group_TCC2.........................proved - complete   [shostak](0.02 s)
    Zn_group..............................proved - complete   [shostak](0.29 s)
    Zn_finite.............................proved - complete   [shostak](0.02 s)
    Zn_card_TCC1..........................proved - complete   [shostak](0.01 s)
    Zn_card...............................proved - complete   [shostak](0.06 s)
    Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.41 s)

 Proof summary for theory cauchy_scaf
    set_seq_TCC1..........................proved - complete   [shostak](0.03 s)
    emptyset_gives_emptyset...............proved - complete   [shostak](0.02 s)
    emptyset_gives_emptyset1..............proved - complete   [shostak](0.13 s)
    set_seq_singleton.....................proved - complete   [shostak](0.05 s)
    set_seq_empty.........................proved - complete   [shostak](0.03 s)
    add_element_add_set...................proved - complete   [shostak](0.27 s)
    card_add_element_aux..................proved - complete   [shostak](0.12 s)
    card_add_element_TCC1.................proved - incomplete [shostak](0.03 s)
    card_add_element......................proved - incomplete [shostak](0.11 s)
    disjoint_add_set......................proved - complete   [shostak](0.18 s)
    add_set_is_add_ele....................proved - complete   [shostak](0.20 s)
    add_set_is_finite_aux.................proved - complete   [shostak](0.13 s)
    add_set_is_finite.....................proved - incomplete [shostak](0.16 s)
    card_add_set_TCC1.....................proved - incomplete [shostak](0.04 s)
    card_add_set..........................proved - incomplete [shostak](0.38 s)
    set_seq_is_finite.....................proved - incomplete [shostak](0.68 s)
    set_seq_is_add_set_TCC1...............proved - complete   [shostak](0.03 s)
    set_seq_is_add_set_TCC2...............proved - incomplete [shostak](0.03 s)
    set_seq_is_add_set....................proved - incomplete [shostak](0.77 s)
    card_set_seq_TCC1.....................proved - incomplete [shostak](0.02 s)
    card_set_seq_TCC2.....................proved - complete   [shostak](0.05 s)
    card_set_seq..........................proved - incomplete [shostak](0.34 s)
    Theory totals: 22 formulas, 22 attempted, 22 succeeded (3.83 s)

Grand Totals: 320 proofs, 320 attempted, 320 succeeded (163.86 s)

[ Original von:0.130Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.  ]