| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: pretyping.mllib Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[585] Hlasm[1209] Haskell[1601]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (17:43:53 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 top_group Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory groupoid fullset_is_groupoid...................proved - complete [shostak](0.03 s) groupoid_TCC1.........................proved - complete [shostak](0.01 s) closed................................proved - complete [shostak](0.03 s) star_closed...........................proved - complete [shostak](0.02 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.08 s) Proof summary for theory groupoid_def commutative_groupoid?_TCC1............proved - complete [shostak](0.01 s) finite_commutative_groupoid?_TCC1.....proved - complete [shostak](0.01 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.02 s) Proof summary for theory commutative_groupoid commutative_groupoid_TCC1.............proved - complete [shostak](0.00 s) commutative...........................proved - complete [shostak](0.02 s) commutative_groupoid_is_groupoid......proved - complete [shostak](0.01 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.03 s) Proof summary for theory monad monad_TCC1............................proved - complete [shostak](0.00 s) one_member............................proved - complete [shostak](0.04 s) one_in................................proved - complete [shostak](0.03 s) left_identity.........................proved - complete [shostak](0.01 s) right_identity........................proved - complete [shostak](0.02 s) unique_left_identity..................proved - complete [shostak](0.02 s) unique_right_identity.................proved - complete [shostak](0.01 s) one_is_monad..........................proved - complete [shostak](0.06 s) trivial_monad_TCC1....................proved - complete [shostak](0.05 s) monad_is_groupoid.....................proved - complete [shostak](0.04 s) sing_one_finite_monad.................proved - complete [shostak](0.05 s) finite_monad_TCC1.....................proved - complete [shostak](0.06 s) commutative_monad_TCC1................proved - complete [shostak](0.07 s) finite_commutative_monad_TCC1.........proved - complete [shostak](0.07 s) order_TCC1............................proved - complete [shostak](0.05 s) order_TCC2............................proved - complete [shostak](0.05 s) order_is_1............................proved - complete [shostak](0.14 s) finite_monad_is_monad.................proved - complete [shostak](0.06 s) commutative_monad_is_monad............proved - complete [shostak](0.06 s) finite_commutative_monad_is_commutative_monad...proved - complete [shostak](0.08 s) finite_commutative_monad_is_finite_monad...proved - complete [shostak](0.08 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (1.01 s) Proof summary for theory monad_def monad?_TCC1...........................proved - complete [shostak](0.00 s) monad?_TCC2...........................proved - complete [shostak](0.01 s) commutative_monad?_TCC1...............proved - complete [shostak](0.01 s) finite_commutative_monad?_TCC1........proved - complete [shostak](0.01 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.03 s) Proof summary for theory semigroup semigroup_TCC1........................proved - complete [shostak](0.00 s) associative...........................proved - complete [shostak](0.03 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.03 s) Proof summary for theory semigroup_def semigroup?_TCC1.......................proved - complete [shostak](0.01 s) finite_commutative_semigroup?_TCC1....proved - complete [shostak](0.01 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.02 s) Proof summary for theory commutative_semigroup IMP_commutative_groupoid_TCC1.........proved - complete [shostak](0.02 s) IMP_semigroup_TCC1....................proved - complete [shostak](0.01 s) commutative_semigroup_TCC1............proved - complete [shostak](0.00 s) commutative_semigroup_is_semigroup....proved - complete [shostak](0.01 s) commutative_semigroup_is_commutative_groupoid...proved - complete [shostak](0.02 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.06 s) Proof summary for theory monoid IMP_monad_TCC1........................proved - complete [shostak](0.01 s) IMP_semigroup_TCC1....................proved - complete [shostak](0.02 s) monoid_TCC1...........................proved - complete [shostak](-.00 s) monoid_is_monad.......................proved - complete [shostak](0.01 s) monoid_is_semigroup...................proved - complete [shostak](0.02 s) power_0...............................proved - complete [shostak](0.01 s) power_1...............................proved - complete [shostak](0.01 s) one_power.............................proved - complete [shostak](0.02 s) power_def.............................proved - complete [shostak](0.05 s) power_mult............................proved - complete [shostak](0.09 s) power_power...........................proved - complete [shostak](0.09 s) power_commutes........................proved - complete [shostak](0.04 s) power_member..........................proved - complete [shostak](0.06 s) one_is_monoid.........................proved - complete [shostak](0.05 s) generated_is_submonoid................proved - complete [shostak](0.10 s) generated_set_card_1..................proved - complete [shostak](0.05 s) finite_monoid_TCC1....................proved - complete [shostak](0.10 s) finite_monoid_is_monoid...............proved - complete [shostak](0.01 s) finite_monoid_is_finite_monad.........proved - complete [shostak](0.09 s) finite_submonoids.....................proved - complete [shostak](0.00 s) commutative_monoid_TCC1...............proved - complete [shostak](0.09 s) commutative_monoid_is_monoid..........proved - complete [shostak](0.01 s) commutative_monoid_is_commutative_monad...proved - complete [shostak](0.03 s) commutative_submonoids................proved - complete [shostak](0.04 s) Theory totals: 24 formulas, 24 attempted, 24 succeeded (0.99 s) Proof summary for theory monoid_def power_TCC1............................proved - complete [shostak](0.01 s) power_TCC2............................proved - complete [shostak](0.00 s) generated_set_lem.....................proved - complete [shostak](0.01 s) monoid?_TCC1..........................proved - complete [shostak](0.02 s) commutative_monoid?_TCC1..............proved - complete [shostak](0.02 s) finite_commutative_monoid?_TCC1.......proved - complete [shostak](0.02 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.07 s) Proof summary for theory cyclic_monoid IMP_monoid_TCC1.......................proved - complete [shostak](0.00 s) cyclic_monoid_TCC1....................proved - complete [shostak](0.01 s) cyclic_monoid_is......................proved - complete [shostak](0.01 s) cyclic_monoid_is_monoid...............proved - complete [shostak](0.01 s) cyclic_monoid_is_commutative_monoid...proved - complete [shostak](0.07 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.10 s) Proof summary for theory cyclic_monoid_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory cyclic_group IMP_group_TCC1........................proved - complete [shostak](0.01 s) generated_by_lem......................proved - complete [shostak](0.02 s) generated_is_subgroup.................proved - complete [shostak](0.03 s) generated_by_is_finite................proved - complete [shostak](0.13 s) cyclic_abelian........................proved - complete [shostak](0.08 s) cyclic_subgroup.......................proved - complete [shostak](0.57 s) is_cyclic.............................proved - complete [shostak](0.09 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.93 s) Proof summary for theory group_def abelian_group?_TCC1...................proved - complete [shostak](0.03 s) finite_abelian_group?_TCC1............proved - complete [shostak](0.02 s) finite_group_surj.....................proved - complete [shostak](0.02 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.06 s) Proof summary for theory group IMP_monoid_TCC1.......................proved - complete [shostak](0.00 s) group_TCC1............................proved - complete [shostak](0.01 s) group_is_monoid.......................proved - complete [shostak](0.01 s) finite_group_TCC1.....................proved - complete [shostak](0.11 s) finite_group_is_group.................proved - complete [shostak](0.10 s) finite_group_is_finite_monoid.........proved - complete [shostak](0.10 s) finite_subgroups......................proved - complete [shostak](0.02 s) one_is_group..........................proved - complete [shostak](0.03 s) one_finite_group......................proved - complete [shostak](0.01 s) one_group_TCC1........................proved - complete [shostak](0.10 s) group_card_gt_0_TCC1..................proved - complete [shostak](0.09 s) group_card_gt_0.......................proved - complete [shostak](0.05 s) inv_exists............................proved - complete [shostak](0.02 s) inv_TCC1..............................proved - complete [shostak](0.04 s) inv_left..............................proved - complete [shostak](0.01 s) inv_right.............................proved - complete [shostak](0.01 s) cancel_right..........................proved - complete [shostak](0.07 s) cancel_left...........................proved - complete [shostak](0.02 s) inv_inv...............................proved - complete [shostak](0.02 s) cancel_right_inv......................proved - complete [shostak](0.02 s) cancel_left_inv.......................proved - complete [shostak](0.05 s) inv_one...............................proved - complete [shostak](0.02 s) inv_star..............................proved - complete [shostak](0.03 s) unique_inv............................proved - complete [shostak](0.02 s) inv_member............................proved - complete [shostak](0.03 s) inv_in................................proved - complete [shostak](0.03 s) divby.................................proved - complete [shostak](0.03 s) product_in............................proved - complete [shostak](0.04 s) one_is_subgroup.......................proved - complete [shostak](0.12 s) group_is_subgroup.....................proved - complete [shostak](0.06 s) subgroup_is_group.....................proved - complete [shostak](0.01 s) subgroup_def..........................proved - complete [shostak](0.15 s) inv_power.............................proved - complete [shostak](0.08 s) power_inv_right.......................proved - complete [shostak](0.01 s) power_inv_left........................proved - complete [shostak](0.01 s) caret_TCC1............................proved - complete [shostak](0.01 s) caret_TCC2............................proved - complete [shostak](0.02 s) expt_0................................proved - complete [shostak](0.01 s) expt_1................................proved - complete [shostak](0.01 s) expt_m1...............................proved - complete [shostak](0.02 s) one_expt..............................proved - complete [shostak](0.02 s) expt_neg..............................proved - complete [shostak](0.03 s) inv_expt..............................proved - complete [shostak](0.03 s) expt_def1.............................proved - complete [shostak](0.11 s) expt_def2.............................proved - complete [shostak](0.07 s) expt_mult.............................proved - complete [shostak](0.23 s) expt_div..............................proved - complete [shostak](0.03 s) expt_expt.............................proved - complete [shostak](0.12 s) expt_commutes.........................proved - complete [shostak](0.04 s) expt_inv_right........................proved - complete [shostak](0.01 s) expt_inv_left.........................proved - complete [shostak](0.02 s) expt_member...........................proved - complete [shostak](0.05 s) generated_by_TCC1.....................proved - complete [shostak](0.13 s) generated_by_lem......................proved - complete [shostak](0.01 s) generated_is_subgroup.................proved - complete [shostak](0.02 s) generated_by_is_finite................proved - complete [shostak](0.11 s) center_TCC1...........................proved - complete [shostak](0.10 s) center_def............................proved - complete [shostak](0.07 s) center_subgroup.......................proved - complete [shostak](0.21 s) one_left..............................proved - complete [shostak](0.00 s) one_right.............................proved - complete [shostak](0.01 s) assoc.................................proved - complete [shostak](0.01 s) Theory totals: 62 formulas, 62 attempted, 62 succeeded (2.98 s) Proof summary for theory abelian_group IMP_group_TCC1........................proved - complete [shostak](0.00 s) abelian_group_TCC1....................proved - complete [shostak](0.03 s) abelian_group_is_group................proved - complete [shostak](0.03 s) abelian_group_is_commutative_monoid...proved - complete [shostak](0.04 s) abelian_subgroups.....................proved - complete [shostak](0.16 s) finite_abelian_group_TCC1.............proved - complete [shostak](0.08 s) finite_abelian_group_is_abelian_group...proved - complete [shostak](0.03 s) finite_abelian_group_is_finite_group...proved - complete [shostak](0.03 s) finite_abelian_subgroups..............proved - complete [shostak](0.05 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.43 s) Proof summary for theory symmetric_groups op_TCC1...............................proved - complete [shostak](0.01 s) Sym_is_group..........................proved - complete [shostak](0.61 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.62 s) Proof summary for theory group_test integer_plus_TCC1.....................proved - complete [shostak](0.10 s) nz_rational_mult_TCC1.................proved - complete [shostak](0.16 s) pos_rational_mult_TCC1................proved - complete [shostak](0.17 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.43 s) Proof summary for theory finite_cyclic_groups IMP_finite_groups_TCC1................proved - complete [shostak](0.00 s) prime_order_cycle.....................proved - complete [shostak](0.14 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.14 s) Proof summary for theory finite_groups IMP_group_TCC1........................proved - complete [shostak](0.00 s) finite_generated_by...................proved - complete [shostak](0.04 s) finite_generated_by_def_TCC1..........proved - complete [shostak](0.03 s) finite_generated_by_def...............proved - complete [shostak](0.82 s) finite_generated_by_one...............proved - complete [shostak](0.51 s) generated_by_card_1_TCC1..............proved - complete [shostak](0.02 s) generated_by_card_1...................proved - complete [shostak](0.08 s) finite_group_elements.................proved - complete [shostak](0.09 s) period_TCC1...........................proved - complete [shostak](0.08 s) a_hat_period_TCC1.....................proved - complete [shostak](0.03 s) a_hat_period..........................proved - complete [shostak](-.69 s) finite_subgroup_def...................proved - complete [shostak](0.17 s) orders_equal..........................proved - complete [shostak](0.05 s) period_is_generated_order_TCC1........proved - complete [shostak](0.43 s) period_is_generated_order.............proved - complete [shostak](0.88 s) period_element_divides_group..........proved - complete [shostak](0.07 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (2.61 s) Proof summary for theory lagrange IMP_group_TCC1........................proved - complete [shostak](0.00 s) right_coset_finite_TCC1...............proved - complete [shostak](0.09 s) right_coset_finite....................proved - complete [shostak](0.25 s) finite_right_coset_correspondence_TCC1...proved - complete [shostak](0.03 s) finite_right_coset_correspondence_TCC2...proved - complete [shostak](0.03 s) finite_right_coset_correspondence_TCC3...proved - complete [shostak](0.03 s) finite_right_coset_correspondence.....proved - complete [shostak](0.15 s) set_right_cosets_full.................proved - complete [shostak](0.20 s) right_cosets_disjoint.................proved - complete [shostak](0.17 s) right_cosets_partition................proved - complete [shostak](0.12 s) Lagrange..............................proved - complete [shostak](0.29 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.36 s) Proof summary for theory cosets IMP_group_TCC1........................proved - complete [shostak](-.00 s) congruence_is_equivalence.............proved - complete [shostak](0.13 s) left_coset_subset.....................proved - complete [shostak](0.05 s) right_coset_subset....................proved - complete [shostak](0.06 s) left_coset_one........................proved - complete [shostak](0.05 s) right_coset_one.......................proved - complete [shostak](0.06 s) left_coset_assoc......................proved - complete [shostak](0.06 s) right_coset_assoc.....................proved - complete [shostak](0.07 s) lr_coset_assoc........................proved - complete [shostak](0.12 s) subset_left_coset.....................proved - complete [shostak](0.03 s) subset_right_coset....................proved - complete [shostak](0.04 s) right_coset_TCC1......................proved - complete [shostak](0.03 s) right_coset_image_TCC1................proved - complete [shostak](0.07 s) right_coset_image.....................proved - complete [shostak](0.04 s) right_coset_is........................proved - complete [shostak](0.15 s) right_coset_def.......................proved - complete [shostak](0.03 s) nonempty_right_coset..................proved - complete [shostak](0.03 s) right_coset_correspondence_TCC1.......proved - complete [shostak](0.07 s) right_coset_correspondence............proved - complete [shostak](0.26 s) left_coset_TCC1.......................proved - complete [shostak](0.03 s) left_coset_image......................proved - complete [shostak](0.04 s) left_coset_def........................proved - complete [shostak](0.02 s) lc_gen_TCC1...........................proved - complete [shostak](0.03 s) lc_gen_def_TCC1.......................proved - complete [shostak](2.08 s) lc_gen_def............................proved - complete [shostak](0.03 s) rc_gen_TCC1...........................proved - complete [shostak](0.04 s) rc_gen_def_TCC1.......................proved - complete [shostak](2.10 s) rc_gen_def............................proved - complete [shostak](0.03 s) lc_eq.................................proved - complete [shostak](0.05 s) lc_is_eq..............................proved - complete [shostak](0.07 s) rc_eq.................................proved - complete [shostak](0.05 s) rc_is_eq..............................proved - complete [shostak](0.08 s) Theory totals: 32 formulas, 32 attempted, 32 succeeded (5.98 s) Proof summary for theory lagrange_scaf partition_TCC1........................proved - complete [shostak](0.04 s) finite_partition_TCC1.................proved - complete [shostak](0.05 s) finite_partition_is_partition.........proved - complete [shostak](0.01 s) card_Union_rest.......................proved - complete [shostak](0.06 s) card_equal_partition_TCC1.............proved - complete [shostak](0.00 s) card_equal_partition_TCC2.............proved - complete [shostak](0.40 s) card_equal_partition_TCC3.............proved - complete [shostak](0.02 s) card_equal_partition..................proved - complete [shostak](0.71 s) card_eq_part_TCC1.....................proved - complete [shostak](0.40 s) card_eq_part_TCC2.....................proved - complete [shostak](0.38 s) card_eq_part_TCC3.....................proved - complete [shostak](0.02 s) card_eq_part_TCC4.....................proved - complete [shostak](0.39 s) card_eq_part..........................proved - complete [shostak](0.06 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (2.52 s) Proof summary for theory infinite_cyclic_groups Z_TCC1................................proved - complete [shostak](0.13 s) F_TCC1................................proved - complete [shostak](0.00 s) Z_gen.................................proved - complete [shostak](0.23 s) inf_cyclic_is_Z.......................proved - complete [shostak](0.23 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.59 s) Proof summary for theory group_rew IMP_group_TCC1........................proved - complete [shostak](0.00 s) inv_left..............................proved - complete [shostak](0.02 s) inv_right.............................proved - complete [shostak](0.03 s) inv_inv...............................proved - complete [shostak](0.02 s) inv_one...............................proved - complete [shostak](0.01 s) inv_in................................proved - complete [shostak](0.03 s) expt_0................................proved - complete [shostak](0.03 s) expt_1................................proved - complete [shostak](0.03 s) expt_m1...............................proved - complete [shostak](0.02 s) one_expt..............................proved - complete [shostak](0.02 s) one_left..............................proved - complete [shostak](0.03 s) one_right.............................proved - complete [shostak](0.02 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.25 s) Proof summary for theory homomorphisms IMP_group_TCC1........................proved - complete [shostak](0.00 s) IMP_group_TCC2........................proved - complete [shostak](0.03 s) homomorphism?_TCC1....................proved - complete [shostak](0.15 s) homo_one_TCC1.........................proved - complete [shostak](0.05 s) homo_one..............................proved - complete [shostak](0.05 s) kernel_TCC1...........................proved - complete [shostak](0.17 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.45 s) Proof summary for theory factor_groups IMP_normal_subgroups_TCC1.............proved - complete [shostak](0.00 s) p0....................................proved - complete [shostak](0.04 s) prep..................................proved - complete [shostak](0.06 s) mult_prep.............................proved - complete [shostak](0.05 s) mult_TCC1.............................proved - complete [shostak](0.05 s) mult_TCC2.............................proved - complete [shostak](0.10 s) mult_lem_TCC1.........................proved - complete [shostak](0.04 s) mult_lem_TCC2.........................proved - complete [shostak](0.05 s) mult_lem..............................proved - complete [shostak](0.27 s) mult_in...............................proved - complete [shostak](0.09 s) mult_is_coset.........................proved - complete [shostak](0.07 s) N_is_identity_TCC1....................proved - complete [shostak](0.07 s) N_is_identity.........................proved - complete [shostak](0.13 s) left_cosets_group_TCC1................proved - complete [shostak](0.10 s) left_cosets_group_TCC2................proved - complete [shostak](0.11 s) left_cosets_group.....................proved - complete [shostak](0.20 s) divide_TCC1...........................proved - complete [shostak](0.05 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (1.49 s) Proof summary for theory normal_subgroups IMP_cosets_TCC1.......................proved - complete [shostak](0.00 s) normal_prep...........................proved - complete [shostak](0.17 s) normal_left_is_right..................proved - complete [shostak](0.12 s) normal_subgroup_is_subgroup...........proved - complete [shostak](0.03 s) nsg_prop..............................proved - complete [shostak](0.06 s) nsg_prop2.............................proved - complete [shostak](0.05 s) lc_gen_normal_TCC1....................proved - complete [shostak](0.08 s) lc_gen_normal_TCC2....................proved - complete [shostak](0.03 s) lc_gen_normal.........................proved - complete [shostak](0.12 s) abelian_normal........................proved - complete [shostak](0.09 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.75 s) Proof summary for theory A_group op_TCC1...............................proved - complete [shostak](0.03 s) A_is_group_TCC1.......................proved - complete [shostak](0.00 s) A_is_group............................proved - complete [shostak](0.62 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.65 s) Proof summary for theory cayleys S_TCC1................................proved - complete [shostak](0.02 s) cayley_prep_TCC1......................proved - complete [shostak](0.00 s) cayley_prep_TCC2......................proved - complete [shostak](0.06 s) cayley_prep...........................proved - complete [shostak](0.06 s) trans_is_group_TCC1...................proved - complete [shostak](0.07 s) trans_is_group_TCC2...................proved - complete [shostak](0.14 s) trans_is_group_TCC3...................proved - complete [shostak](0.07 s) trans_is_group........................proved - complete [shostak](0.54 s) Cayleys_TCC1..........................proved - complete [shostak](0.01 s) Cayleys_TCC2..........................proved - complete [shostak](0.05 s) Cayleys...............................proved - complete [shostak](0.24 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.26 s) Proof summary for theory zn floor_help............................proved - complete [shostak](0.06 s) Z_group...............................proved - complete [shostak](0.11 s) Z_TCC1................................proved - complete [shostak](0.00 s) Z_prep_TCC1...........................proved - complete [shostak](0.01 s) Z_prep_TCC2...........................proved - complete [shostak](0.00 s) Z_prep................................proved - complete [shostak](0.66 s) Z__TCC1...............................proved - complete [shostak](0.00 s) nZ_plus_TCC1..........................proved - complete [shostak](0.10 s) nZ_prep_TCC1..........................proved - complete [shostak](0.04 s) nZ_prep_TCC2..........................proved - complete [shostak](0.04 s) nZ_prep...............................proved - complete [shostak](0.16 s) nZ_TCC1...............................proved - complete [shostak](0.15 s) nZ_TCC2...............................proved - complete [shostak](0.17 s) nZ_normal_TCC1........................proved - complete [shostak](0.37 s) nZ_normal.............................proved - complete [shostak](0.09 s) Z_fact_test_TCC1......................proved - complete [shostak](0.55 s) Z_fact_test_TCC2......................proved - complete [shostak](0.23 s) Z_fact_test...........................proved - complete [shostak](0.13 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (2.88 s) Proof summary for theory subgroups G_TCC1................................proved - complete [shostak](0.00 s) pg64_1................................proved - complete [shostak](0.27 s) center_normal_TCC1....................proved - complete [shostak](0.02 s) center_normal.........................proved - complete [shostak](0.14 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.43 s) Proof summary for theory top_field Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory ring IMP_abelian_group_TCC1................proved - complete [shostak](0.02 s) ring_TCC1.............................proved - complete [shostak](0.02 s) plus_associative......................proved - complete [shostak](0.03 s) plus_commutative......................proved - complete [shostak](0.16 s) times_associative.....................proved - complete [shostak](0.06 s) right_distributive....................proved - complete [shostak](0.05 s) left_distributive.....................proved - complete [shostak](0.05 s) zero_plus.............................proved - complete [shostak](0.02 s) plus_zero.............................proved - complete [shostak](0.02 s) negate_is_left_inv....................proved - complete [shostak](0.02 s) negate_is_right_inv...................proved - complete [shostak](0.02 s) cancel_right_plus.....................proved - complete [shostak](0.02 s) cancel_left_plus......................proved - complete [shostak](0.02 s) negate_negate.........................proved - complete [shostak](0.02 s) cancel_right_minus....................proved - complete [shostak](0.03 s) cancel_left_minus.....................proved - complete [shostak](0.03 s) negate_zero...........................proved - complete [shostak](0.03 s) negate_plus...........................proved - complete [shostak](0.02 s) times_plus............................proved - complete [shostak](0.05 s) idempotent_add_is_zero................proved - complete [shostak](0.03 s) zero_times............................proved - complete [shostak](0.03 s) times_zero............................proved - complete [shostak](0.03 s) negative_times........................proved - complete [shostak](0.05 s) times_negative........................proved - complete [shostak](0.05 s) negative_times_negative...............proved - complete [shostak](0.04 s) ring_is_abelian_group.................proved - complete [shostak](0.05 s) subring_is_ring.......................proved - complete [shostak](0.06 s) sq_rew................................proved - complete [shostak](0.02 s) sq_neg................................proved - complete [shostak](0.03 s) sq_plus...............................proved - complete [shostak](0.07 s) sq_minus..............................proved - complete [shostak](0.04 s) sq_neg_minus..........................proved - complete [shostak](0.04 s) sq_zero...............................proved - complete [shostak](0.02 s) Theory totals: 33 formulas, 33 attempted, 33 succeeded (1.21 s) Proof summary for theory ring_def ring?_TCC1............................proved - complete [shostak](0.01 s) ring?_TCC2............................proved - complete [shostak](0.03 s) commutative_ring?_TCC1................proved - complete [shostak](0.01 s) finite_commutative_ring?_TCC1.........proved - complete [shostak](0.02 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.07 s) Proof summary for theory operator_defs_more Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory commutative_ring IMP_ring_TCC1.........................proved - complete [shostak](0.01 s) commutative_ring_TCC1.................proved - complete [shostak](0.04 s) times_commutative.....................proved - complete [shostak](0.04 s) commutative_ring_is_ring..............proved - complete [shostak](0.05 s) commutative_subrings..................proved - complete [shostak](0.07 s) sq_times..............................proved - complete [shostak](0.05 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.26 s) Proof summary for theory ring_nz_closed IMP_ring_TCC1.........................proved - complete [shostak](0.01 s) ring_nz_closed_TCC1...................proved - complete [shostak](0.03 s) ring_nz_closed_is.....................proved - complete [shostak](0.04 s) ring_nz_closed_is_ring................proved - complete [shostak](0.03 s) nz_T_times_nz_T_is_nz_T...............proved - complete [shostak](0.14 s) negate_nz_T_is_nz_T...................proved - complete [shostak](0.05 s) times_is_zero.........................proved - complete [shostak](0.04 s) nz_T_times............................proved - complete [shostak](0.04 s) times_nz_T............................proved - complete [shostak](0.05 s) nz_T_times_nz_T_is_not_zero...........proved - complete [shostak](0.04 s) sq_nz_is_nz...........................proved - complete [shostak](0.04 s) sq_eq_zero............................proved - complete [shostak](0.05 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.56 s) Proof summary for theory ring_nz_closed_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory ring_with_one IMP_ring_TCC1.........................proved - complete [shostak](0.01 s) IMP_monoid_TCC1.......................proved - complete [shostak](0.03 s) ring_with_one_TCC1....................proved - complete [shostak](0.05 s) one_times.............................proved - complete [shostak](0.04 s) times_one.............................proved - complete [shostak](0.04 s) unique_left_identity..................proved - complete [shostak](0.09 s) unique_right_identity.................proved - complete [shostak](0.09 s) minus_one_times.......................proved - complete [shostak](0.04 s) times_minus_one.......................proved - complete [shostak](0.04 s) minus_one_sq_is_one...................proved - complete [shostak](0.04 s) ring_with_one_is_ring.................proved - complete [shostak](0.03 s) ring_with_one_is_monoid...............proved - complete [shostak](0.04 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.55 s) Proof summary for theory ring_with_one_def commutative_ring_with_one?_TCC1.......proved - complete [shostak](0.03 s) finite_commutative_ring_with_one?_TCC1...proved - complete [shostak](0.03 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.06 s) Proof summary for theory commutative_ring_with_one IMP_ring_with_one_TCC1................proved - complete [shostak](0.01 s) IMP_commutative_ring_TCC1.............proved - complete [shostak](0.06 s) commutative_ring_with_one_TCC1........proved - complete [shostak](0.05 s) commutative_ring_with_one_is..........proved - complete [shostak](0.05 s) commutative_ring_with_one_is_commutative_ring...proved - complete [shostak](0.07 s) commutative_ring_with_one_is_ring_with_one...proved - complete [shostak](0.05 s) commutative_ring_with_one_is_commutative_monoid...proved - complete [shostak](0.07 s Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.35 s) Proof summary for theory integral_domain IMP_commutative_ring_TCC1.............proved - complete [shostak](0.01 s) integral_domain_TCC1..................proved - complete [shostak](0.03 s) integral_domain_is....................proved - complete [shostak](0.04 s) integral_domain_is_ring...............proved - complete [shostak](0.04 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.11 s) Proof summary for theory integral_domain_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory division_ring IMP_ring_with_one_TCC1................proved - complete [shostak](0.00 s) IMP_ring_nz_closed_TCC1...............proved - complete [shostak](0.07 s) IMP_group_TCC1........................proved - complete [shostak](0.18 s) IMP_group_TCC2........................proved - complete [shostak](0.16 s) IMP_group_TCC3........................proved - complete [shostak](0.33 s) IMP_group_TCC4........................proved - complete [shostak](0.17 s) division_ring_TCC1....................proved - complete [shostak](0.08 s) division_ring_is......................proved - complete [shostak](0.08 s) division_ring_is_ring_with_one........proved - complete [shostak](0.08 s) division_ring_is_ring_nz_closed.......proved - complete [shostak](0.15 s) division_ring_is_group................proved - complete [shostak](-.13 s) one_ne_zero...........................proved - complete [shostak](0.22 s) cancel_times_right....................proved - complete [shostak](0.10 s) cancel_times_left.....................proved - complete [shostak](0.10 s) idempotent_times......................proved - complete [shostak](0.09 s) recip_ne_zero.........................proved - complete [shostak](0.11 s) nz_T_div_nz_T_is_nz_T.................proved - complete [shostak](0.11 s) div_simplify..........................proved - complete [shostak](0.09 s) cancel_div_right......................proved - complete [shostak](0.14 s) cancel_div_left.......................proved - complete [shostak](0.18 s) times_div_left........................proved - complete [shostak](0.09 s) div_eq_zero...........................proved - complete [shostak](0.12 s) div_mult..............................proved - complete [shostak](0.09 s) div_mult_left.........................proved - complete [shostak](0.10 s) div_mult_right........................proved - complete [shostak](0.09 s) div_distributes.......................proved - complete [shostak](0.10 s) div_distributes_minus.................proved - complete [shostak](0.11 s) div_div1..............................proved - complete [shostak](0.11 s) div_div2_TCC1.........................proved - complete [shostak](0.09 s) div_div2..............................proved - complete [shostak](0.12 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (3.34 s) Proof summary for theory division_ring_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory field IMP_division_ring_TCC1................proved - complete [shostak](0.01 s) IMP_integral_domain_TCC1..............proved - complete [shostak](0.12 s) field_TCC1............................proved - complete [shostak](0.08 s) nz_star_TCC1..........................proved - complete [shostak](0.10 s) field_is_division_ring................proved - complete [shostak](0.09 s) field_is_integral_domain..............proved - complete [shostak](0.20 s) field_is_abelian_group_TCC1...........proved - complete [shostak](0.08 s) field_is_abelian_group_TCC2...........proved - complete [shostak](0.08 s) field_is_abelian_group................proved - complete [shostak](0.73 s) mult_div_TCC1.........................proved - complete [shostak](0.08 s) mult_div..............................proved - complete [shostak](0.13 s) times_div_right.......................proved - complete [shostak](0.14 s) div_times_TCC1........................proved - complete [shostak](0.08 s) div_times.............................proved - complete [shostak](0.20 s) cross_mult............................proved - complete [shostak](0.19 s) add_div...............................proved - complete [shostak](0.25 s) minus_div1............................proved - complete [shostak](0.13 s) sq_div................................proved - complete [shostak](0.13 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (2.82 s) Proof summary for theory field_def field?_TCC1...........................proved - complete [shostak](0.03 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.03 s) Grand Totals: 452 proofs, 452 attempted, 452 succeeded (38.58 s) [ Dauer der Verarbeitung: 0.176 Sekunden ] |