|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
derivatives_def.pvs
Sprache: PVS
Untersuchungsergebnis.summary Download desMT940 {MT940[670] Hlasm[1084] Haskell[1492]}zum Wurzelverzeichnis wechseln
***
*** top (16:7:44 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 const_fun_def
image_const...........................proved - complete [shostak](0.09 s)
inverse_image_const...................proved - complete [shostak](0.02 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.11 s)
Proof summary for theory function_image_bis
image_emptyset........................proved - complete [shostak](0.01 s)
inverse_image_emptyset................proved - complete [shostak](0.02 s)
surjective_image_inverse_image........proved - complete [shostak](0.03 s)
injective_inverse_image_image.........proved - complete [shostak](0.02 s)
bijective_image_iff_inverse_image.....proved - complete [shostak](0.01 s)
bijective_image_inverse_alt_TCC1......proved - complete [shostak](0.01 s)
bijective_image_inverse_alt...........proved - complete [shostak](0.09 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.19 s)
Proof summary for theory function_inverse_alt_aux
inverse_inverse_alt_TCC1..............proved - complete [shostak](0.00 s)
inverse_inverse_alt_TCC2..............proved - complete [shostak](0.01 s)
inverse_inverse_alt...................proved - complete [shostak](0.06 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.08 s)
Proof summary for theory function_props_aux
inverse_image_composition.............proved - complete [shostak](0.02 s)
composition_inverse_alt_TCC1..........proved - complete [shostak](0.01 s)
composition_inverse_alt_TCC2..........proved - complete [shostak](0.00 s)
composition_inverse_alt_TCC3..........proved - complete [shostak](0.01 s)
composition_inverse_alt...............proved - complete [shostak](0.08 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.13 s)
Proof summary for theory top_array
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory min_array
imin_TCC1.............................proved - complete [shostak](0.12 s)
min_TCC1..............................proved - complete [shostak](0.01 s)
min_lem...............................proved - complete [shostak](0.01 s)
min_in?...............................proved - complete [shostak](0.01 s)
min_def...............................proved - complete [shostak](0.03 s)
min_it_is.............................proved - complete [shostak](0.02 s)
imin_lem..............................proved - complete [shostak](0.03 s)
imin_1................................proved - complete [shostak](0.00 s)
min_2_TCC1............................proved - complete [shostak](0.01 s)
min_2_TCC2............................proved - complete [shostak](0.00 s)
min_2.................................proved - complete [shostak](0.04 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.29 s)
Proof summary for theory min_array_def
ge_total..............................proved - complete [shostak](0.03 s)
IMP_max_array_def_TCC1................proved - complete [shostak](0.00 s)
Imin_TCC1.............................proved - complete [shostak](0.00 s)
Imin_TCC2.............................proved - complete [shostak](0.10 s)
Imin_1_TCC1...........................proved - complete [shostak](0.00 s)
Imin_1................................proved - complete [shostak](0.02 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.15 s)
Proof summary for theory below_arrays
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory max_array_def
imax_rec_TCC1.........................proved - complete [shostak](0.01 s)
imax_rec_TCC2.........................proved - complete [shostak](0.00 s)
imax_rec_lem..........................proved - complete [shostak](0.15 s)
imax_rec_rng..........................proved - complete [shostak](0.08 s)
Imax_rec_TCC1.........................proved - complete [shostak](0.01 s)
Imax_rec_TCC2.........................proved - complete [shostak](0.01 s)
Imax_TCC1.............................proved - complete [shostak](0.00 s)
Imax_TCC2.............................proved - complete [shostak](0.03 s)
Imax_1_TCC1...........................proved - complete [shostak](0.01 s)
Imax_1................................proved - complete [shostak](0.01 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.32 s)
Proof summary for theory max_array
imax_TCC1.............................proved - complete [shostak](0.03 s)
max_TCC1..............................proved - complete [shostak](0.01 s)
max_lem...............................proved - complete [shostak](0.01 s)
max_in?...............................proved - complete [shostak](0.01 s)
imax_lem..............................proved - complete [shostak](0.02 s)
max_def...............................proved - complete [shostak](0.02 s)
max_it_is.............................proved - complete [shostak](0.02 s)
imax_1................................proved - complete [shostak](0.01 s)
max_2_TCC1............................proved - complete [shostak](0.00 s)
max_2_TCC2............................proved - complete [shostak](0.00 s)
max_2.................................proved - complete [shostak](0.04 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.19 s)
Proof summary for theory permutations
perm_reflexive........................proved - complete [shostak](0.03 s)
perm_symmetric........................proved - complete [shostak](0.06 s)
perm_tran.............................proved - complete [shostak](0.07 s)
perm_in?..............................proved - complete [shostak](0.03 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.19 s)
Proof summary for theory sort_array
sort_TCC1.............................proved - complete [shostak](0.06 s)
sort_lem..............................proved - complete [shostak](0.00 s)
sort_in?..............................proved - complete [shostak](0.01 s)
sort_map_TCC1.........................proved - complete [shostak](0.03 s)
sort_map_def..........................proved - complete [shostak](0.00 s)
sort_map_bij..........................proved - complete [shostak](0.00 s)
isort_map_TCC1........................proved - complete [shostak](0.08 s)
isort_map_def.........................proved - complete [shostak](0.00 s)
isort_map_bij.........................proved - complete [shostak](0.00 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.18 s)
Proof summary for theory sort_array_def
swap_TCC1.............................proved - complete [shostak](0.01 s)
swap_TCC2.............................proved - complete [shostak](0.02 s)
asort_TCC1............................proved - complete [shostak](0.01 s)
asort_TCC2............................proved - complete [shostak](0.00 s)
swap_perm.............................proved - complete [shostak](0.24 s)
asort_perm............................proved - complete [shostak](0.06 s)
swap_P_and_Q_TCC1.....................proved - complete [shostak](0.02 s)
swap_P_and_Q..........................proved - complete [shostak](0.33 s)
asort_P_and_Q.........................proved - complete [shostak](0.18 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.88 s)
Proof summary for theory sort_array_lems
sort_min_TCC1.........................proved - complete [shostak](0.00 s)
sort_min..............................proved - complete [shostak](0.07 s)
sort_max_TCC1.........................proved - complete [shostak](0.01 s)
sort_max..............................proved - complete [shostak](0.07 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.14 s)
Proof summary for theory array_ops
caret_fill0_TCC1......................proved - complete [shostak](0.04 s)
caret_fill0_TCC2......................proved - complete [shostak](0.05 s)
caret_fill0...........................proved - complete [shostak](0.17 s)
caret_fill1...........................proved - complete [shostak](0.17 s)
caret_concat_bot_TCC1.................proved - complete [shostak](0.00 s)
caret_concat_bot......................proved - complete [shostak](1.03 s)
caret_concat_top_TCC1.................proved - complete [shostak](0.02 s)
caret_concat_top_TCC2.................proved - complete [shostak](0.05 s)
caret_concat_top_TCC3.................proved - complete [shostak](0.05 s)
caret_concat_top_TCC4.................proved - complete [shostak](0.06 s)
caret_concat_top......................proved - complete [shostak](0.34 s)
caret_concat_all_TCC1.................proved - complete [shostak](0.00 s)
caret_concat_all_TCC2.................proved - complete [shostak](0.01 s)
caret_concat_all_TCC3.................proved - complete [shostak](0.00 s)
caret_concat_all_TCC4.................proved - complete [shostak](0.02 s)
caret_concat_all_TCC5.................proved - complete [shostak](0.01 s)
caret_concat_all_TCC6.................proved - complete [shostak](0.00 s)
caret_concat_all......................proved - complete [shostak](0.12 s)
array_decomp_TCC1.....................proved - complete [shostak](0.00 s)
array_decomp_TCC2.....................proved - complete [shostak](0.00 s)
array_decomp_TCC3.....................proved - complete [shostak](0.01 s)
array_decomp_TCC4.....................proved - complete [shostak](0.01 s)
array_decomp..........................proved - complete [shostak](0.22 s)
caret_bot_all_TCC1....................proved - complete [shostak](0.00 s)
caret_bot_all_TCC2....................proved - complete [shostak](0.00 s)
caret_bot_all.........................proved - complete [shostak](0.18 s)
caret_top_all_TCC1....................proved - complete [shostak](0.04 s)
caret_top_all_TCC2....................proved - complete [shostak](0.05 s)
caret_top_all.........................proved - complete [shostak](0.26 s)
concat_array_bot_TCC1.................proved - complete [shostak](0.01 s)
concat_array_bot......................proved - complete [shostak](0.01 s)
concat_array_top_TCC1.................proved - complete [shostak](0.01 s)
concat_array_top_TCC2.................proved - complete [shostak](0.00 s)
concat_array_top......................proved - complete [shostak](0.06 s)
concat_array_r........................proved - complete [shostak](0.02 s)
concat_array_l........................proved - complete [shostak](0.02 s)
concat_array_assoc....................proved - complete [shostak](0.13 s)
Theory totals: 37 formulas, 37 attempted, 37 succeeded (3.19 s)
Proof summary for theory caret_arrays
caret_TCC1............................proved - complete [shostak](0.02 s)
caret_TCC2............................proved - complete [shostak](0.04 s)
caret_TCC3............................proved - complete [shostak](0.03 s)
caret_TCC4............................proved - complete [shostak](0.06 s)
caret_TCC5............................proved - complete [shostak](0.03 s)
caret_all_TCC1........................proved - complete [shostak](0.01 s)
caret_all_TCC2........................proved - complete [shostak](0.00 s)
caret_all.............................proved - complete [shostak](0.05 s)
caret_ii_0............................proved - complete [shostak](0.04 s)
caret_elim_TCC1.......................proved - complete [shostak](0.06 s)
caret_elim_TCC2.......................proved - complete [shostak](0.06 s)
caret_elim............................proved - complete [shostak](0.09 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.50 s)
Proof summary for theory empty_array_def
empty_array_TCC1......................proved - complete [shostak](0.00 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.00 s)
Proof summary for theory concat_arrays
oh_TCC1...............................proved - complete [shostak](0.04 s)
concat_array_bot0_TCC1................proved - complete [shostak](0.00 s)
concat_array_bot0.....................proved - complete [shostak](0.01 s)
concat_array_top0_TCC1................proved - complete [shostak](0.01 s)
concat_array_top0.....................proved - complete [shostak](0.02 s)
concat_array_bot_TCC1.................proved - complete [shostak](0.02 s)
concat_array_bot......................proved - complete [shostak](0.01 s)
concat_array_top_TCC1.................proved - complete [shostak](0.02 s)
concat_array_top_TCC2.................proved - complete [shostak](0.01 s)
concat_array_top......................proved - complete [shostak](0.00 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.15 s)
Proof summary for theory majority_array
is_majority_TCC1......................proved - incomplete [shostak](0.01 s)
maj_TCC1..............................proved - incomplete [shostak](0.07 s)
is_majority_unique....................proved - incomplete [shostak](0.15 s)
maj_lem...............................proved - incomplete [shostak](0.01 s)
maj_subset............................proved - incomplete [shostak](0.08 s)
maj_in_array..........................proved - incomplete [shostak](0.06 s)
is_majority_const.....................proved - incomplete [shostak](0.04 s)
maj_const.............................proved - incomplete [shostak](0.00 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.43 s)
Proof summary for theory top_seq
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory seqs
seq1_def_TCC1.........................proved - complete [shostak](0.01 s)
seq1_def..............................proved - complete [shostak](0.00 s)
rev_TCC1..............................proved - complete [shostak](0.00 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.01 s)
Proof summary for theory max_seq
Imax_TCC1.............................proved - complete [shostak](0.01 s)
Imax_TCC2.............................proved - complete [shostak](0.01 s)
Imax_TCC3.............................proved - complete [shostak](0.27 s)
Imax_1_TCC1...........................proved - complete [shostak](0.01 s)
Imax_1................................proved - complete [shostak](0.03 s)
imax_TCC1.............................proved - complete [shostak](0.06 s)
max_TCC1..............................proved - complete [shostak](0.03 s)
max_seq_lem...........................proved - complete [shostak](0.02 s)
max_seq_in?...........................proved - complete [shostak](0.02 s)
imax_seq_lem..........................proved - complete [shostak](0.03 s)
max_seq_def...........................proved - complete [shostak](0.02 s)
max_seq_it_is.........................proved - complete [shostak](0.04 s)
imax_seq_1............................proved - complete [shostak](0.01 s)
max_seq_2_TCC1........................proved - complete [shostak](0.01 s)
max_seq_2_TCC2........................proved - complete [shostak](0.01 s)
max_seq_2.............................proved - complete [shostak](0.05 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.65 s)
Proof summary for theory min_seq
Imin_TCC1.............................proved - complete [shostak](0.01 s)
Imin_TCC2.............................proved - complete [shostak](0.04 s)
Imin_TCC3.............................proved - complete [shostak](0.26 s)
Imin_seq_1_TCC1.......................proved - complete [shostak](0.00 s)
Imin_seq_1............................proved - complete [shostak](0.04 s)
imin_TCC1.............................proved - complete [shostak](0.06 s)
min_TCC1..............................proved - complete [shostak](0.03 s)
min_seq_lem...........................proved - complete [shostak](0.02 s)
min_seq_in?...........................proved - complete [shostak](0.02 s)
min_seq_def...........................proved - complete [shostak](0.02 s)
min_seq_it_is.........................proved - complete [shostak](0.04 s)
imin_seq_lem..........................proved - complete [shostak](0.03 s)
imin_seq_1............................proved - complete [shostak](0.02 s)
min_seq_2_TCC1........................proved - complete [shostak](0.01 s)
min_seq_2_TCC2........................proved - complete [shostak](0.01 s)
min_seq_2.............................proved - complete [shostak](0.04 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.68 s)
Proof summary for theory permutations_seq
perm_length...........................proved - incomplete [shostak](0.13 s)
perm_reflexive........................proved - complete [shostak](0.05 s)
perm_symmetric........................proved - incomplete [shostak](0.19 s)
perm_tran.............................proved - complete [shostak](0.08 s)
perm_in?..............................proved - incomplete [shostak](0.03 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.49 s)
Proof summary for theory majority_seq
is_majority_TCC1......................proved - incomplete [shostak](0.01 s)
maj_TCC1..............................proved - incomplete [shostak](0.03 s)
is_majority_unique....................proved - incomplete [shostak](0.14 s)
maj_lem...............................proved - incomplete [shostak](0.02 s)
maj_subset............................proved - incomplete [shostak](0.09 s)
maj_in_seq............................proved - incomplete [shostak](0.08 s)
length_eq_1...........................proved - incomplete [shostak](0.05 s)
is_majority_const.....................proved - incomplete [shostak](0.05 s)
maj_const.............................proved - incomplete [shostak](0.01 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.48 s)
Proof summary for theory bubblesort
epsilon_lem_TCC1......................proved - complete [shostak](0.06 s)
epsilon_lem_TCC2......................proved - complete [shostak](0.13 s)
epsilon_lem...........................proved - complete [shostak](0.36 s)
bubblesort_TCC1.......................proved - complete [shostak](0.04 s)
bubblesort_TCC2.......................proved - complete [shostak](0.14 s)
sorted_bubblesort.....................proved - complete [shostak](0.59 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.33 s)
Proof summary for theory sort_inversions
finite_inversions.....................proved - complete [shostak](0.32 s)
inversions_TCC1.......................proved - complete [shostak](0.00 s)
finite_ap.............................proved - complete [shostak](0.08 s)
ap_TCC1...............................proved - complete [shostak](0.01 s)
card_ap...............................proved - complete [shostak](0.19 s)
inversions_transpose_TCC1.............proved - complete [shostak](0.04 s)
inversions_transpose..................proved - complete [shostak](0.51 s)
card_inversions_transpose.............proved - complete [shostak](0.07 s)
sorted_iff_no_inversions..............proved - complete [shostak](0.03 s)
successive_inversion_lem..............proved - complete [shostak](0.18 s)
successive_inversion_exists...........proved - complete [shostak](0.05 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.48 s)
Proof summary for theory permutation_ops
sorted_iff_id_lem.....................proved - complete [shostak](0.16 s)
sorted_iff_id.........................proved - complete [shostak](0.06 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.22 s)
Proof summary for theory permutation
inverse_id_TCC1.......................proved - complete [shostak](0.00 s)
inverse_id............................proved - complete [shostak](0.03 s)
inverse_composition...................proved - complete [shostak](0.09 s)
transpose_TCC1........................proved - complete [shostak](0.06 s)
involutorian_transpose................proved - complete [shostak](0.02 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.20 s)
Proof summary for theory sort_seq
increasing?_TCC1......................proved - complete [shostak](0.02 s)
sort_TCC1.............................proved - complete [shostak](0.08 s)
sort_length...........................proved - incomplete [shostak](0.01 s)
sort_seq_lem..........................proved - complete [shostak](0.00 s)
sort_seq_in?..........................proved - incomplete [shostak](0.10 s)
sort_seq_in_TCC1......................proved - incomplete [shostak](0.00 s)
sort_seq_in...........................proved - incomplete [shostak](0.02 s)
sort_seq_in2..........................proved - incomplete [shostak](0.03 s)
sort_map_TCC1.........................proved - incomplete [shostak](0.01 s)
sort_map_TCC2.........................proved - incomplete [shostak](0.13 s)
sort_map_def_TCC1.....................proved - incomplete [shostak](0.02 s)
sort_map_def..........................proved - incomplete [shostak](0.02 s)
sort_map_bij..........................proved - incomplete [shostak](0.01 s)
isort_map_TCC1........................proved - incomplete [shostak](0.17 s)
isort_map_def_TCC1....................proved - complete [shostak](0.01 s)
isort_map_def.........................proved - incomplete [shostak](0.02 s)
isort_map_bij.........................proved - incomplete [shostak](0.01 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (0.67 s)
Proof summary for theory sort_seq_lems
sort_seq_min_TCC1.....................proved - incomplete [shostak](0.01 s)
sort_seq_min..........................proved - incomplete [shostak](0.11 s)
sort_seq_max_TCC1.....................proved - incomplete [shostak](0.01 s)
sort_seq_max..........................proved - incomplete [shostak](0.13 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.27 s)
Proof summary for theory set2seq
gen_seq_lem_TCC1......................proved - complete [shostak](0.00 s)
gen_seq_lem...........................proved - complete [shostak](0.01 s)
set2seq_TCC1..........................proved - complete [shostak](0.00 s)
set2seq_TCC2..........................proved - complete [shostak](0.01 s)
set2seq_length........................proved - incomplete [shostak](0.14 s)
set2seq_lem...........................proved - incomplete [shostak](0.16 s)
set2seq_exists........................proved - incomplete [shostak](0.45 s)
set2seq_neq...........................proved - incomplete [shostak](0.22 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.98 s)
Proof summary for theory seq2set
seq2set_TCC1..........................proved - complete [shostak](0.05 s)
seq2set_lem...........................proved - complete [shostak](0.02 s)
card_seq2set..........................proved - complete [shostak](0.10 s)
seq2set_TCC2..........................proved - complete [shostak](0.02 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.19 s)
Proof summary for theory seq_extras
first_TCC1............................proved - complete [shostak](0.01 s)
last_TCC1.............................proved - complete [shostak](0.01 s)
rest_TCC1.............................proved - complete [shostak](0.01 s)
delete_TCC1...........................proved - complete [shostak](0.00 s)
delete_TCC2...........................proved - complete [shostak](0.01 s)
insert?_TCC1..........................proved - complete [shostak](0.04 s)
insert?_TCC2..........................proved - complete [shostak](0.04 s)
add_first_TCC1........................proved - complete [shostak](0.00 s)
add_last_TCC1.........................proved - complete [shostak](0.01 s)
empty_0...............................proved - complete [shostak](0.05 s)
empty_o_seq...........................proved - complete [shostak](0.16 s)
seq_o_empty...........................proved - complete [shostak](0.15 s)
length_rest...........................proved - complete [shostak](0.13 s)
length_delete_TCC1....................proved - complete [shostak](0.02 s)
length_delete.........................proved - complete [shostak](0.02 s)
seq_empty.............................proved - complete [shostak](0.14 s)
seq_first_rest........................proved - complete [shostak](0.32 s)
seq_first_rest_1......................proved - complete [shostak](0.28 s)
add_first_empty_seq...................proved - complete [shostak](0.05 s)
length_rest_0.........................proved - complete [shostak](0.21 s)
rest_add_first........................proved - complete [shostak](0.22 s)
first_add_TCC1........................proved - complete [shostak](0.05 s)
first_add.............................proved - complete [shostak](0.02 s)
nth_add_first_TCC1....................proved - complete [shostak](0.02 s)
nth_add_first_TCC2....................proved - complete [shostak](0.03 s)
nth_add_first_TCC3....................proved - complete [shostak](0.03 s)
nth_add_first.........................proved - complete [shostak](0.03 s)
first_add_last_TCC1...................proved - complete [shostak](0.05 s)
first_add_last........................proved - complete [shostak](0.06 s)
rest_add_last.........................proved - complete [shostak](0.44 s)
add_first_last_commute................proved - complete [shostak](0.25 s)
add_first_last........................proved - complete [shostak](0.39 s)
add_last_delete.......................proved - complete [shostak](0.11 s)
add_last_delete_is_o..................proved - complete [shostak](0.09 s)
nth_add_last_TCC1.....................proved - complete [shostak](0.02 s)
nth_add_last_TCC2.....................proved - complete [shostak](0.03 s)
nth_add_last_TCC3.....................proved - complete [shostak](0.04 s)
nth_add_last..........................proved - complete [shostak](0.03 s)
add_first_compo.......................proved - complete [shostak](0.24 s)
first_compo_TCC1......................proved - complete [shostak](0.07 s)
first_compo...........................proved - complete [shostak](0.06 s)
rest_compo............................proved - complete [shostak](0.02 s)
rest_pos_TCC1.........................proved - complete [shostak](0.11 s)
rest_pos_TCC2.........................proved - complete [shostak](0.08 s)
rest_pos_TCC3.........................proved - complete [shostak](0.09 s)
rest_pos..............................proved - complete [shostak](0.15 s)
delete_is_empty_TCC1..................proved - complete [shostak](0.01 s)
delete_is_empty.......................proved - complete [shostak](0.06 s)
delete_pos_TCC1.......................proved - complete [shostak](0.01 s)
delete_pos_TCC2.......................proved - complete [shostak](0.02 s)
delete_pos............................proved - complete [shostak](0.02 s)
insert_delete_TCC1....................proved - complete [shostak](0.02 s)
insert_delete.........................proved - complete [shostak](0.12 s)
add_first_delete_TCC1.................proved - complete [shostak](0.00 s)
add_first_delete......................proved - complete [shostak](0.75 s)
delete_rest_TCC1......................proved - complete [shostak](0.00 s)
delete_rest_TCC2......................proved - complete [shostak](0.10 s)
delete_rest...........................proved - complete [shostak](0.68 s)
first_equal...........................proved - complete [shostak](0.30 s)
nth_x_TCC1............................proved - complete [shostak](0.02 s)
nth_x.................................proved - complete [shostak](0.03 s)
replace_nth...........................proved - complete [shostak](0.05 s)
replace_n2............................proved - complete [shostak](0.15 s)
delete_equivalent.....................proved - complete [shostak](0.60 s)
equal_prefix..........................proved - complete [shostak](0.29 s)
o_equals_o............................proved - complete [shostak](0.32 s)
o_length_o............................proved - complete [shostak](0.70 s)
add_last_is_o.........................proved - complete [shostak](0.20 s)
add_first_is_o........................proved - complete [shostak](0.12 s)
Theory totals: 69 formulas, 69 attempted, 69 succeeded (9.00 s)
Proof summary for theory seq_pigeon
seq_pigeon_lem........................proved - incomplete [shostak](0.06 s)
seq_pigeon_hole.......................proved - incomplete [shostak](0.02 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.08 s)
Proof summary for theory minmax_set2seq
minmax_set2seq_TCC1...................proved - incomplete [shostak](0.04 s)
minmax_set2seq_TCC2...................proved - complete [shostak](0.02 s)
minmax_set2seq........................proved - incomplete [shostak](0.28 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.34 s)
Proof summary for theory minmax_seq2set
minmax_seq2set_TCC1...................proved - complete [shostak](0.03 s)
minmax_seq2set........................proved - incomplete [shostak](1.06 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.09 s)
Proof summary for theory top_bags
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory bags_aux
choose_TCC1...........................proved - complete [shostak](0.03 s)
rest_TCC1.............................proved - complete [shostak](0.01 s)
choose_gt_zero........................proved - complete [shostak](0.03 s)
insert_choose_rest....................proved - complete [shostak](0.03 s)
filter_emptybag.......................proved - complete [shostak](0.00 s)
filter_insert.........................proved - complete [shostak](0.04 s)
filter_delete.........................proved - complete [shostak](0.04 s)
filter_prop...........................proved - complete [shostak](0.02 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.20 s)
Proof summary for theory bags
delete_TCC1...........................proved - complete [shostak](0.01 s)
emptybag_is_empty?....................proved - complete [shostak](0.01 s)
delete_purge..........................proved - complete [shostak](0.03 s)
insert_unique.........................proved - complete [shostak](0.05 s)
insert_exchange.......................proved - complete [shostak](0.05 s)
delete_insert_TCC1....................proved - complete [shostak](0.02 s)
delete_insert.........................proved - complete [shostak](0.05 s)
insert_delete.........................proved - complete [shostak](0.01 s)
delete_insert_diff....................proved - complete [shostak](0.07 s)
decomposition.........................proved - complete [shostak](0.02 s)
bag_equality..........................proved - complete [shostak](0.00 s)
subbag_empty..........................proved - complete [shostak](0.01 s)
subbag_equality.......................proved - complete [shostak](0.01 s)
subbag_trans..........................proved - complete [shostak](0.02 s)
bag_plus_union........................proved - complete [shostak](0.08 s)
bag_plus_comm.........................proved - complete [shostak](0.01 s)
plus_emptybag.........................proved - complete [shostak](0.01 s)
bag_plus_insert.......................proved - complete [shostak](0.01 s)
bag_distributive......................proved - complete [shostak](0.44 s)
extract_subbag........................proved - complete [shostak](0.01 s)
extract_disj..........................proved - complete [shostak](0.03 s)
bag_disj_comm.........................proved - complete [shostak](0.08 s)
bag_union_comm........................proved - complete [shostak](0.02 s)
bag_union_fix_pt......................proved - complete [shostak](0.02 s)
bag_purge_extract.....................proved - complete [shostak](0.01 s)
bag_disj_extract_perge................proved - complete [shostak](0.02 s)
bag_extract_union_subbag..............proved - complete [shostak](0.06 s)
union_upper_bound.....................proved - complete [shostak](0.03 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (1.20 s)
Proof summary for theory bags_to_sets
insert_bag_lem........................proved - complete [shostak](0.06 s)
purge_bag_lem.........................proved - complete [shostak](0.04 s)
bag_union_lem.........................proved - complete [shostak](0.05 s)
bag_intersection_lem..................proved - complete [shostak](0.06 s)
subbag_lem............................proved - complete [shostak](0.01 s)
bag_to_set_emptybag...................proved - complete [shostak](0.00 s)
empty_bts_bag.........................proved - complete [shostak](0.02 s)
bag_intersection_commutative..........proved - complete [shostak](0.07 s)
bag_union_commutative.................proved - complete [shostak](0.07 s)
bag_plus_lem..........................proved - complete [shostak](0.06 s)
extract_empty_or_singlton_set.........proved - complete [shostak](0.03 s)
extract_singleton.....................proved - complete [shostak](0.05 s)
bag_disj_set..........................proved - complete [shostak](0.05 s)
bag_set_dist_union....................proved - complete [shostak](0.09 s)
bag_non_empty.........................proved - complete [shostak](0.02 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (0.69 s)
Proof summary for theory finite_bags_lems
card_bag_plus.........................proved - incomplete [shostak](0.10 s)
card_bag_union........................proved - incomplete [shostak](0.05 s)
card_bag_disj_union...................proved - incomplete [shostak](0.04 s)
card_subbag_strict....................proved - incomplete [shostak](0.11 s)
card_subbag_strict2...................proved - incomplete [shostak](0.12 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.42 s)
Proof summary for theory finite_bags
bag_to_set_TCC1.......................proved - complete [shostak](0.03 s)
finite_bag............................proved - complete [shostak](0.04 s)
finite_emptybag.......................proved - complete [shostak](0.01 s)
finite_singleton_bag..................proved - complete [shostak](0.02 s)
finite_insert.........................proved - complete [shostak](0.02 s)
finite_purge..........................proved - complete [shostak](0.01 s)
finite_delete.........................proved - complete [shostak](0.06 s)
finite_bag_union......................proved - complete [shostak](0.01 s)
finite_bag_intersection...............proved - complete [shostak](0.01 s)
finite_bag_plus.......................proved - complete [shostak](0.01 s)
finite_update.........................proved - complete [shostak](0.13 s)
finite_set............................proved - complete [shostak](0.01 s)
finite_extract........................proved - complete [shostak](0.02 s)
subtype_TCC1..........................proved - complete [shostak](0.02 s)
singleton_bag_TCC1....................proved - complete [shostak](0.00 s)
union_TCC1............................proved - complete [shostak](0.00 s)
intersection_TCC1.....................proved - complete [shostak](0.01 s)
plus_TCC1.............................proved - complete [shostak](0.00 s)
union_TCC2............................proved - complete [shostak](0.16 s)
plus_TCC2.............................proved - complete [shostak](0.17 s)
union_TCC3............................proved - complete [shostak](0.17 s)
plus_TCC3.............................proved - complete [shostak](0.17 s)
insert_TCC1...........................proved - complete [shostak](0.16 s)
purge_TCC1............................proved - complete [shostak](0.00 s)
delete_TCC1...........................proved - complete [shostak](0.01 s)
emptybag_TCC1.........................proved - complete [shostak](0.00 s)
extract_TCC1..........................proved - complete [shostak](0.00 s)
card_emptybag.........................proved - incomplete [shostak](0.11 s)
card_bag_empty?.......................proved - incomplete [shostak](0.62 s)
card_singleton_bag....................proved - incomplete [shostak](0.10 s)
card_subbag?..........................proved - incomplete [shostak](0.02 s)
card_bag_particular_TCC1..............proved - complete [shostak](-.00 s)
card_bag_particular...................proved - incomplete [shostak](0.44 s)
card_bag_delete.......................proved - incomplete [shostak](0.15 s)
card_bag_insert.......................proved - incomplete [shostak](0.07 s)
card_nonempty_bag?....................proved - incomplete [shostak](0.23 s)
card_disj_intersection................proved - incomplete [shostak](0.00 s)
sum_bag_disj_union....................proved - incomplete [shostak](0.17 s)
card_extract..........................proved - incomplete [shostak](0.01 s)
card_extract_bag......................proved - incomplete [shostak](0.32 s)
card_disjoint_add.....................proved - incomplete [shostak](0.10 s)
card_purge_extract....................proved - incomplete [shostak](0.02 s)
card_union_extract_add................proved - incomplete [shostak](0.06 s)
card_union_extract....................proved - incomplete [shostak](0.02 s)
card_geq_count........................proved - incomplete [shostak](0.01 s)
card_geq_count_add....................proved - incomplete [shostak](0.04 s)
Theory totals: 46 formulas, 46 attempted, 46 succeeded (3.78 s)
Proof summary for theory finite_bags_inductions
cardinal_induction....................proved - incomplete [shostak](0.47 s)
finite_bag_induction..................proved - incomplete [shostak](0.46 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.93 s)
Proof summary for theory finite_bags_aux
finite_bag_rest.......................proved - complete [shostak](0.01 s)
rest_TCC1.............................proved - complete [shostak](0.00 s)
card_bag_rest.........................proved - incomplete [shostak](0.17 s)
finite_filter.........................proved - complete [shostak](0.18 s)
filter_TCC1...........................proved - complete [shostak](0.01 s)
card_filter_insert....................proved - incomplete [shostak](0.04 s)
card_filter_delete....................proved - incomplete [shostak](0.13 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.54 s)
Proof summary for theory fault_masking_vote
mid_val_is_maj........................proved - incomplete [shostak](0.43 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.43 s)
Proof summary for theory majority_vote
maj_size..............................proved - incomplete [shostak](0.13 s)
maj_single_or_empty...................proved - incomplete [shostak](0.17 s)
maj_unique............................proved - incomplete [shostak](0.43 s)
maj_pigeonhole........................proved - incomplete [shostak](0.01 s)
maj_is_extraction.....................proved - incomplete [shostak](0.07 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.80 s)
Proof summary for theory middle_value_select
mid_val_singleton.....................proved - incomplete [shostak](1.62 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (1.62 s)
Proof summary for theory bag_filters
finite_l_filter.......................proved - complete [shostak](0.03 s)
finite_u_filter.......................proved - complete [shostak](0.03 s)
l_filter_TCC1.........................proved - complete [shostak](0.01 s)
u_filter_TCC1.........................proved - complete [shostak](0.00 s)
l_filter_extract......................proved - complete [shostak](0.05 s)
u_filter_extract......................proved - complete [shostak](0.06 s)
l_filter_singleton....................proved - complete [shostak](0.05 s)
u_filter_singleton....................proved - complete [shostak](0.05 s)
l_filter_subbag.......................proved - complete [shostak](0.01 s)
u_filter_subbag.......................proved - complete [shostak](0.02 s)
l_filter_orders.......................proved - complete [shostak](0.02 s)
u_filter_orders.......................proved - complete [shostak](0.03 s)
l_filter_orders_2.....................proved - complete [shostak](0.06 s)
u_filter_orders_2.....................proved - complete [shostak](0.06 s)
l_filter_insert_assoc.................proved - complete [shostak](0.08 s)
u_filter_insert_assoc.................proved - complete [shostak](0.08 s)
l_filter_insert.......................proved - complete [shostak](0.04 s)
u_filter_insert.......................proved - complete [shostak](0.04 s)
l_filter_purge........................proved - complete [shostak](0.05 s)
u_filter_purge........................proved - complete [shostak](0.05 s)
l_u_diff_disj.........................proved - complete [shostak](0.09 s)
l_u_fullset...........................proved - complete [shostak](0.13 s)
l_u_fullset2..........................proved - complete [shostak](0.13 s)
l_u_diff..............................proved - incomplete [shostak](0.53 s)
subset_diff_elements..................proved - complete [shostak](0.20 s)
card_diff_elements....................proved - incomplete [shostak](0.17 s)
card_plus.............................proved - incomplete [shostak](1.53 s)
pigeonhole............................proved - incomplete [shostak](0.26 s)
maj_pigeonhole........................proved - incomplete [shostak](0.08 s)
l_filter_nonempty.....................proved - incomplete [shostak](0.25 s)
u_filter_nonempty.....................proved - incomplete [shostak](0.25 s)
l_filter_max..........................proved - incomplete [shostak](0.75 s)
u_filter_min..........................proved - incomplete [shostak](0.64 s)
l_filter_max_purge....................proved - incomplete [shostak](0.35 s)
u_filter_min_purge....................proved - incomplete [shostak](0.35 s)
filter_exists.........................proved - incomplete [shostak](3.92 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (10.46 s)
Proof summary for theory finite_bags_minmax
max_TCC1..............................proved - complete [shostak](0.15 s)
max_member............................proved - incomplete [shostak](0.02 s)
min_member............................proved - incomplete [shostak](0.02 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.19 s)
Proof summary for theory more_list_props
prefix?_TCC1..........................proved - complete [shostak](0.06 s)
suffix?_TCC1..........................proved - complete [shostak](0.08 s)
caret_TCC1............................proved - complete [shostak](0.01 s)
caret_TCC2............................proved - complete [shostak](0.00 s)
caret_TCC3............................proved - complete [shostak](0.01 s)
caret_TCC4............................proved - complete [shostak](0.02 s)
caret_TCC5............................proved - complete [shostak](0.02 s)
caret_TCC6............................proved - complete [shostak](0.06 s)
prefix_length.........................proved - complete [shostak](0.01 s)
suffix_length.........................proved - complete [shostak](0.00 s)
every_forall..........................proved - complete [shostak](0.01 s)
some_exists...........................proved - complete [shostak](0.19 s)
list_extensionality_TCC1..............proved - complete [shostak](0.01 s)
list_extensionality...................proved - complete [shostak](0.23 s)
list_pigeonhole.......................proved - complete [shostak](0.30 s)
nth_append_TCC1.......................proved - complete [shostak](0.03 s)
nth_append_TCC2.......................proved - complete [shostak](0.04 s)
nth_append............................proved - complete [shostak](0.23 s)
length_null...........................proved - complete [shostak](0.00 s)
length_singleton......................proved - complete [shostak](0.00 s)
length_null_list......................proved - complete [shostak](0.03 s)
reverse_def_TCC1......................proved - complete [shostak](0.01 s)
reverse_def_TCC2......................proved - complete [shostak](0.02 s)
reverse_def...........................proved - complete [shostak](0.50 s)
cons_append...........................proved - complete [shostak](0.09 s)
expand_list_TCC1......................proved - complete [shostak](0.01 s)
expand_list...........................proved - complete [shostak](0.03 s)
append_null_left......................proved - complete [shostak](0.01 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (2.02 s)
Proof summary for theory listn
listn_ext_TCC1........................proved - complete [shostak](0.01 s)
listn_ext_TCC2........................proved - complete [shostak](0.00 s)
listn_ext.............................proved - complete [shostak](0.17 s)
listn_0...............................proved - complete [shostak](0.01 s)
setnth_TCC1...........................proved - complete [shostak](0.00 s)
setnth_TCC2...........................proved - complete [shostak](0.01 s)
setnth_TCC3...........................proved - complete [shostak](0.04 s)
setnth_TCC4...........................proved - complete [shostak](0.09 s)
setnth_TCC5...........................proved - complete [shostak](0.02 s)
setnth_TCC6...........................proved - complete [shostak](0.02 s)
setnth_TCC7...........................proved - complete [shostak](0.13 s)
normalize_fseq_TCC1...................proved - complete [shostak](0.42 s)
normalize_fseq_def....................proved - complete [shostak](0.01 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.94 s)
Proof summary for theory array2list
array2list_it_TCC1....................proved - complete [shostak](0.00 s)
array2list_it_TCC2....................proved - complete [shostak](0.01 s)
array2list_it_TCC3....................proved - complete [shostak](0.01 s)
array2list_it_TCC4....................proved - complete [shostak](0.02 s)
array2list_it_TCC5....................proved - complete [shostak](0.04 s)
array2list_it_TCC6....................proved - complete [shostak](0.00 s)
array2list_it_TCC7....................proved - complete [shostak](0.13 s)
array2list_TCC1.......................proved - complete [shostak](0.00 s)
array2list_TCC2.......................proved - complete [shostak](0.00 s)
array2list_TCC3.......................proved - complete [shostak](0.02 s)
list2array_TCC1.......................proved - complete [shostak](0.01 s)
list2array_TCC2.......................proved - complete [shostak](0.01 s)
list2array_TCC3.......................proved - complete [shostak](0.02 s)
list2array_TCC4.......................proved - complete [shostak](0.01 s)
list2array_sound......................proved - complete [shostak](0.14 s)
default_TCC1..........................proved - complete [shostak](0.01 s)
array2list_inv........................proved - complete [shostak](0.02 s)
list2array_inv_TCC1...................proved - complete [shostak](0.02 s)
list2array_inv........................proved - complete [shostak](0.03 s)
list2array_inv_ext....................proved - complete [shostak](0.04 s)
fill_TCC1.............................proved - complete [shostak](0.01 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (0.56 s)
Proof summary for theory set_as_list
empty_sl_is_empty.....................proved - complete [shostak](0.02 s)
subset_sl?_TCC1.......................proved - complete [shostak](0.01 s)
subset_sl?_TCC2.......................proved - complete [shostak](0.03 s)
subset_sl?_TCC3.......................proved - complete [shostak](0.05 s)
add_sl_TCC1...........................proved - complete [shostak](0.01 s)
add_sl_TCC2...........................proved - complete [shostak](0.03 s)
add_sl_TCC3...........................proved - complete [shostak](0.01 s)
add_sl_TCC4...........................proved - complete [shostak](0.05 s)
remove_sl_TCC1........................proved - complete [shostak](0.01 s)
remove_sl_TCC2........................proved - complete [shostak](0.02 s)
remove_sl_TCC3........................proved - complete [shostak](0.04 s)
remove_sl_TCC4........................proved - complete [shostak](0.04 s)
equal_sl_TCC1.........................proved - complete [shostak](0.88 s)
strict_subset_sl?_TCC1................proved - complete [shostak](0.02 s)
union_sl_TCC1.........................proved - complete [shostak](0.01 s)
union_sl_TCC2.........................proved - complete [shostak](0.02 s)
union_sl_TCC3.........................proved - complete [shostak](0.05 s)
intersection_sl_TCC1..................proved - complete [shostak](0.01 s)
intersection_sl_TCC2..................proved - complete [shostak](0.03 s)
intersection_sl_TCC3..................proved - complete [shostak](0.03 s)
difference_sl_TCC1....................proved - complete [shostak](0.01 s)
difference_sl_TCC2....................proved - complete [shostak](0.02 s)
difference_sl_TCC3....................proved - complete [shostak](0.03 s)
list2set_TCC1.........................proved - complete [shostak](0.01 s)
list2set_TCC2.........................proved - complete [shostak](0.03 s)
card_sl_TCC1..........................proved - complete [shostak](0.01 s)
card_sl_TCC2..........................proved - complete [shostak](0.05 s)
card_sl_TCC3..........................proved - complete [shostak](0.12 s)
reduce_sl_TCC1........................proved - complete [shostak](0.04 s)
reduce_sl_TCC2........................proved - complete [shostak](0.11 s)
reduce_sl_TCC3........................proved - complete [shostak](0.13 s)
equal_sl_card.........................proved - complete [shostak](0.04 s)
Theory totals: 32 formulas, 32 attempted, 32 succeeded (2.01 s)
Proof summary for theory set_as_list_props
strict_subset_card_lt.................proved - complete [shostak](0.19 s)
empty_l2s.............................proved - complete [shostak](0.16 s)
emptyset_l2s..........................proved - complete [shostak](0.03 s)
nonempty_l2s..........................proved - complete [shostak](0.16 s)
subset_l2s............................proved - complete [shostak](0.07 s)
remove_l2s............................proved - complete [shostak](0.04 s)
equal_l2s.............................proved - complete [shostak](0.17 s)
strict_subset_l2s.....................proved - complete [shostak](0.11 s)
union_l2s.............................proved - complete [shostak](0.05 s)
intersection_l2s......................proved - complete [shostak](0.05 s)
disjoint_l2s..........................proved - complete [shostak](0.02 s)
difference_l2s........................proved - complete [shostak](0.09 s)
symmetric_difference_l2s..............proved - complete [shostak](0.06 s)
subset_sl_emptyset_sl.................proved - complete [shostak](0.03 s)
subset_sl_reflexive...................proved - complete [shostak](0.01 s)
subset_sl_transitive..................proved - complete [shostak](0.28 s)
subset_sl_preorder....................proved - complete [shostak](0.02 s)
subset_sl_is_preorder.................proved - complete [shostak](0.01 s)
equal_sl_reflexive....................proved - complete [shostak](0.02 s)
equal_sl_transitive...................proved - complete [shostak](0.03 s)
equal_sl_symmetric....................proved - complete [shostak](0.05 s)
strict_subset_sl_irreflexive..........proved - complete [shostak](0.02 s)
strict_subset_sl_transitive...........proved - complete [shostak](0.08 s)
strict_subset_sl_strict_order.........proved - complete [shostak](0.03 s)
strict_subset_sl_is_strict_order......proved - complete [shostak](0.00 s)
strict_subset_sl_wf...................proved - complete [shostak](0.27 s)
strict_subset_sl_is_wf................proved - complete [shostak](-.00 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (2.08 s)
Proof summary for theory for_iterate
for_def_TCC1..........................proved - complete [shostak](0.04 s)
for_def_TCC2..........................proved - complete [shostak](0.06 s)
for_def_inv...........................proved - complete [shostak](0.09 s)
for_shift.............................proved - complete [shostak](0.13 s)
for_def_ext...........................proved - complete [shostak](0.14 s)
for_def_induction_TCC1................proved - complete [shostak](0.01 s)
for_def_induction_TCC2................proved - complete [shostak](0.00 s)
for_def_induction_TCC3................proved - complete [shostak](0.05 s)
for_def_induction.....................proved - complete [shostak](0.27 s)
ext2int_TCC1..........................proved - complete [shostak](0.01 s)
for_it_TCC1...........................proved - complete [shostak](0.05 s)
for_it_TCC2...........................proved - complete [shostak](0.01 s)
for_it_TCC3...........................proved - complete [shostak](0.00 s)
for_it_TCC4...........................proved - complete [shostak](0.02 s)
for_it_TCC5...........................proved - complete [shostak](0.04 s)
for_it_TCC6...........................proved - complete [shostak](0.06 s)
for_TCC1..............................proved - complete [shostak](0.00 s)
for_eq................................proved - complete [shostak](0.02 s)
for_induction_TCC1....................proved - complete [shostak](0.02 s)
for_induction_TCC2....................proved - complete [shostak](0.02 s)
for_induction_TCC3....................proved - complete [shostak](0.03 s)
for_induction_TCC4....................proved - complete [shostak](0.00 s)
for_induction_TCC5....................proved - complete [shostak](0.02 s)
for_induction.........................proved - complete [shostak](0.07 s)
for_down_def_TCC1.....................proved - complete [shostak](0.04 s)
for_down_def_TCC2.....................proved - complete [shostak](0.05 s)
for_down_def_ext......................proved - complete [shostak](0.11 s)
for_down_up...........................proved - complete [shostak](0.13 s)
for_down_def_induction_TCC1...........proved - complete [shostak](0.00 s)
for_down_def_induction_TCC2...........proved - complete [shostak](0.00 s)
for_down_def_induction_TCC3...........proved - complete [shostak](0.06 s)
for_down_def_induction................proved - complete [shostak](0.05 s)
for_down_TCC1.........................proved - complete [shostak](0.02 s)
for_down_induction_TCC1...............proved - complete [shostak](0.02 s)
for_down_induction_TCC2...............proved - complete [shostak](0.02 s)
for_down_induction_TCC3...............proved - complete [shostak](0.02 s)
for_down_induction_TCC4...............proved - complete [shostak](0.01 s)
for_down_induction_TCC5...............proved - complete [shostak](0.02 s)
for_down_induction....................proved - complete [shostak](0.06 s)
for_down_eq...........................proved - complete [shostak](0.09 s)
iterate_left_def_TCC1.................proved - complete [shostak](0.00 s)
iterate_left_def_TCC2.................proved - complete [shostak](0.01 s)
iterate_left_def_TCC3.................proved - complete [shostak](0.01 s)
iterate_left_def_ext..................proved - complete [shostak](0.15 s)
ext2int_TCC2..........................proved - complete [shostak](0.01 s)
iterate_left_TCC1.....................proved - complete [shostak](0.00 s)
iterate_left_TCC2.....................proved - complete [shostak](0.01 s)
iterate_left_eq.......................proved - complete [shostak](0.25 s)
iterate_left_induction_TCC1...........proved - complete [shostak](0.00 s)
iterate_left_induction_TCC2...........proved - complete [shostak](0.01 s)
iterate_left_induction_TCC3...........proved - complete [shostak](0.00 s)
iterate_left_induction_TCC4...........proved - complete [shostak](0.02 s)
iterate_left_induction_TCC5...........proved - complete [shostak](0.03 s)
iterate_left_induction................proved - complete [shostak](0.13 s)
iterate_right_def_TCC1................proved - complete [shostak](0.03 s)
iterate_right_def_TCC2................proved - complete [shostak](0.03 s)
iterate_right_def_ext.................proved - complete [shostak](0.12 s)
iterate_right_TCC1....................proved - complete [shostak](0.00 s)
iterate_right_TCC2....................proved - complete [shostak](0.01 s)
iterate_right_eq......................proved - complete [shostak](0.25 s)
iterate_right_induction_TCC1..........proved - complete [shostak](0.01 s)
iterate_right_induction_TCC2..........proved - complete [shostak](0.00 s)
iterate_right_induction_TCC3..........proved - complete [shostak](0.01 s)
iterate_right_induction_TCC4..........proved - complete [shostak](0.00 s)
iterate_right_induction...............proved - complete [shostak](0.09 s)
Theory totals: 65 formulas, 65 attempted, 65 succeeded (3.06 s)
Proof summary for theory for_examples
expit_test............................proved - complete [shostak](0.08 s)
expit_sound_TCC1......................proved - complete [shostak](0.00 s)
expit_sound...........................proved - complete [shostak](0.20 s)
factit_test...........................proved - complete [shostak](0.14 s)
factit_sound..........................proved - complete [shostak](0.39 s)
maxit_TCC1............................proved - complete [shostak](0.03 s)
maxit_TCC2............................proved - complete [shostak](0.03 s)
maxit_test............................proved - complete [shostak](0.16 s)
maxit_sound...........................proved - complete [shostak](0.16 s)
minit_test............................proved - complete [shostak](0.16 s)
minit_sound...........................proved - complete [shostak](0.19 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.52 s)
Proof summary for theory big_ops_nat
big_ops_nat_TCC1......................proved - complete [shostak](0.00 s)
big_ops_nat_eq........................proved - complete [shostak](0.06 s)
big_ops_nat_expand_right_TCC1.........proved - complete [shostak](0.01 s)
big_ops_nat_expand_right..............proved - complete [shostak](0.15 s)
big_ops_nat_expand_left...............proved - complete [shostak](0.21 s)
big_ops_nat_split.....................proved - complete [shostak](0.34 s)
big_ops_nat_shift.....................proved - complete [shostak](0.32 s)
big_ops_nat_reverse...................proved - complete [shostak](0.45 s)
big_ops_nat_id........................proved - complete [shostak](0.13 s)
big_ops_nat_comp......................proved - complete [shostak](0.26 s)
big_ops_nat_distrib...................proved - complete [shostak](0.16 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.09 s)
Proof summary for theory arrays
init_TCC1.............................proved - complete [shostak](0.01 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.01 s)
Proof summary for theory arrays_examples
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory runs
invariant_rule........................proved - complete [shostak](0.08 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)
Proof summary for theory fseqs
default_TCC1..........................proved - complete [shostak](0.00 s)
empty_seq_fseq........................proved - complete [shostak](0.01 s)
emptyseq_fseq.........................proved - complete [shostak](0.00 s)
singleton_TCC1........................proved - complete [shostak](0.01 s)
tofseq_TCC1...........................proved - complete [shostak](0.01 s)
singleton_length......................proved - complete [shostak](0.14 s)
fseqs_eq..............................proved - complete [shostak](0.04 s)
fseq_length_zero......................proved - complete [shostak](0.02 s)
oh_TCC1...............................proved - complete [shostak](0.06 s)
oh_TCC2...............................proved - complete [shostak](0.06 s)
concat_length_add.....................proved - complete [shostak](0.01 s)
member_composition....................proved - complete [shostak](0.13 s)
concat_right_emptyseq.................proved - complete [shostak](0.03 s)
concat_left_emptyseq..................proved - complete [shostak](0.03 s)
member_singleton......................proved - complete [shostak](0.02 s)
caret_TCC1............................proved - complete [shostak](0.02 s)
caret_TCC2............................proved - complete [shostak](0.06 s)
caret_TCC3............................proved - complete [shostak](0.07 s)
o_assoc...............................proved - complete [shostak](0.25 s)
fseq1_TCC1............................proved - complete [shostak](0.02 s)
fseq2_TCC1............................proved - complete [shostak](0.01 s)
fseq1_def.............................proved - complete [shostak](0.00 s)
const_seq_TCC1........................proved - complete [shostak](0.02 s)
rev_TCC1..............................proved - complete [shostak](0.02 s)
rev_TCC2..............................proved - complete [shostak](0.01 s)
Theory totals: 25 formulas, 25 attempted, 25 succeeded (1.07 s)
Proof summary for theory fsq
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory fseqs_def
empty_seq_fseq........................proved - complete [shostak](0.00 s)
emptyseq_fseq.........................proved - complete [shostak](0.00 s)
singleton_TCC1........................proved - complete [shostak](0.01 s)
tofseq_TCC1...........................proved - complete [shostak](0.01 s)
singleton_length......................proved - complete [shostak](0.14 s)
fseqs_eq..............................proved - complete [shostak](0.04 s)
fseq_length_zero......................proved - complete [shostak](0.03 s)
oh_TCC1...............................proved - complete [shostak](0.05 s)
oh_TCC2...............................proved - complete [shostak](0.05 s)
concat_length_add.....................proved - complete [shostak](0.01 s)
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.234Quellennavigators
]
|
|
|
|
|
|
