|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
cyclic_monoid.pvs
Sprache: Shell
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[585] Hlasm[1209] Haskell[1601]}Entwicklung
***
*** 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)
[ zur Elbe Produktseite wechseln0.165Quellennavigators
]
|
|
|
|
|
|
