| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: lim_of_composition.pvs Sprache: PVS
|
Untersuchungsergebnis.summary Download desMT940 {MT940[418] Hlasm[1930] Haskell[2258]}zum Wurzelverzeichnis wechseln *** *** 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) [ zur Elbe Produktseite wechseln0.276Quellennavigators ] |