|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
relation_extension.prf
Sprache: Unknown
rahmenlose Ansicht.summary DruckansichtMT940 {MT940[418] Hlasm[1930] Haskell[2258]}Entwicklung
***
*** top (20:33:35 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 ascending_chains
ascending_chain?_def..................proved - complete [shostak](0.17 s)
least_upperbound_inj..................proved - complete [shostak](0.03 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.21 s)
Proof summary for theory csequence_add
add_finite............................proved - complete [shostak](0.03 s)
add_infinite..........................proved - complete [shostak](0.02 s)
add_length............................proved - complete [shostak](0.04 s)
add_index_TCC1........................proved - complete [shostak](0.03 s)
add_index.............................proved - complete [shostak](0.04 s)
add_nth_TCC1..........................proved - complete [shostak](0.02 s)
add_nth...............................proved - complete [shostak](0.03 s)
add_last_TCC1.........................proved - complete [shostak](0.04 s)
add_last..............................proved - complete [shostak](0.07 s)
add_some..............................proved - complete [shostak](0.03 s)
add_every.............................proved - complete [shostak](0.03 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.37 s)
Proof summary for theory csequence_nth
index?_TCC1...........................proved - complete [shostak](0.04 s)
index?_TCC2...........................proved - complete [shostak](0.03 s)
index?_0..............................proved - complete [shostak](0.02 s)
index?_ub.............................proved - complete [shostak](0.06 s)
index?_lt.............................proved - complete [shostak](0.11 s)
index?_finite.........................proved - complete [shostak](0.13 s)
index?_finite_bound...................proved - complete [shostak](0.06 s)
index?_infinite.......................proved - complete [shostak](0.06 s)
index?_infinite_full..................proved - complete [shostak](0.10 s)
index?_prop...........................proved - complete [shostak](0.04 s)
index?_nonempty.......................proved - complete [shostak](0.04 s)
nth_TCC1..............................proved - complete [shostak](0.06 s)
nth_TCC2..............................proved - complete [shostak](0.06 s)
nth_TCC3..............................proved - complete [shostak](0.03 s)
nth_TCC4..............................proved - complete [shostak](0.03 s)
nth_extensionality_TCC1...............proved - complete [shostak](0.03 s)
nth_extensionality....................proved - complete [shostak](0.17 s)
nth_every.............................proved - complete [shostak](0.19 s)
nth_some..............................proved - complete [shostak](0.19 s)
last_TCC1.............................proved - complete [shostak](0.04 s)
last_rest_TCC1........................proved - complete [shostak](0.03 s)
last_rest.............................proved - complete [shostak](0.11 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.60 s)
Proof summary for theory csequence_length
length_TCC1...........................proved - complete [shostak](0.07 s)
length_TCC2...........................proved - complete [shostak](0.03 s)
length_TCC3...........................proved - complete [shostak](0.04 s)
length_TCC4...........................proved - complete [shostak](0.03 s)
length_TCC5...........................proved - complete [shostak](0.09 s)
length_TCC6...........................proved - complete [shostak](0.06 s)
length_def............................proved - complete [shostak](0.04 s)
length_empty?_rew.....................proved - complete [shostak](0.09 s)
length_nonempty?_rew..................proved - complete [shostak](0.09 s)
length_rest_TCC1......................proved - complete [shostak](0.02 s)
length_rest...........................proved - complete [shostak](0.03 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.59 s)
Proof summary for theory csequence_props
has_length_TCC1.......................proved - complete [shostak](0.03 s)
has_length_TCC2.......................proved - complete [shostak](0.04 s)
has_length_TCC3.......................proved - complete [shostak](0.03 s)
has_length_injective..................proved - complete [shostak](0.08 s)
is_finite_TCC1........................proved - complete [shostak](0.03 s)
is_finite_def.........................proved - complete [shostak](0.11 s)
finite_csequence_TCC1.................proved - complete [shostak](0.03 s)
empty_csequence_is_finite.............proved - complete [shostak](0.01 s)
infinite_csequence_is_nonempty........proved - complete [shostak](0.03 s)
some_every_rew........................proved - complete [shostak](0.06 s)
every_some_rew........................proved - complete [shostak](0.04 s)
some_implies..........................proved - complete [shostak](0.07 s)
every_implies.........................proved - complete [shostak](0.07 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.63 s)
Proof summary for theory csequence_append
append_struct_TCC1....................proved - complete [shostak](0.04 s)
append_TCC1...........................proved - complete [shostak](0.10 s)
append_finite.........................proved - complete [shostak](0.21 s)
append_first_TCC1.....................proved - complete [shostak](0.03 s)
append_first..........................proved - complete [shostak](0.11 s)
append_rest...........................proved - complete [shostak](1.18 s)
append_finite_def.....................proved - complete [shostak](0.22 s)
append_infinite_def...................proved - complete [shostak](0.17 s)
append_length.........................proved - complete [shostak](-.44 s)
append_index..........................proved - complete [shostak](0.56 s)
append_nth_TCC1.......................proved - complete [shostak](0.04 s)
append_nth............................proved - complete [shostak](0.09 s)
append_add............................proved - complete [shostak](0.09 s)
append_last...........................proved - complete [shostak](0.14 s)
append_extensionality.................proved - complete [shostak](0.15 s)
append_some...........................proved - complete [shostak](0.04 s)
append_every..........................proved - complete [shostak](0.05 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (2.77 s)
Proof summary for theory csequence_insert
insert_TCC1...........................proved - complete [shostak](0.03 s)
insert_TCC2...........................proved - complete [shostak](0.04 s)
insert_TCC3...........................proved - complete [shostak](0.02 s)
insert_finite.........................proved - complete [shostak](0.09 s)
insert_infinite.......................proved - complete [shostak](0.06 s)
insert_first..........................proved - complete [shostak](0.03 s)
insert_rest...........................proved - complete [shostak](0.02 s)
insert_length.........................proved - complete [shostak](0.11 s)
insert_index_TCC1.....................proved - complete [shostak](0.04 s)
insert_index..........................proved - complete [shostak](0.09 s)
insert_nth_TCC1.......................proved - complete [shostak](0.10 s)
insert_nth............................proved - complete [shostak](0.25 s)
insert_0..............................proved - complete [shostak](0.03 s)
insert_add............................proved - complete [shostak](0.02 s)
insert_last_TCC1......................proved - complete [shostak](0.05 s)
insert_last...........................proved - complete [shostak](0.43 s)
insert_beyond.........................proved - complete [shostak](0.13 s)
insert_insert_TCC1....................proved - complete [shostak](0.04 s)
insert_insert.........................proved - complete [shostak](0.76 s)
insert_extensionality.................proved - complete [shostak](0.11 s)
insert_some...........................proved - complete [shostak](0.12 s)
insert_every..........................proved - complete [shostak](0.13 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (2.69 s)
Proof summary for theory csequence_concatenate
concatenate_struct_TCC1...............proved - complete [shostak](0.04 s)
concatenate_struct_TCC2...............proved - complete [shostak](0.03 s)
o_finite..............................proved - complete [shostak](0.37 s)
o_finiteness..........................proved - complete [shostak](0.56 s)
o_infinite1...........................proved - complete [shostak](0.03 s)
o_infinite2...........................proved - complete [shostak](0.03 s)
o_empty...............................proved - complete [shostak](0.14 s)
o_nonempty............................proved - complete [shostak](0.06 s)
o_nonempty_left.......................proved - complete [shostak](0.09 s)
o_nonempty_right......................proved - complete [shostak](0.13 s)
o_empty_left..........................proved - complete [shostak](0.22 s)
o_empty_right.........................proved - complete [shostak](0.22 s)
o_first_TCC1..........................proved - complete [shostak](0.03 s)
o_first...............................proved - complete [shostak](0.18 s)
o_rest................................proved - complete [shostak](0.11 s)
o_first_rest..........................proved - complete [shostak](0.17 s)
o_length..............................proved - complete [shostak](0.47 s)
o_index...............................proved - complete [shostak](0.09 s)
o_nth_TCC1............................proved - complete [shostak](0.09 s)
o_nth_TCC2............................proved - complete [shostak](0.07 s)
o_nth.................................proved - complete [shostak](0.52 s)
o_add.................................proved - complete [shostak](0.05 s)
o_last_TCC1...........................proved - complete [shostak](0.09 s)
o_last_TCC2...........................proved - complete [shostak](0.03 s)
o_last................................proved - complete [shostak](0.12 s)
o_infinite............................proved - complete [shostak](0.09 s)
o_assoc...............................proved - complete [shostak](1.13 s)
o_extensionality_left.................proved - complete [shostak](0.12 s)
o_extensionality_right................proved - complete [shostak](0.31 s)
o_some................................proved - complete [shostak](0.33 s)
o_every...............................proved - complete [shostak](0.06 s)
Theory totals: 31 formulas, 31 attempted, 31 succeeded (5.96 s)
Proof summary for theory csequence_concatenate_extract
o_extract.............................proved - complete [shostak](0.47 s)
o_extract_eta.........................proved - complete [shostak](0.08 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.55 s)
Proof summary for theory csequence_extract
caret_TCC1............................proved - complete [shostak](0.04 s)
caret_TCC2............................proved - complete [shostak](0.04 s)
caret_TCC3............................proved - complete [shostak](0.05 s)
caret_TCC4............................proved - complete [shostak](0.05 s)
caret_TCC5............................proved - complete [shostak](0.04 s)
caret_TCC6............................proved - complete [shostak](0.05 s)
caret_TCC7............................proved - complete [shostak](0.05 s)
caret_TCC8............................proved - complete [shostak](0.04 s)
extract_empty.........................proved - complete [shostak](0.25 s)
extract_nonempty......................proved - complete [shostak](0.08 s)
extract_length........................proved - complete [shostak](0.55 s)
extract_def...........................proved - complete [shostak](0.23 s)
extract_rest_TCC1.....................proved - complete [shostak](0.02 s)
extract_rest..........................proved - complete [shostak](0.12 s)
extract_rest2.........................proved - complete [shostak](0.18 s)
extract_extract.......................proved - complete [shostak](1.20 s)
extract_index.........................proved - complete [shostak](0.21 s)
extract_first_TCC1....................proved - complete [shostak](0.08 s)
extract_first.........................proved - complete [shostak](0.12 s)
extract_nth_TCC1......................proved - complete [shostak](0.08 s)
extract_nth...........................proved - complete [shostak](1.82 s)
extract_add_TCC1......................proved - complete [shostak](0.03 s)
extract_add_TCC2......................proved - complete [shostak](0.05 s)
extract_add_TCC3......................proved - complete [shostak](0.05 s)
extract_add...........................proved - complete [shostak](0.06 s)
extract_last_TCC1.....................proved - complete [shostak](0.03 s)
extract_last..........................proved - complete [shostak](-.31 s)
extract_extensionality................proved - complete [shostak](0.20 s)
extract_some..........................proved - complete [shostak](0.17 s)
extract_every.........................proved - complete [shostak](0.17 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (5.73 s)
Proof summary for theory csequence_constant
constant_cseq_TCC1....................proved - complete [shostak](0.04 s)
constant_cseq_TCC2....................proved - complete [shostak](0.02 s)
constant_cseq_TCC3....................proved - complete [shostak](0.03 s)
constant_cseq_empty...................proved - complete [shostak](0.03 s)
constant_cseq_1.......................proved - complete [shostak](0.02 s)
constant_cseq_first_TCC1..............proved - complete [shostak](0.03 s)
constant_cseq_first...................proved - complete [shostak](0.03 s)
constant_cseq_rest_TCC1...............proved - complete [shostak](0.03 s)
constant_cseq_rest....................proved - complete [shostak](0.03 s)
constant_cseq_length..................proved - complete [shostak](0.05 s)
constant_cseq_index...................proved - complete [shostak](0.04 s)
constant_cseq_nth_TCC1................proved - complete [shostak](0.04 s)
constant_cseq_nth.....................proved - complete [shostak](0.07 s)
constant_cseq_add.....................proved - complete [shostak](0.03 s)
constant_cseq_last....................proved - complete [shostak](0.08 s)
constant_cseq_some....................proved - complete [shostak](0.05 s)
constant_cseq_every...................proved - complete [shostak](0.04 s)
constant_cseq_TCC4....................proved - complete [shostak](0.07 s)
constant_cseq_inf_first...............proved - complete [shostak](0.05 s)
constant_cseq_inf_rest................proved - complete [shostak](0.06 s)
constant_cseq_inf_nth_TCC1............proved - complete [shostak](0.03 s)
constant_cseq_inf_nth.................proved - complete [shostak](0.08 s)
constant_cseq_inf_add.................proved - complete [shostak](0.06 s)
constant_cseq_inf_some................proved - complete [shostak](0.09 s)
constant_cseq_inf_every...............proved - complete [shostak](0.04 s)
Theory totals: 25 formulas, 25 attempted, 25 succeeded (1.12 s)
Proof summary for theory csequence_singleton
singleton_is_nonempty_finite..........proved - complete [shostak](0.03 s)
singleton_cseq_length_TCC1............proved - complete [shostak](0.04 s)
singleton_cseq_length.................proved - complete [shostak](0.07 s)
singleton_cseq_index..................proved - complete [shostak](0.04 s)
singleton_cseq_TCC1...................proved - complete [shostak](0.02 s)
singleton_def_TCC1....................proved - complete [shostak](0.03 s)
singleton_def.........................proved - complete [shostak](0.04 s)
singleton_cseq_first..................proved - complete [shostak](0.02 s)
singleton_cseq_rest...................proved - complete [shostak](0.03 s)
singleton_cseq_last...................proved - complete [shostak](0.04 s)
singleton_cseq_some...................proved - complete [shostak](0.02 s)
singleton_cseq_every..................proved - complete [shostak](0.03 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.39 s)
Proof summary for theory csequence_filter
filter_TCC1...........................proved - complete [shostak](0.18 s)
filter_empty..........................proved - complete [shostak](0.09 s)
filter_nonempty.......................proved - complete [shostak](0.13 s)
filter_def............................proved - complete [shostak](0.55 s)
filter_finite.........................proved - complete [shostak](0.03 s)
filter_length.........................proved - complete [shostak](0.03 s)
filter_length_eq......................proved - complete [shostak](0.03 s)
filter_reduce_TCC1....................proved - complete [shostak](0.03 s)
filter_reduce.........................proved - complete [shostak](0.36 s)
filter_add............................proved - complete [shostak](0.42 s)
filter_rest_TCC1......................proved - complete [shostak](0.03 s)
filter_rest...........................proved - complete [shostak](0.06 s)
filter_suffix_TCC1....................proved - complete [shostak](0.22 s)
filter_suffix_TCC2....................proved - complete [shostak](0.02 s)
filter_suffix.........................proved - complete [shostak](0.14 s)
filter_first_TCC1.....................proved - complete [shostak](0.03 s)
filter_first..........................proved - complete [shostak](0.11 s)
filter_first_first_TCC1...............proved - complete [shostak](0.03 s)
filter_first_first....................proved - complete [shostak](0.08 s)
filter_full...........................proved - complete [shostak](1.00 s)
filter_idem...........................proved - complete [shostak](0.07 s)
filter_some...........................proved - complete [shostak](0.69 s)
filter_every..........................proved - complete [shostak](0.08 s)
filter_filter_of......................proved - complete [shostak](0.37 s)
filter_concatenate....................proved - complete [shostak](0.09 s)
filter_filter.........................proved - complete [shostak](0.11 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (4.97 s)
Proof summary for theory csequence_filter_of
filter_of?_TCC1.......................proved - complete [shostak](0.06 s)
filter_of?_empty......................proved - complete [shostak](0.04 s)
filter_of?_nonempty...................proved - complete [shostak](0.03 s)
filter_of?_finite.....................proved - complete [shostak](0.09 s)
filter_of?_def........................proved - complete [shostak](0.18 s)
filter_of?_first_p_TCC1...............proved - complete [shostak](0.03 s)
filter_of?_first_p....................proved - complete [shostak](0.21 s)
filter_of?_suffix.....................proved - complete [shostak](0.33 s)
filter_of?_injective..................proved - complete [shostak](0.17 s)
filter_of?_concatenate................proved - complete [shostak](1.05 s)
filter_of?_implication................proved - complete [shostak](0.11 s)
filter_of?_implication_rev............proved - complete [shostak](0.13 s)
filter_of?_some.......................proved - complete [shostak](0.10 s)
filter_of?_filter_of?.................proved - complete [shostak](0.25 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (2.78 s)
Proof summary for theory csequence_first_p
p_indexes_nonempty....................proved - complete [shostak](0.04 s)
first_p_TCC1..........................proved - complete [shostak](0.02 s)
first_p_nth...........................proved - complete [shostak](0.03 s)
first_p_rest_TCC1.....................proved - complete [shostak](0.03 s)
first_p_rest_TCC2.....................proved - complete [shostak](0.04 s)
first_p_rest..........................proved - complete [shostak](0.49 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.64 s)
Proof summary for theory csequence_suffix
suffix?_empty.........................proved - complete [shostak](0.13 s)
suffix?_rest_left.....................proved - complete [shostak](0.05 s)
suffix?_rest_right....................proved - complete [shostak](0.03 s)
suffix?_finite_left...................proved - complete [shostak](0.06 s)
suffix?_finite_right..................proved - complete [shostak](0.06 s)
suffix?_infinite_left.................proved - complete [shostak](0.03 s)
suffix?_infinite_right................proved - complete [shostak](0.03 s)
suffix?_length........................proved - complete [shostak](0.13 s)
suffix?_length_eq.....................proved - complete [shostak](0.12 s)
suffix?_index.........................proved - complete [shostak](0.08 s)
suffix?_concatenate...................proved - complete [shostak](0.11 s)
suffix?_def...........................proved - complete [shostak](0.07 s)
suffix?_is_preorder...................proved - complete [shostak](0.11 s)
suffix?_finite_antisymmetric..........proved - complete [shostak](0.15 s)
suffix?_order.........................proved - complete [shostak](0.07 s)
suffix_TCC1...........................proved - complete [shostak](0.03 s)
suffix_TCC2...........................proved - complete [shostak](0.03 s)
suffix_TCC3...........................proved - complete [shostak](0.04 s)
suffix_TCC4...........................proved - complete [shostak](0.03 s)
suffix_TCC5...........................proved - complete [shostak](0.03 s)
suffix_is_finite......................proved - complete [shostak](0.04 s)
suffix_is_infinite....................proved - complete [shostak](0.06 s)
suffix_0..............................proved - complete [shostak](0.02 s)
suffix_1..............................proved - complete [shostak](0.03 s)
suffix_rest1..........................proved - complete [shostak](0.03 s)
suffix_rest2_TCC1.....................proved - complete [shostak](0.09 s)
suffix_rest2..........................proved - complete [shostak](0.22 s)
suffix_suffix.........................proved - complete [shostak](0.16 s)
suffix_length.........................proved - complete [shostak](0.12 s)
suffix_first_TCC1.....................proved - complete [shostak](0.03 s)
suffix_first..........................proved - complete [shostak](-.52 s)
suffix_index..........................proved - complete [shostak](0.14 s)
suffix_nth_TCC1.......................proved - complete [shostak](0.07 s)
suffix_nth............................proved - complete [shostak](0.26 s)
suffix_empty..........................proved - complete [shostak](0.09 s)
suffix_nonempty.......................proved - complete [shostak](0.03 s)
suffix_concatenate_TCC1...............proved - complete [shostak](0.03 s)
suffix_concatenate_TCC2...............proved - complete [shostak](0.04 s)
suffix_concatenate....................proved - complete [shostak](0.75 s)
suffix?_suffix........................proved - complete [shostak](0.06 s)
suffix_some...........................proved - complete [shostak](0.11 s)
suffix_every..........................proved - complete [shostak](0.12 s)
Theory totals: 42 formulas, 42 attempted, 42 succeeded (3.33 s)
Proof summary for theory csequence_subsequence
subsequence?_TCC1.....................proved - complete [shostak](0.04 s)
subsequence?_empty_left...............proved - complete [shostak](0.02 s)
subsequence?_empty_right..............proved - complete [shostak](0.04 s)
subsequence?_rest1....................proved - complete [shostak](0.23 s)
subsequence?_rest2....................proved - complete [shostak](0.11 s)
subsequence?_extensionality...........proved - complete [shostak](0.04 s)
subsequence?_finite...................proved - complete [shostak](0.15 s)
subsequence?_nth......................proved - complete [shostak](0.34 s)
subsequence?_concatenate_left.........proved - complete [shostak](0.25 s)
subsequence?_concatenate_right........proved - complete [shostak](0.48 s)
subsequence?_prefix...................proved - complete [shostak](0.21 s)
subsequence?_suffix...................proved - complete [shostak](0.21 s)
subsequence?_length...................proved - complete [shostak](0.46 s)
subsequence?_length_eq................proved - complete [shostak](0.48 s)
subsequence?_is_preorder..............proved - complete [shostak](0.12 s)
subsequence?_finite_antisymmetric.....proved - complete [shostak](0.16 s)
prefix?_is_subsequence?...............proved - complete [shostak](0.06 s)
suffix?_is_subsequence?...............proved - complete [shostak](0.04 s)
subsequence?_some.....................proved - complete [shostak](0.13 s)
subsequence?_every....................proved - complete [shostak](0.04 s)
subsequence_func_TCC1.................proved - complete [shostak](0.04 s)
subsequence_func_TCC2.................proved - complete [shostak](0.14 s)
subsequence_func_TCC3.................proved - complete [shostak](0.12 s)
subsequence_func_TCC4.................proved - complete [shostak](0.05 s)
subsequence_func_TCC5.................proved - complete [shostak](0.26 s)
subsequence_func_TCC6.................proved - complete [shostak](0.14 s)
subsequence_func_TCC7.................proved - complete [shostak](0.15 s)
subsequence_func_monotonic............proved - complete [shostak](0.58 s)
subsequence_func_nth..................proved - complete [shostak](0.77 s)
subsequence?_def......................proved - complete [shostak](0.33 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (6.18 s)
Proof summary for theory csequence_prefix
prefix?_TCC1..........................proved - complete [shostak](0.04 s)
prefix?_finite........................proved - complete [shostak](0.06 s)
prefix?_infinite......................proved - complete [shostak](0.07 s)
prefix?_empty.........................proved - complete [shostak](0.02 s)
prefix?_empty_is_prefix...............proved - complete [shostak](0.02 s)
prefix?_first.........................proved - complete [shostak](0.03 s)
prefix?_rest..........................proved - complete [shostak](0.03 s)
prefix?_length........................proved - complete [shostak](0.11 s)
prefix?_length_eq.....................proved - complete [shostak](0.12 s)
prefix?_index.........................proved - complete [shostak](0.04 s)
prefix?_nth_TCC1......................proved - complete [shostak](0.03 s)
prefix?_nth...........................proved - complete [shostak](0.15 s)
prefix?_concatenate...................proved - complete [shostak](0.08 s)
prefix?_def...........................proved - complete [shostak](0.10 s)
prefix?_is_partial_order..............proved - complete [shostak](0.16 s)
prefix?_total_order...................proved - complete [shostak](0.27 s)
prefix_TCC1...........................proved - complete [shostak](0.02 s)
prefix_TCC2...........................proved - complete [shostak](0.04 s)
prefix_TCC3...........................proved - complete [shostak](0.04 s)
prefix_TCC4...........................proved - complete [shostak](0.02 s)
prefix_TCC5...........................proved - complete [shostak](0.04 s)
prefix_0..............................proved - complete [shostak](0.03 s)
prefix_extract........................proved - complete [shostak](0.10 s)
prefix_rest_TCC1......................proved - complete [shostak](0.03 s)
prefix_rest...........................proved - complete [shostak](0.09 s)
prefix_prefix.........................proved - complete [shostak](0.29 s)
prefix_length.........................proved - complete [shostak](0.15 s)
prefix_index..........................proved - complete [shostak](0.15 s)
prefix_full...........................proved - complete [shostak](0.09 s)
prefix_concatenate_TCC1...............proved - complete [shostak](0.03 s)
prefix_concatenate_TCC2...............proved - complete [shostak](0.05 s)
prefix_concatenate....................proved - complete [shostak](1.08 s)
prefix?_prefix........................proved - complete [shostak](0.40 s)
prefix_some...........................proved - complete [shostak](0.07 s)
prefix_every..........................proved - complete [shostak](0.07 s)
prefix?_order.........................proved - complete [shostak](0.16 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (4.25 s)
Proof summary for theory csequence_filter_map
map_first_p_TCC1......................proved - complete [shostak](-.66 s)
map_first_p...........................proved - complete [shostak](1.03 s)
map_suffix_empty......................proved - complete [shostak](0.13 s)
map_suffix............................proved - complete [shostak](0.09 s)
filter_map............................proved - complete [shostak](0.77 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.37 s)
Proof summary for theory csequence_map_props
map_empty.............................proved - complete [shostak](0.06 s)
map_nonempty..........................proved - complete [shostak](0.05 s)
map_finite............................proved - complete [shostak](0.05 s)
map_infinite..........................proved - complete [shostak](0.11 s)
map_first_TCC1........................proved - complete [shostak](0.03 s)
map_first.............................proved - complete [shostak](0.03 s)
map_rest..............................proved - complete [shostak](0.03 s)
map_length............................proved - complete [shostak](0.13 s)
map_index.............................proved - complete [shostak](0.06 s)
map_nth_TCC1..........................proved - complete [shostak](0.03 s)
map_nth...............................proved - complete [shostak](0.17 s)
map_add...............................proved - complete [shostak](0.03 s)
map_last_TCC1.........................proved - complete [shostak](0.02 s)
map_last..............................proved - complete [shostak](0.06 s)
map_map...............................proved - complete [shostak](0.11 s)
map_injective.........................proved - complete [shostak](0.24 s)
map_extensionality....................proved - complete [shostak](0.04 s)
map_some..............................proved - complete [shostak](0.15 s)
map_every.............................proved - complete [shostak](0.13 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (1.53 s)
Proof summary for theory csequence_finseq
from_finseq_TCC1......................proved - complete [shostak](0.03 s)
from_finseq_TCC2......................proved - complete [shostak](0.03 s)
from_finseq_TCC3......................proved - complete [shostak](0.03 s)
from_finseq_TCC4......................proved - complete [shostak](0.02 s)
from_finseq_TCC5......................proved - complete [shostak](0.03 s)
from_finseq_length....................proved - complete [shostak](0.10 s)
from_finseq_index.....................proved - complete [shostak](0.03 s)
from_finseq_nth_TCC1..................proved - complete [shostak](0.03 s)
from_finseq_nth.......................proved - complete [shostak](0.21 s)
to_finseq_TCC1........................proved - complete [shostak](0.03 s)
to_finseq_length......................proved - complete [shostak](0.02 s)
to_finseq_index.......................proved - complete [shostak](0.03 s)
to_finseq_nth_TCC1....................proved - complete [shostak](0.03 s)
to_finseq_nth.........................proved - complete [shostak](0.02 s)
to_from_finseq........................proved - complete [shostak](0.44 s)
from_to_finseq........................proved - complete [shostak](0.07 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (1.12 s)
Proof summary for theory csequence_flatten
some_every_empty......................proved - complete [shostak](0.04 s)
flatten_struct_TCC1...................proved - complete [shostak](0.04 s)
flatten_struct_TCC2...................proved - complete [shostak](0.04 s)
flatten_struct_TCC3...................proved - complete [shostak](0.03 s)
flatten_struct_TCC4...................proved - complete [shostak](0.04 s)
flatten_TCC1..........................proved - complete [shostak](0.03 s)
flatten_empty.........................proved - complete [shostak](0.18 s)
flatten_empty_cseq....................proved - complete [shostak](0.03 s)
flatten_nonempty......................proved - complete [shostak](0.07 s)
flatten_filter........................proved - complete [shostak](0.04 s)
flatten_reduce_TCC1...................proved - complete [shostak](0.03 s)
flatten_reduce........................proved - complete [shostak](0.06 s)
flatten_rest_TCC1.....................proved - complete [shostak](0.10 s)
flatten_rest_TCC2.....................proved - complete [shostak](0.17 s)
flatten_rest..........................proved - complete [shostak](0.55 s)
flatten_rest2_TCC1....................proved - complete [shostak](0.04 s)
flatten_rest2_TCC2....................proved - complete [shostak](0.04 s)
flatten_rest2.........................proved - complete [shostak](0.47 s)
flatten_first.........................proved - complete [shostak](0.21 s)
flatten_suffix........................proved - complete [shostak](0.27 s)
flatten_concatenate...................proved - complete [shostak](0.63 s)
flatten_rest_suffix_TCC1..............proved - complete [shostak](0.03 s)
flatten_rest_suffix_TCC2..............proved - complete [shostak](0.13 s)
flatten_rest_suffix...................proved - complete [shostak](0.28 s)
flatten_finite........................proved - complete [shostak](0.87 s)
flatten_infinite......................proved - complete [shostak](0.09 s)
length_of_flatten_TCC1................proved - complete [shostak](0.04 s)
length_of_flatten_TCC2................proved - complete [shostak](0.02 s)
length_of_flatten_TCC3................proved - complete [shostak](0.05 s)
length_of_flatten_TCC4................proved - complete [shostak](0.14 s)
length_of_flatten_TCC5................proved - complete [shostak](0.15 s)
length_of_flatten_add_TCC1............proved - complete [shostak](0.03 s)
length_of_flatten_add.................proved - complete [shostak](0.43 s)
flatten_length........................proved - complete [shostak](0.48 s)
flatten_some..........................proved - complete [shostak](0.41 s)
flatten_some_finite...................proved - complete [shostak](0.09 s)
flatten_every.........................proved - complete [shostak](0.41 s)
flatten_every_finite..................proved - complete [shostak](0.09 s)
Theory totals: 38 formulas, 38 attempted, 38 succeeded (6.81 s)
Proof summary for theory csequence_prefix_suffix
prefix_suffix_eta.....................proved - complete [shostak](0.10 s)
prefix_suffix_extensionality..........proved - complete [shostak](0.05 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.15 s)
Proof summary for theory csequence_generate
generate_TCC1.........................proved - complete [shostak](0.11 s)
generate_first........................proved - complete [shostak](0.06 s)
generate_rest.........................proved - complete [shostak](0.07 s)
generate_nth_TCC1.....................proved - complete [shostak](0.03 s)
generate_nth..........................proved - complete [shostak](0.09 s)
generate_add..........................proved - complete [shostak](0.05 s)
generate_some.........................proved - complete [shostak](0.05 s)
generate_every........................proved - complete [shostak](0.05 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.50 s)
Proof summary for theory csequence_generate_limit
generate_empty........................proved - complete [shostak](0.09 s)
generate_first_TCC1...................proved - complete [shostak](0.03 s)
generate_first........................proved - complete [shostak](0.09 s)
generate_rest.........................proved - complete [shostak](0.10 s)
generate_has_length...................proved - complete [shostak](0.35 s)
generate_finite.......................proved - complete [shostak](0.08 s)
generate_nth..........................proved - complete [shostak](0.26 s)
generate_add..........................proved - complete [shostak](-.61 s)
generate_some.........................proved - complete [shostak](0.04 s)
generate_every........................proved - complete [shostak](0.04 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.46 s)
Proof summary for theory csequence_induction
cseq_induction........................proved - complete [shostak](0.11 s)
cseq_infinite_induction_TCC1..........proved - complete [shostak](0.03 s)
cseq_infinite_induction_TCC2..........proved - complete [shostak](0.03 s)
cseq_infinite_induction_TCC3..........proved - complete [shostak](0.03 s)
cseq_infinite_induction...............proved - complete [shostak](0.07 s)
CSEQ_induction........................proved - complete [shostak](0.14 s)
CSEQ_infinite_induction_TCC1..........proved - complete [shostak](0.03 s)
CSEQ_infinite_induction_TCC2..........proved - complete [shostak](0.03 s)
CSEQ_infinite_induction...............proved - complete [shostak](0.05 s)
finite_sequence_induction.............proved - complete [shostak](0.04 s)
FINITE_SEQUENCE_induction.............proved - complete [shostak](0.06 s)
sequence_induction....................proved - complete [shostak](0.04 s)
SEQUENCE_induction....................proved - complete [shostak](0.04 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.67 s)
Proof summary for theory csequence_insert_remove
insert_remove_eta.....................proved - complete [shostak](0.14 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.14 s)
Proof summary for theory csequence_remove
remove_TCC1...........................proved - complete [shostak](0.03 s)
remove_TCC2...........................proved - complete [shostak](0.04 s)
remove_TCC3...........................proved - complete [shostak](0.04 s)
remove_TCC4...........................proved - complete [shostak](0.02 s)
remove_finite.........................proved - complete [shostak](0.06 s)
remove_infinite.......................proved - complete [shostak](0.05 s)
remove_0..............................proved - complete [shostak](0.03 s)
remove_empty..........................proved - complete [shostak](0.04 s)
remove_nonempty.......................proved - complete [shostak](0.04 s)
remove_first_TCC1.....................proved - complete [shostak](0.03 s)
remove_first_TCC2.....................proved - complete [shostak](0.03 s)
remove_first_TCC3.....................proved - complete [shostak](0.03 s)
remove_first..........................proved - complete [shostak](0.05 s)
remove_rest_TCC1......................proved - complete [shostak](0.03 s)
remove_rest_TCC2......................proved - complete [shostak](0.04 s)
remove_rest...........................proved - complete [shostak](0.20 s)
remove_upfrom_length..................proved - complete [shostak](0.14 s)
remove_length.........................proved - complete [shostak](0.18 s)
remove_index..........................proved - complete [shostak](0.15 s)
remove_nth_TCC1.......................proved - complete [shostak](0.09 s)
remove_nth............................proved - complete [shostak](0.22 s)
remove_add............................proved - complete [shostak](0.02 s)
remove_last_TCC1......................proved - complete [shostak](0.12 s)
remove_last_TCC2......................proved - complete [shostak](0.03 s)
remove_last...........................proved - complete [shostak](0.98 s)
remove_remove_TCC1....................proved - complete [shostak](0.04 s)
remove_remove.........................proved - complete [shostak](0.32 s)
remove_extensionality.................proved - complete [shostak](0.25 s)
remove_some...........................proved - complete [shostak](0.21 s)
remove_every..........................proved - complete [shostak](0.06 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (3.54 s)
Proof summary for theory csequence_length_comp
length_lt_le..........................proved - complete [shostak](0.04 s)
length_gt_ge..........................proved - complete [shostak](0.03 s)
length_eq_le..........................proved - complete [shostak](0.03 s)
length_eq_ge..........................proved - complete [shostak](0.04 s)
length_lt_neq.........................proved - complete [shostak](0.04 s)
length_gt_neq.........................proved - complete [shostak](0.03 s)
length_eq_empty.......................proved - complete [shostak](0.09 s)
length_eq_rest........................proved - complete [shostak](0.05 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.34 s)
Proof summary for theory csequence_limit
prefix_chain_TCC1.....................proved - complete [shostak](0.06 s)
suffix_chain_TCC1.....................proved - complete [shostak](0.19 s)
rest_chain_TCC1.......................proved - complete [shostak](0.04 s)
rest_chain_TCC2.......................proved - complete [shostak](0.11 s)
ascending_chain?_nth..................proved - complete [shostak](0.04 s)
limit_struct_TCC1.....................proved - complete [shostak](0.08 s)
limit_struct_TCC2.....................proved - complete [shostak](0.05 s)
limit_empty...........................proved - complete [shostak](0.15 s)
limit_nonempty........................proved - complete [shostak](0.15 s)
limit_first_TCC1......................proved - complete [shostak](0.03 s)
limit_first...........................proved - complete [shostak](0.22 s)
limit_rest_chain......................proved - complete [shostak](0.19 s)
limit_suffix_chain....................proved - complete [shostak](0.90 s)
limit_lub.............................proved - complete [shostak](0.47 s)
limit_nth.............................proved - complete [shostak](0.09 s)
limit_def.............................proved - complete [shostak](0.66 s)
limit_prefix_chain....................proved - complete [shostak](0.10 s)
limit_prefix_compact_TCC1.............proved - complete [shostak](0.05 s)
limit_prefix_compact..................proved - complete [shostak](0.36 s)
limit_finite_compact..................proved - complete [shostak](0.29 s)
continuous?_infinite..................proved - complete [shostak](0.07 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (4.30 s)
Proof summary for theory csequence_list
from_list_TCC1........................proved - complete [shostak](0.03 s)
from_list_TCC2........................proved - complete [shostak](0.04 s)
from_list_TCC3........................proved - complete [shostak](0.03 s)
from_list_length......................proved - complete [shostak](0.04 s)
from_list_index.......................proved - complete [shostak](0.09 s)
from_list_nth_TCC1....................proved - complete [shostak](0.03 s)
from_list_nth.........................proved - complete [shostak](0.10 s)
to_list_TCC1..........................proved - complete [shostak](0.03 s)
to_list_TCC2..........................proved - complete [shostak](0.03 s)
to_list_TCC3..........................proved - complete [shostak](0.06 s)
to_list_length........................proved - complete [shostak](0.09 s)
to_list_index.........................proved - complete [shostak](0.13 s)
to_list_nth_TCC1......................proved - complete [shostak](0.02 s)
to_list_nth...........................proved - complete [shostak](0.13 s)
to_from_list..........................proved - complete [shostak](0.04 s)
from_to_list..........................proved - complete [shostak](0.06 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.93 s)
Proof summary for theory csequence_map_composition
map_composition.......................proved - complete [shostak](0.23 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.23 s)
Proof summary for theory csequence_merge
merge_struct_TCC1.....................proved - complete [shostak](0.03 s)
merge_struct_TCC2.....................proved - complete [shostak](0.02 s)
merge_empty...........................proved - complete [shostak](0.13 s)
merge_nonempty........................proved - complete [shostak](0.14 s)
merge_empty_left......................proved - complete [shostak](0.51 s)
merge_empty_right.....................proved - complete [shostak](0.52 s)
merge_first_TCC1......................proved - complete [shostak](0.03 s)
merge_first...........................proved - complete [shostak](0.16 s)
merge_rest............................proved - complete [shostak](0.11 s)
merge_finite..........................proved - complete [shostak](0.16 s)
merge_finiteness......................proved - complete [shostak](0.15 s)
merge_infinite1.......................proved - complete [shostak](0.02 s)
merge_infinite2.......................proved - complete [shostak](0.03 s)
merge_length..........................proved - complete [shostak](0.30 s)
merge_index_TCC1......................proved - complete [shostak](0.05 s)
merge_index...........................proved - complete [shostak](0.17 s)
merge_nth_TCC1........................proved - complete [shostak](0.05 s)
merge_nth_TCC2........................proved - complete [shostak](0.08 s)
merge_nth_TCC3........................proved - complete [shostak](0.05 s)
merge_nth_TCC4........................proved - complete [shostak](0.19 s)
merge_nth_TCC5........................proved - complete [shostak](0.35 s)
merge_nth_TCC6........................proved - complete [shostak](0.56 s)
merge_nth.............................proved - complete [shostak](7.39 s)
merge_add.............................proved - complete [shostak](0.10 s)
merge_last_TCC1.......................proved - complete [shostak](0.04 s)
merge_last_TCC2.......................proved - complete [shostak](0.04 s)
merge_last............................proved - complete [shostak](0.58 s)
merge_extensionality..................proved - complete [shostak](2.46 s)
merge_some............................proved - complete [shostak](0.57 s)
merge_every...........................proved - complete [shostak](0.05 s)
Theory totals: 30 formulas, 30 attempted, 30 succeeded (15.02 s)
Proof summary for theory csequence_merge_split
merge_split_eta.......................proved - complete [shostak](0.40 s)
split_merge_eta.......................proved - complete [shostak](1.40 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.79 s)
Proof summary for theory csequence_split
split_left_struct_TCC1................proved - complete [shostak](0.03 s)
split_left_struct_TCC2................proved - complete [shostak](0.04 s)
split_empty_left......................proved - complete [shostak](0.13 s)
split_empty_right.....................proved - complete [shostak](0.12 s)
split_nonempty_left...................proved - complete [shostak](0.13 s)
split_nonempty_right..................proved - complete [shostak](0.12 s)
split_first_left_TCC1.................proved - complete [shostak](0.03 s)
split_first_left......................proved - complete [shostak](0.11 s)
split_first_right_TCC1................proved - complete [shostak](0.03 s)
split_first_right.....................proved - complete [shostak](0.13 s)
split_rest_left_TCC1..................proved - complete [shostak](0.04 s)
split_rest_left.......................proved - complete [shostak](0.14 s)
split_rest_right......................proved - complete [shostak](0.14 s)
split_rest_swap_left..................proved - complete [shostak](0.72 s)
split_rest_swap_right.................proved - complete [shostak](0.92 s)
split_finite..........................proved - complete [shostak](0.18 s)
split_infinite........................proved - complete [shostak](0.26 s)
split_length_left.....................proved - complete [shostak](0.28 s)
split_length_right....................proved - complete [shostak](0.26 s)
split_length..........................proved - complete [shostak](0.17 s)
split_index_left......................proved - complete [shostak](0.12 s)
split_index_right.....................proved - complete [shostak](0.14 s)
split_nth_left_TCC1...................proved - complete [shostak](0.05 s)
split_nth_left........................proved - complete [shostak](0.34 s)
split_nth_right_TCC1..................proved - complete [shostak](0.07 s)
split_nth_right.......................proved - complete [shostak](0.47 s)
split_add.............................proved - complete [shostak](1.38 s)
split_last_left_TCC1..................proved - complete [shostak](0.03 s)
split_last_left_TCC2..................proved - complete [shostak](0.10 s)
split_last_left.......................proved - complete [shostak](0.30 s)
split_last_right_TCC1.................proved - complete [shostak](0.03 s)
split_last_right_TCC2.................proved - complete [shostak](0.10 s)
split_last_right......................proved - complete [shostak](0.27 s)
split_extensionality..................proved - complete [shostak](0.14 s)
split_some............................proved - complete [shostak](0.24 s)
split_every...........................proved - complete [shostak](0.05 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (7.80 s)
Proof summary for theory csequence_prefix_append
prefix_append_eta.....................proved - complete [shostak](0.34 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.34 s)
Proof summary for theory csequence_rest
rest_finite...........................proved - complete [shostak](0.02 s)
rest_infinite.........................proved - complete [shostak](0.02 s)
rest_empty_add........................proved - complete [shostak](0.03 s)
rest_empty............................proved - complete [shostak](0.06 s)
rest_nonempty.........................proved - complete [shostak](0.09 s)
rest_first_TCC1.......................proved - complete [shostak](0.03 s)
rest_first............................proved - complete [shostak](0.03 s)
rest_length...........................proved - complete [shostak](0.03 s)
rest_index............................proved - complete [shostak](0.03 s)
rest_nth_TCC1.........................proved - complete [shostak](0.02 s)
rest_nth..............................proved - complete [shostak](0.03 s)
rest_some.............................proved - complete [shostak](0.02 s)
rest_every............................proved - complete [shostak](0.03 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.44 s)
Proof summary for theory csequence_reverse
reverse_TCC1..........................proved - complete [shostak](0.03 s)
reverse_TCC2..........................proved - complete [shostak](0.03 s)
reverse_TCC3..........................proved - complete [shostak](0.07 s)
reverse_empty.........................proved - complete [shostak](0.04 s)
reverse_nonempty......................proved - complete [shostak](0.04 s)
reverse_first_TCC1....................proved - complete [shostak](0.03 s)
reverse_first.........................proved - complete [shostak](0.28 s)
reverse_last..........................proved - complete [shostak](0.02 s)
reverse_length........................proved - complete [shostak](0.13 s)
reverse_index.........................proved - complete [shostak](0.05 s)
reverse_nth_TCC1......................proved - complete [shostak](0.05 s)
reverse_nth...........................proved - complete [shostak](0.43 s)
reverse_add1..........................proved - complete [shostak](0.58 s)
reverse_add2_TCC1.....................proved - complete [shostak](0.02 s)
reverse_add2..........................proved - complete [shostak](0.02 s)
reverse_reverse.......................proved - complete [shostak](0.11 s)
reverse_extensionality................proved - complete [shostak](0.12 s)
reverse_some..........................proved - complete [shostak](-.49 s)
reverse_every.........................proved - complete [shostak](0.04 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (1.59 s)
Proof summary for theory csequence_sequence
from_sequence_TCC1....................proved - complete [shostak](0.12 s)
from_sequence_nth_TCC1................proved - complete [shostak](0.02 s)
from_sequence_nth.....................proved - complete [shostak](0.10 s)
to_sequence_TCC1......................proved - complete [shostak](0.03 s)
to_sequence_nth.......................proved - complete [shostak](0.02 s)
to_from_sequence......................proved - complete [shostak](0.04 s)
from_to_sequence......................proved - complete [shostak](0.05 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.38 s)
Proof summary for theory csequence_strict_prefix
strict_prefix?_TCC1...................proved - complete [shostak](0.04 s)
strict_prefix?_prefix?................proved - complete [shostak](0.13 s)
strict_prefix?_finite.................proved - complete [shostak](0.03 s)
strict_prefix?_first_TCC1.............proved - complete [shostak](0.03 s)
strict_prefix?_first..................proved - complete [shostak](0.03 s)
strict_prefix?_rest...................proved - complete [shostak](0.03 s)
strict_prefix?_length_TCC1............proved - complete [shostak](0.03 s)
strict_prefix?_length.................proved - complete [shostak](0.05 s)
strict_prefix?_index..................proved - complete [shostak](0.04 s)
strict_prefix?_nth_TCC1...............proved - complete [shostak](0.03 s)
strict_prefix?_nth....................proved - complete [shostak](0.04 s)
strict_prefix?_concatenate............proved - complete [shostak](0.07 s)
strict_prefix?_def....................proved - complete [shostak](0.17 s)
strict_prefix?_is_strict_order........proved - complete [shostak](0.11 s)
strict_prefix?_well_ordered...........proved - complete [shostak](0.26 s)
strict_prefix?_prefix.................proved - complete [shostak](0.16 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (1.23 s)
Proof summary for theory csequence_unzip
unzip_left_struct_TCC1................proved - complete [shostak](0.03 s)
unzip_finite..........................proved - complete [shostak](0.26 s)
unzip_infinite........................proved - complete [shostak](0.31 s)
unzip_nonempty........................proved - complete [shostak](0.13 s)
unzip_empty_left......................proved - complete [shostak](0.09 s)
unzip_empty_right.....................proved - complete [shostak](0.09 s)
unzip_first_left......................proved - complete [shostak](0.08 s)
unzip_first_right.....................proved - complete [shostak](0.08 s)
unzip_rest_left.......................proved - complete [shostak](0.09 s)
unzip_rest_right......................proved - complete [shostak](0.09 s)
unzip_length_left.....................proved - complete [shostak](0.21 s)
unzip_length_right....................proved - complete [shostak](0.20 s)
unzip_index_left......................proved - complete [shostak](0.08 s)
unzip_index_right.....................proved - complete [shostak](0.08 s)
unzip_nth_left_TCC1...................proved - complete [shostak](0.03 s)
unzip_nth_left........................proved - complete [shostak](0.28 s)
unzip_nth_right_TCC1..................proved - complete [shostak](0.04 s)
unzip_nth_right.......................proved - complete [shostak](0.28 s)
unzip_map.............................proved - complete [shostak](0.49 s)
unzip_extensionality..................proved - complete [shostak](0.93 s)
unzip_add.............................proved - complete [shostak](0.14 s)
unzip_last_left_TCC1..................proved - complete [shostak](0.04 s)
unzip_last_left.......................proved - complete [shostak](0.05 s)
unzip_last_right_TCC1.................proved - complete [shostak](0.04 s)
unzip_last_right......................proved - complete [shostak](0.05 s)
unzip_some............................proved - complete [shostak](0.14 s)
unzip_every...........................proved - complete [shostak](0.14 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (4.45 s)
Proof summary for theory csequence_zip
zip_struct_TCC1.......................proved - complete [shostak](0.03 s)
zip_struct_TCC2.......................proved - complete [shostak](0.03 s)
zip_finite1...........................proved - complete [shostak](0.19 s)
zip_finite2...........................proved - complete [shostak](0.18 s)
zip_infinite..........................proved - complete [shostak](0.16 s)
zip_nonempty..........................proved - complete [shostak](0.09 s)
zip_empty.............................proved - complete [shostak](0.11 s)
zip_first.............................proved - complete [shostak](0.08 s)
zip_rest..............................proved - complete [shostak](0.09 s)
zip_add...............................proved - complete [shostak](0.09 s)
zip_length_TCC1.......................proved - complete [shostak](0.04 s)
zip_length............................proved - complete [shostak](0.93 s)
zip_index.............................proved - complete [shostak](0.41 s)
zip_nth_TCC1..........................proved - complete [shostak](0.03 s)
zip_nth_TCC2..........................proved - complete [shostak](0.04 s)
zip_nth...............................proved - complete [shostak](0.50 s)
zip_last_TCC1.........................proved - complete [shostak](0.06 s)
zip_last_TCC2.........................proved - complete [shostak](0.05 s)
zip_last_TCC3.........................proved - complete [shostak](0.10 s)
zip_last_TCC4.........................proved - complete [shostak](0.06 s)
zip_last_TCC5.........................proved - complete [shostak](0.10 s)
zip_last_TCC6.........................proved - complete [shostak](0.06 s)
zip_last_TCC7.........................proved - complete [shostak](0.04 s)
zip_last_TCC8.........................proved - complete [shostak](0.04 s)
zip_last_TCC9.........................proved - complete [shostak](0.07 s)
zip_last..............................proved - complete [shostak](0.27 s)
zip_extensionality....................proved - complete [shostak](0.67 s)
zip_some_TCC1.........................proved - complete [shostak](0.06 s)
zip_some_TCC2.........................proved - complete [shostak](0.05 s)
zip_some_TCC3.........................proved - complete [shostak](0.06 s)
zip_some..............................proved - complete [shostak](0.41 s)
zip_every_TCC1........................proved - complete [shostak](0.06 s)
zip_every.............................proved - complete [shostak](0.42 s)
Theory totals: 33 formulas, 33 attempted, 33 succeeded (5.59 s)
Proof summary for theory csequence_zip_unzip
zip_unzip_eta.........................proved - complete [shostak](0.74 s)
unzip_zip_eta.........................proved - complete [shostak](0.46 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.20 s)
Grand Totals: 726 proofs, 726 attempted, 726 succeeded (106.67 s)
[ Verzeichnis aufwärts0.960unsichere Verbindung
]
|
|
|
|
|
|
