Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[795] Hlasm[2301] Haskell[2619]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen]
***
*** top (18:26:9 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 matrices
IMP_sigma_swap_TCC1...................proved - complete [shostak](0.04 s)
length_matrix_eq......................proved - complete [shostak](0.09 s)
nth_matrix_eq_TCC1....................proved - complete [shostak](0.03 s)
nth_matrix_eq.........................proved - complete [shostak](-1.43 s)
length_matrix_equiv...................proved - complete [shostak](0.06 s)
length_matrix_nth.....................proved - complete [shostak](0.34 s)
matrix_listn_nth_TCC1.................proved - complete [shostak](0.04 s)
matrix_listn_nth......................proved - complete [shostak](0.04 s)
length_rows...........................proved - complete [shostak](0.01 s)
columns_TCC1..........................proved - complete [shostak](0.02 s)
columns_TCC2..........................proved - complete [shostak](0.03 s)
columns_TCC3..........................proved - complete [shostak](0.05 s)
columns_TCC4..........................proved - complete [shostak](0.29 s)
row_TCC1..............................proved - complete [shostak](0.02 s)
col_TCC1..............................proved - complete [shostak](0.04 s)
col_TCC2..............................proved - complete [shostak](0.06 s)
col_def_TCC1..........................proved - complete [shostak](0.03 s)
col_def_TCC2..........................proved - complete [shostak](0.03 s)
col_def...............................proved - complete [shostak](0.59 s)
col_zero..............................proved - complete [shostak](0.19 s)
access_zero...........................proved - complete [shostak](0.03 s)
entry_test............................proved - complete [shostak](0.02 s)
access_row............................proved - complete [shostak](0.01 s)
access_col............................proved - complete [shostak](0.11 s)
coltest...............................proved - complete [shostak](0.02 s)
full_matrix_columns_TCC1..............proved - complete [shostak](0.06 s)
full_matrix_columns...................proved - complete [shostak](0.07 s)
rows_mn...............................proved - complete [shostak](0.01 s)
columns_mn............................proved - complete [shostak](0.05 s)
length_row............................proved - complete [shostak](0.06 s)
length_col............................proved - complete [shostak](0.02 s)
columns_0_entry.......................proved - complete [shostak](0.06 s)
rows_0_entry..........................proved - complete [shostak](0.08 s)
entry_eq_0............................proved - complete [shostak](0.04 s)
add_TCC1..............................proved - complete [shostak](0.04 s)
add_TCC2..............................proved - complete [shostak](0.05 s)
add_TCC3..............................proved - complete [shostak](0.02 s)
add_TCC4..............................proved - complete [shostak](0.02 s)
add_TCC5..............................proved - complete [shostak](0.09 s)
add_TCC6..............................proved - complete [shostak](0.15 s)
scal_TCC1.............................proved - complete [shostak](0.02 s)
scal_TCC2.............................proved - complete [shostak](0.04 s)
scal_TCC3.............................proved - complete [shostak](0.06 s)
sub_TCC1..............................proved - complete [shostak](0.06 s)
super_dot_TCC1........................proved - complete [shostak](0.04 s)
super_dot_TCC2........................proved - complete [shostak](0.06 s)
super_dot_TCC3........................proved - complete [shostak](0.07 s)
super_duper_dot_TCC1..................proved - complete [shostak](0.01 s)
super_duper_dot_TCC2..................proved - complete [shostak](0.01 s)
access_sum............................proved - complete [shostak](1.48 s)
access_scal...........................proved - complete [shostak](0.34 s)
vect_scal_1...........................proved - complete [shostak](0.06 s)
dot_eq_sigma_TCC1.....................proved - complete [shostak](0.04 s)
dot_eq_sigma..........................proved - complete [shostak](1.43 s)
dot_zero_right........................proved - complete [shostak](0.12 s)
dot_commutes..........................proved - complete [shostak](0.07 s)
dot_zero_left.........................proved - complete [shostak](0.02 s)
length_add_vect.......................proved - complete [shostak](0.04 s)
length_add_vect_same..................proved - complete [shostak](0.05 s)
length_scal_vect......................proved - complete [shostak](0.02 s)
form_matrix_TCC1......................proved - complete [shostak](0.06 s)
form_matrix_TCC2......................proved - complete [shostak](0.06 s)
form_matrix_TCC3......................proved - complete [shostak](0.38 s)
columns_form_matrix...................proved - complete [shostak](0.07 s)
rows_form_matrix......................proved - complete [shostak](0.02 s)
form_matrix_empty.....................proved - complete [shostak](0.42 s)
form_matrix_test1.....................proved - complete [shostak](0.04 s)
full_matrix_eq........................proved - complete [shostak](0.22 s)
matrix2array..........................proved - complete [shostak](1.61 s)
entry_form_matrix.....................proved - complete [shostak](0.11 s)
entry_form_matrix2....................proved - complete [shostak](0.09 s)
form_matrix_eq........................proved - complete [shostak](0.53 s)
matrix_reduce_prop....................proved - complete [shostak](0.75 s)
mult_TCC1.............................proved - complete [shostak](0.23 s)
mult_full.............................proved - complete [shostak](0.04 s)
mult_null_left........................proved - complete [shostak](0.08 s)
mult_null_right.......................proved - complete [shostak](0.15 s)
columns_mult..........................proved - complete [shostak](1.43 s)
rows_mult.............................proved - complete [shostak](0.02 s)
columns_append........................proved - complete [shostak](0.56 s)
append_mult...........................proved - complete [shostak](2.48 s)
matrix_mult_assoc.....................proved - complete [shostak](9.53 s)
entry_mult............................proved - complete [shostak](0.05 s)
form_matrix_mult_TCC1.................proved - complete [shostak](0.04 s)
form_matrix_mult......................proved - complete [shostak](1.44 s)
add_TCC7..............................proved - complete [shostak](0.71 s)
columns_add...........................proved - complete [shostak](0.43 s)
rows_add..............................proved - complete [shostak](0.04 s)
matrix_add_assoc......................proved - complete [shostak](2.32 s)
matrix_add_comm.......................proved - complete [shostak](0.89 s)
scal_TCC4.............................proved - complete [shostak](0.12 s)
columns_scal..........................proved - complete [shostak](0.31 s)
rows_scal.............................proved - complete [shostak](0.05 s)
sub_TCC2..............................proved - complete [shostak](0.27 s)
rows_sub..............................proved - complete [shostak](0.12 s)
columns_sub...........................proved - complete [shostak](0.16 s)
matrix_sub_test.......................proved - complete [shostak](0.06 s)
Id_TCC1...............................proved - complete [shostak](0.83 s)
mult_Id_left..........................proved - complete [shostak](0.24 s)
mult_Id_right.........................proved - complete [shostak](0.23 s)
rows_Id...............................proved - complete [shostak](0.06 s)
columns_Id............................proved - complete [shostak](0.07 s)
entry_Id..............................proved - complete [shostak](0.08 s)
transpose_TCC1........................proved - complete [shostak](0.12 s)
rows_transpose........................proved - complete [shostak](0.04 s)
columns_transpose.....................proved - complete [shostak](0.04 s)
entry_transpose.......................proved - complete [shostak](0.09 s)
transpose_transpose...................proved - complete [shostak](0.08 s)
transpose_mult_TCC1...................proved - complete [shostak](0.08 s)
transpose_mult........................proved - complete [shostak](0.96 s)
form_matrix_square....................proved - complete [shostak](0.05 s)
transpose_Id..........................proved - complete [shostak](0.23 s)
vect2matrix_TCC1......................proved - complete [shostak](0.06 s)
vect2matrix_eq........................proved - complete [shostak](0.16 s)
Theory totals: 114 formulas, 114 attempted, 114 succeeded (34.96 s)
Proof summary for theory matrix_inv
left_inv_TCC1........................proved - complete [shostak]( 0.09 s)
left_inv_TCC2........................proved - incomplete [shostak]( 0.16 s)
left_inv_TCC3........................proved - incomplete [shostak]( 1.83 s)
mult_left_inv_right_TCC1.............proved - complete [shostak]( 0.05 s)
mult_left_inv_right..................proved - incomplete [shostak]( 6.29 s)
invertible?_TCC1.....................proved - complete [shostak]( 0.08 s)
invertible_rew.......................proved - incomplete [shostak]( 3.87 s)
inverse_TCC1.........................proved - incomplete [shostak]( 0.20 s)
inverse_TCC2.........................proved - incomplete [shostak]( 0.79 s)
mult_inverse_left_TCC1...............proved - complete [shostak]( 8.60 s)
mult_inverse_left_TCC2...............proved - complete [shostak]( 6.99 s)
mult_inverse_left....................proved - incomplete [shostak]( 0.16 s)
mult_inverse_right...................proved - incomplete [shostak]( 0.16 s)
inverse_unique.......................proved - incomplete [shostak]( 6.88 s)
invertible_det.......................proved - incomplete [shostak]( 0.29 s)
invertible_mult_TCC1.................proved - complete [shostak]( 0.14 s)
invertible_mult......................proved - incomplete [shostak]( 0.38 s)
inverse_mult_TCC1....................proved - incomplete [shostak]( 0.28 s)
inverse_mult.........................proved - incomplete [shostak]( 3.04 s)
det_inverse_TCC1.....................proved - incomplete [shostak]( 0.02 s)
det_inverse..........................proved - incomplete [shostak]( 0.29 s)
inverse_invertible...................proved - incomplete [shostak]( 0.22 s)
inverse_inverse_TCC1.................proved - incomplete [shostak]( 0.27 s)
inverse_inverse......................proved - incomplete [shostak]( 0.50 s)
GH_TCC1..............................proved - complete [shostak]( 0.01 s)
GH_TCC2..............................proved - complete [shostak]( 0.01 s)
GH_TCC3..............................proved - complete [shostak]( 0.02 s)
GH_TCC4..............................proved - complete [shostak]( 0.21 s)
det_nonzero_simple_prod..............proved - incomplete [shostak](18.07 s)
mult_induction_TCC1..................proved - complete [shostak]( 0.05 s)
mult_induction_TCC2..................proved - complete [shostak]( 2.69 s)
mult_induction_TCC3..................proved - complete [shostak]( 2.78 s)
mult_induction_TCC4..................proved - complete [shostak]( 0.37 s)
mult_induction.......................proved - incomplete [shostak]( 1.55 s)
det_transpose........................proved - incomplete [shostak]( 1.93 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (69.27 s)
Proof summary for theory matrix_diag
diagonalize_TCC1......................proved - complete [shostak](0.18 s)
diagonalize_TCC2......................proved - complete [shostak](0.27 s)
diagonalize_TCC3......................proved - complete [shostak](0.04 s)
diagonalize_TCC4......................proved - complete [shostak](0.29 s)
diagonalize_TCC5......................proved - complete [shostak](0.31 s)
diagonalize_TCC6......................proved - complete [shostak](0.20 s)
diagonalize_TCC7......................proved - complete [shostak](1.08 s)
diagonalize_TCC8......................proved - complete [shostak](0.22 s)
diagonalize_TCC9......................proved - complete [shostak](0.28 s)
diagonalize_TCC10.....................proved - complete [shostak](0.19 s)
diagonalize_TCC11.....................proved - complete [shostak](0.25 s)
diagonalize_TCC12.....................proved - complete [shostak](0.31 s)
diagonalize_TCC13.....................proved - complete [shostak](1.17 s)
diagonalize_TCC14.....................proved - complete [shostak](0.32 s)
diagonalize_TCC15.....................proved - complete [shostak](0.68 s)
diagonalize_TCC16.....................proved - complete [shostak](0.24 s)
diagonalize_TCC17.....................proved - complete [shostak](1.88 s)
diagonalize_TCC18.....................proved - complete [shostak](0.38 s)
diagonalize_TCC19.....................proved - complete [shostak](1.13 s)
diagonalize_TCC20.....................proved - complete [shostak](1.04 s)
diagonalize_TCC21.....................proved - complete [shostak](1.05 s)
diagonalize_TCC22.....................proved - complete [shostak](0.20 s)
diagonalize_TCC23.....................proved - complete [shostak](0.26 s)
diagonalize_TCC24.....................proved - complete [shostak](5.89 s)
diagonalize_TCC25.....................proved - complete [shostak](0.28 s)
diag_TCC1.............................proved - complete [shostak](0.04 s)
diag_TCC2.............................proved - complete [shostak](0.08 s)
diag_TCC3.............................proved - complete [shostak](0.28 s)
diag_TCC4.............................proved - complete [shostak](0.09 s)
diag_TCC5.............................proved - complete [shostak](0.05 s)
diag_TCC6.............................proved - complete [shostak](0.26 s)
diag_TCC7.............................proved - incomplete [shostak](0.39 s)
diag_TCC8.............................proved - incomplete [shostak](1.94 s)
diag_TCC9.............................proved - incomplete [shostak](0.43 s)
diag_TCC10............................proved - incomplete [shostak](3.70 s)
diag_TCC11............................proved - incomplete [shostak](5.69 s)
diag_TCC12............................proved - incomplete [shostak](5.73 s)
diag_TCC13............................proved - incomplete [shostak](6.14 s)
diag_det_zero_row.....................proved - incomplete [shostak](1.14 s)
det_mult..............................proved - incomplete [shostak](7.97 s)
Theory totals: 40 formulas, 40 attempted, 40 succeeded (52.08 s)
Proof summary for theory matrix_upper_triang
upper_triangulate_TCC1................proved - complete [shostak](0.18 s)
upper_triangulate_TCC2................proved - complete [shostak](0.21 s)
upper_triangulate_TCC3................proved - complete [shostak](0.03 s)
upper_triangulate_TCC4................proved - complete [shostak](0.26 s)
upper_triangulate_TCC5................proved - complete [shostak](0.25 s)
upper_triangulate_TCC6................proved - complete [shostak](0.21 s)
upper_triangulate_TCC7................proved - complete [shostak](0.18 s)
upper_triangulate_TCC8................proved - incomplete [shostak](0.44 s)
upper_triangulate_TCC9................proved - complete [shostak](0.21 s)
upper_triangulate_TCC10...............proved - complete [shostak](0.18 s)
upper_triangulate_TCC11...............proved - incomplete [shostak](0.20 s)
upper_triangulate_TCC12...............proved - complete [shostak](0.31 s)
upper_triangulate_TCC13...............proved - complete [shostak](0.40 s)
upper_triangulate_TCC14...............proved - complete [shostak](0.28 s)
upper_triangulate_TCC15...............proved - complete [shostak](1.03 s)
upper_triangulate_TCC16...............proved - complete [shostak](0.21 s)
upper_triangulate_TCC17...............proved - complete [shostak](1.93 s)
upper_triangulate_TCC18...............proved - complete [shostak](0.37 s)
upper_triangulate_TCC19...............proved - complete [shostak](0.80 s)
upper_triangulate_TCC20...............proved - complete [shostak](0.51 s)
upper_triangulate_TCC21...............proved - complete [shostak](0.46 s)
upper_triangulate_TCC22...............proved - complete [shostak](0.18 s)
upper_triangulate_TCC23...............proved - incomplete [shostak](0.70 s)
upper_triangulate_TCC24...............proved - incomplete [shostak](9.06 s)
upper_triangulate_TCC25...............proved - complete [shostak](0.30 s)
upper_triangulate_TCC26...............proved - complete [shostak](0.39 s)
upper_triangulate_TCC27...............proved - complete [shostak](0.31 s)
upper_triangulate_TCC28...............proved - complete [shostak](0.67 s)
upper_triangulate_TCC29...............proved - complete [shostak](0.22 s)
upper_triangulate_TCC30...............proved - complete [shostak](1.79 s)
upper_triangulate_TCC31...............proved - complete [shostak](0.42 s)
upper_triangulate_TCC32...............proved - complete [shostak](-.80 s)
upper_triangulate_TCC33...............proved - complete [shostak](0.63 s)
upper_triangulate_TCC34...............proved - complete [shostak](0.69 s)
upper_triangulate_TCC35...............proved - complete [shostak](1.10 s)
upper_triangulate_TCC36...............proved - incomplete [shostak](0.68 s)
upper_triangulate_TCC37...............proved - incomplete [shostak](7.06 s)
upper_triangulate_TCC38...............proved - complete [shostak](0.16 s)
Theory totals: 38 formulas, 38 attempted, 38 succeeded (32.25 s)
Proof summary for theory matrix_det
Esr_TCC1..............................proved - complete [shostak](0.13 s)
entry_Esr.............................proved - complete [shostak](0.09 s)
rows_Esr..............................proved - complete [shostak](0.06 s)
columns_Esr...........................proved - complete [shostak](0.07 s)
det_Esr...............................proved - complete [shostak](1.21 s)
transpose_Esr.........................proved - complete [shostak](0.14 s)
mult_Esr_left_TCC1....................proved - complete [shostak](0.04 s)
mult_Esr_left.........................proved - complete [shostak](1.46 s)
mult_Esr_Esr_inv......................proved - complete [shostak](0.59 s)
Ers_TCC1..............................proved - complete [shostak](0.93 s)
entry_Ers.............................proved - complete [shostak](0.21 s)
rows_Ers..............................proved - complete [shostak](0.13 s)
columns_Ers...........................proved - complete [shostak](0.15 s)
mult_Ers_left.........................proved - complete [shostak](2.18 s)
transpose_Ers.........................proved - complete [shostak](0.62 s)
det_Ers...............................proved - complete [shostak](0.54 s)
mult_Ers_Ers_inv......................proved - complete [shostak](0.75 s)
Easr_TCC1.............................proved - complete [shostak](0.24 s)
entry_Easr............................proved - complete [shostak](0.20 s)
rows_Easr.............................proved - complete [shostak](0.10 s)
columns_Easr..........................proved - complete [shostak](0.12 s)
mult_Easr_left_TCC1...................proved - complete [shostak](0.08 s)
mult_Easr_left........................proved - complete [shostak](1.52 s)
transpose_Easr........................proved - complete [shostak](0.33 s)
det_Easr..............................proved - complete [shostak](2.43 s)
mult_Easr_Easr_inv....................proved - complete [shostak](0.78 s)
ZERO_TCC1.............................proved - complete [shostak](0.09 s)
prod_diag_TCC1........................proved - complete [shostak](0.04 s)
prod_diag_TCC2........................proved - complete [shostak](0.04 s)
prod_diag_TCC3........................proved - complete [shostak](0.04 s)
prod_diag_remove_0_0_TCC1.............proved - complete [shostak](0.07 s)
prod_diag_remove_0_0..................proved - complete [shostak](0.65 s)
diagonal_upper_triangular.............proved - complete [shostak](0.01 s)
det_upper_triangular..................proved - complete [shostak](0.82 s)
det_upper_triangular_zero.............proved - complete [shostak](0.28 s)
upper_triangular_mult.................proved - complete [shostak](0.27 s)
lower_triangular_mult.................proved - complete [shostak](0.28 s)
upper_triangular_Id...................proved - complete [shostak](0.08 s)
lower_triangular_Id...................proved - complete [shostak](0.08 s)
upper_triangular_Easr.................proved - complete [shostak](0.09 s)
lower_triangular_Easr.................proved - complete [shostak](0.09 s)
prod_mat_TCC1.........................proved - complete [shostak](0.03 s)
prod_mat_TCC2.........................proved - complete [shostak](0.00 s)
prod_mat_TCC3.........................proved - complete [shostak](0.15 s)
prod_mat_eq...........................proved - complete [shostak](0.27 s)
mult_prod_mat_TCC1....................proved - complete [shostak](0.04 s)
mult_prod_mat.........................proved - complete [shostak](0.83 s)
prod_mat_expand_left_TCC1.............proved - complete [shostak](0.02 s)
prod_mat_expand_left..................proved - complete [shostak](0.87 s)
transpose_prod_mat_TCC1...............proved - complete [shostak](0.03 s)
transpose_prod_mat_TCC2...............proved - complete [shostak](0.06 s)
transpose_prod_mat....................proved - complete [shostak](0.79 s)
mult_simple_prod_TCC1.................proved - complete [shostak](0.11 s)
mult_simple_prod......................proved - complete [shostak](0.62 s)
Id_simple_prod........................proved - complete [shostak](0.21 s)
Esr_simple_prod.......................proved - complete [shostak](0.19 s)
Ers_simple_prod.......................proved - complete [shostak](0.31 s)
Easr_simple_prod......................proved - complete [shostak](0.19 s)
det_simple_prod_1.....................proved - complete [shostak](-.59 s)
det_mult_simple_prod_left.............proved - complete [shostak](1.47 s)
Easr_null.............................proved - complete [shostak](0.05 s)
transpose_simple_prod_TCC1............proved - complete [shostak](0.04 s)
transpose_simple_prod.................proved - complete [shostak](0.97 s)
diagonal_simple_prod..................proved - complete [shostak](3.40 s)
is_simple_prod_implic.................proved - complete [shostak](0.21 s)
Theory totals: 65 formulas, 65 attempted, 65 succeeded (28.30 s)
Proof summary for theory matrix_props
matrix_2x2...........................proved - complete [shostak]( 0.75 s)
length_row...........................proved - complete [shostak]( 0.08 s)
length_nth_row.......................proved - complete [shostak]( 0.02 s)
columns_cdr_TCC1.....................proved - complete [shostak]( 0.08 s)
columns_cdr..........................proved - complete [shostak]( 0.25 s)
columns_cons.........................proved - complete [shostak]( 0.14 s)
access_col...........................proved - complete [shostak]( 0.16 s)
remove_TCC1..........................proved - complete [shostak]( 0.12 s)
remove_TCC2..........................proved - complete [shostak]( 0.03 s)
remove_TCC3..........................proved - complete [shostak]( 0.02 s)
remove_TCC4..........................proved - complete [shostak]( 0.47 s)
remove_posfullmatrix.................proved - complete [shostak]( 0.19 s)
rows_remove..........................proved - complete [shostak]( 0.16 s)
columns_remove.......................proved - complete [shostak]( 0.76 s)
remove_remove_1_0....................proved - complete [shostak]( 1.65 s)
remove_remove_1_0_0..................proved - complete [shostak]( 1.35 s)
remove_remove_1_n....................proved - complete [shostak]( 1.70 s)
entry_remove.........................proved - complete [shostak]( 0.09 s)
remove_Id_0_0_TCC1...................proved - complete [shostak]( 0.01 s)
remove_Id_0_0........................proved - complete [shostak]( 0.43 s)
remove_test..........................proved - complete [shostak]( 0.03 s)
det_TCC1.............................proved - complete [shostak]( 0.03 s)
det_TCC2.............................proved - complete [shostak]( 0.09 s)
det_test.............................proved - complete [shostak]( 0.67 s)
det_size_noteq.......................proved - complete [shostak]( 0.09 s)
swap_fun_test........................proved - complete [shostak]( 0.02 s)
swap_TCC1............................proved - complete [shostak]( 0.37 s)
entry_swap...........................proved - complete [shostak]( 0.06 s)
swap_test_TCC1.......................proved - complete [shostak]( 0.04 s)
swap_test............................proved - complete [shostak]( 0.02 s)
remove_swap_1........................proved - complete [shostak]( 0.54 s)
remove_swap_2_TCC1...................proved - complete [shostak]( 0.09 s)
remove_swap_2_TCC2...................proved - complete [shostak]( 0.06 s)
remove_swap_2_TCC3...................proved - complete [shostak]( 0.05 s)
remove_swap_2........................proved - complete [shostak]( 1.20 s)
swap_sym.............................proved - complete [shostak]( 0.19 s)
det_swap_0_1.........................proved - complete [shostak](17.25 s)
swap_swap_matrix.....................proved - complete [shostak]( 0.31 s)
swap_similar.........................proved - complete [shostak]( 0.63 s)
det_swap.............................proved - complete [shostak]( 0.21 s)
row_swap.............................proved - complete [shostak]( 0.34 s)
rows_swap............................proved - complete [shostak]( 0.06 s)
columns_swap.........................proved - complete [shostak]( 0.08 s)
swap_id..............................proved - complete [shostak]( 0.16 s)
swap_eq..............................proved - complete [shostak]( 0.11 s)
det_rows_eq_0........................proved - complete [shostak]( 0.06 s)
replace_row_TCC1.....................proved - complete [shostak]( 0.81 s)
replace_row_TCC2.....................proved - complete [shostak]( 0.26 s)
replace_row_TCC3.....................proved - complete [shostak]( 0.10 s)
replace_row_TCC4.....................proved - complete [shostak]( 1.56 s)
replace_row_TCC5.....................proved - complete [shostak]( 0.10 s)
replace_row_TCC6.....................proved - complete [shostak]( 0.28 s)
replace_row_TCC7.....................proved - complete [shostak]( 0.07 s)
replace_row_TCC8.....................proved - complete [shostak]( 0.06 s)
replace_row_TCC9.....................proved - complete [shostak]( 2.14 s)
entry_replace_row....................proved - complete [shostak]( 0.08 s)
rows_replace_row.....................proved - complete [shostak]( 0.07 s)
columns_replace_row..................proved - complete [shostak]( 0.04 s)
remove_replace_row...................proved - complete [shostak]( 0.70 s)
swap_replace_row_TCC1................proved - complete [shostak]( 0.07 s)
swap_replace_row_TCC2................proved - complete [shostak]( 0.06 s)
swap_replace_row_TCC3................proved - complete [shostak]( 0.06 s)
swap_replace_row.....................proved - complete [shostak]( 2.99 s)
row_replace_row......................proved - complete [shostak]( 0.09 s)
remove_replace_row_eq................proved - complete [shostak]( 0.69 s)
det_replace_row_sum_TCC1.............proved - complete [shostak]( 0.03 s)
det_replace_row_sum_TCC2.............proved - complete [shostak]( 0.05 s)
det_replace_row_sum..................proved - complete [shostak]( 8.92 s)
det_replace_row_scal_TCC1............proved - complete [shostak]( 0.05 s)
det_replace_row_scal.................proved - complete [shostak]( 3.50 s)
replace_row_id_TCC1..................proved - complete [shostak]( 0.02 s)
replace_row_id.......................proved - complete [shostak]( 0.16 s)
det_replace_row_sum_scal_TCC1........proved - complete [shostak]( 0.09 s)
det_replace_row_sum_scal.............proved - complete [shostak]( 0.53 s)
replace_row_sum_to_scal_TCC1.........proved - complete [shostak]( 0.08 s)
replace_row_sum_to_scal_TCC2.........proved - complete [shostak]( 0.09 s)
replace_row_sum_to_scal..............proved - complete [shostak]( 0.10 s)
det_Id...............................proved - complete [shostak]( 2.08 s)
det_first_column_zero................proved - complete [shostak]( 0.52 s)
remove_transpose_TCC1................proved - complete [shostak]( 0.07 s)
remove_transpose.....................proved - complete [shostak]( 0.60 s)
Theory totals: 81 formulas, 81 attempted, 81 succeeded (58.37 s)
Proof summary for theory query_coeff
bump_one_ind_TCC1.....................proved - complete [shostak](0.03 s)
bump_one_ind_TCC2.....................proved - complete [shostak](0.06 s)
bump_one_ind_TCC3.....................proved - complete [shostak](0.05 s)
bump_one_ind_TCC4.....................proved - complete [shostak](0.07 s)
bump_one_ind_TCC5.....................proved - complete [shostak](0.06 s)
bump_one_ind_TCC6.....................proved - complete [shostak](0.09 s)
switch_one_entry_TCC1.................proved - complete [shostak](0.04 s)
switch_one_entry_TCC2.................proved - complete [shostak](0.08 s)
switch_one_entry_TCC3.................proved - complete [shostak](0.07 s)
switch_one_entry_TCC4.................proved - complete [shostak](0.05 s)
switch_one_entry_TCC5.................proved - complete [shostak](0.01 s)
switch_one_entry_TCC6.................proved - complete [shostak](0.36 s)
switch_is_with_TCC1...................proved - complete [shostak](0.23 s)
switch_is_with........................proved - complete [shostak](1.96 s)
bump_one_ind_list_TCC1................proved - complete [shostak](0.03 s)
bump_one_ind_list_TCC2................proved - complete [shostak](0.14 s)
bump_one_ind_list_TCC3................proved - complete [shostak](0.06 s)
bump_one_ind_list_TCC4................proved - complete [shostak](0.08 s)
bump_one_ind_list_TCC5................proved - complete [shostak](0.09 s)
bump_one_ind_list_TCC6................proved - complete [shostak](0.07 s)
bump_one_ind_list_TCC7................proved - complete [shostak](0.04 s)
bump_one_ind_list_TCC8................proved - complete [shostak](0.10 s)
bump_one_ind_list_TCC9................proved - complete [shostak](0.12 s)
bump_one_ind_list_TCC10...............proved - complete [shostak](0.09 s)
bump_one_ind_list_TCC11...............proved - complete [shostak](0.05 s)
bump_one_below........................proved - complete [shostak](0.21 s)
bump_one_ind_lem......................proved - complete [shostak](0.76 s)
bump_one_ind_lem2_TCC1................proved - complete [shostak](0.01 s)
bump_one_ind_lem2_TCC2................proved - complete [shostak](0.07 s)
bump_one_ind_lem2_TCC3................proved - complete [shostak](0.00 s)
bump_one_ind_lem2.....................proved - complete [shostak](1.09 s)
low2_TCC1.............................proved - complete [shostak](0.10 s)
low2_TCC2.............................proved - complete [shostak](0.11 s)
low2_lem..............................proved - complete [shostak](0.28 s)
bump_one_prep_TCC1....................proved - complete [shostak](0.00 s)
bump_one_prep.........................proved - complete [shostak](0.71 s)
bump_one_prep2_TCC1...................proved - complete [shostak](0.06 s)
bump_one_prep2_TCC2...................proved - complete [shostak](0.04 s)
bump_one_prep2........................proved - complete [shostak](0.70 s)
bump_one_TCC1.........................proved - complete [shostak](0.01 s)
switch_to_array.......................proved - complete [shostak](0.79 s)
bump_one_list_TCC1....................proved - complete [shostak](0.01 s)
bump_one_list_TCC2....................proved - complete [shostak](-1.10 s)
is_nonzero_TCC1.......................proved - complete [shostak](0.05 s)
dot_tail_sum2plus_TCC1................proved - complete [shostak](0.01 s)
dot_tail_sum2plus_TCC2................proved - complete [shostak](0.17 s)
dot_tail_sum2plus_TCC3................proved - complete [shostak](0.11 s)
dot_tail_sum2plus_TCC4................proved - complete [shostak](0.02 s)
dot_tail_sum2plus_TCC5................proved - complete [shostak](0.20 s)
dot_tail_sum2plus_TCC6................proved - complete [shostak](0.23 s)
dot_tail_sum2plus_TCC7................proved - complete [shostak](0.05 s)
dot_tail_sum2plus_TCC8................proved - complete [shostak](0.17 s)
dot_tail_sum_lem_TCC1.................proved - complete [shostak](0.18 s)
dot_tail_sum_lem......................proved - complete [shostak](1.27 s)
is_nz_TCC1............................proved - complete [shostak](0.04 s)
dot_tail_sum2_TCC1....................proved - complete [shostak](0.02 s)
dot_tail_sum2_TCC2....................proved - complete [shostak](0.05 s)
dot_tail_sum2_TCC3....................proved - complete [shostak](0.04 s)
dot_tail_sum_lem2_TCC1................proved - complete [shostak](0.01 s)
dot_tail_sum_lem2_TCC2................proved - complete [shostak](0.02 s)
dot_tail_sum_lem2_TCC3................proved - complete [shostak](0.01 s)
dot_tail_sum_lem2.....................proved - complete [shostak](0.63 s)
Theory totals: 62 formulas, 62 attempted, 62 succeeded (11.16 s)
Proof summary for theory tensor_product
not_null.............................proved - complete [shostak]( 0.02 s)
mod_int..............................proved - complete [shostak]( 0.30 s)
tensor_fun_TCC1......................proved - complete [shostak]( 0.15 s)
tensor_fun_TCC2......................proved - complete [shostak]( 0.23 s)
tensor_fun_TCC3......................proved - complete [shostak]( 0.02 s)
tensor_fun_TCC4......................proved - complete [shostak]( 0.29 s)
tensor_fun_TCC5......................proved - complete [shostak]( 0.03 s)
tensor_fun_TCC6......................proved - complete [shostak]( 0.03 s)
tensor_prod_TCC1.....................proved - complete [shostak]( 0.40 s)
entry_tensor_prod....................proved - complete [shostak]( 0.17 s)
tensor_rows..........................proved - complete [shostak]( 0.11 s)
tensor_cols..........................proved - complete [shostak]( 0.14 s)
tensor_mult_entry_TCC1...............proved - complete [shostak]( 0.14 s)
tensor_mult_entry_TCC2...............proved - complete [shostak]( 0.26 s)
tensor_mult_entry_TCC3...............proved - complete [shostak]( 0.02 s)
tensor_mult_entry_TCC4...............proved - complete [shostak]( 0.26 s)
tensor_mult_entry_TCC5...............proved - complete [shostak]( 0.04 s)
tensor_mult_entry_TCC6...............proved - complete [shostak]( 0.04 s)
tensor_mult_entry....................proved - complete [shostak]( 5.71 s)
invertible_tensor_TCC1...............proved - complete [shostak]( 0.06 s)
invertible_tensor_TCC2...............proved - complete [shostak]( 0.05 s)
invertible_tensor_TCC3...............proved - complete [shostak]( 0.02 s)
invertible_tensor_TCC4...............proved - complete [shostak]( 0.02 s)
invertible_tensor....................proved - incomplete [shostak]( 7.00 s)
TQMat_TCC1...........................proved - complete [shostak]( 0.02 s)
TQMat_TCC2...........................proved - complete [shostak]( 0.03 s)
TQMat_TCC3...........................proved - complete [shostak]( 1.04 s)
TQMatInv_TCC1........................proved - complete [shostak]( 0.01 s)
TQMatInv_TCC2........................proved - complete [shostak]( 0.06 s)
TQMatInv_TCC3........................proved - complete [shostak]( 0.93 s)
invTQ................................proved - complete [shostak]( 2.42 s)
is_invTQ_TCC1........................proved - complete [shostak]( 2.43 s)
is_invTQ.............................proved - incomplete [shostak]( 1.76 s)
tensor_power_TCC1....................proved - complete [shostak]( 0.02 s)
tensor_power_TCC2....................proved - complete [shostak]( 0.01 s)
invertible_tensor_power_TCC1.........proved - complete [shostak]( 0.31 s)
invertible_tensor_power_TCC2.........proved - complete [shostak]( 0.02 s)
invertible_tensor_power_TCC3.........proved - complete [shostak](12.94 s)
invertible_tensor_power..............proved - incomplete [shostak]( 6.89 s)
tensor_power_rows_TCC1...............proved - complete [shostak]( 0.02 s)
tensor_power_rows....................proved - complete [shostak]( 0.17 s)
tensor_power_columns_TCC1............proved - complete [shostak]( 0.01 s)
tensor_power_columns.................proved - complete [shostak]( 0.30 s)
mod_eq_lem_alt_TCC1..................proved - complete [shostak]( 0.10 s)
mod_eq_lem_alt.......................proved - complete [shostak]( 0.29 s)
tensor_prod_assoc....................proved - complete [shostak]( 5.43 s)
power_assoc..........................proved - complete [shostak]( 0.39 s)
tensor_power_rows_alt................proved - complete [shostak]( 0.02 s)
tensor_power_columns_alt.............proved - complete [shostak]( 0.03 s)
TQXL_TCC1............................proved - complete [shostak]( 0.02 s)
TQXL_TCC2............................proved - complete [shostak]( 0.01 s)
TQXL_TCC3............................proved - complete [shostak]( 0.07 s)
TQXLinv_TCC1.........................proved - complete [shostak]( 0.01 s)
TQXLinv_TCC2.........................proved - complete [shostak]( 0.02 s)
TQXLinv_TCC3.........................proved - complete [shostak]( 0.07 s)
invTQXL..............................proved - complete [shostak]( 0.25 s)
is_invTQXL_TCC1......................proved - complete [shostak]( 0.00 s)
is_invTQXL_TCC2......................proved - incomplete [shostak]( 0.00 s)
is_invTQXL...........................proved - incomplete [shostak]( 0.38 s)
RowToMat_TCC1........................proved - complete [shostak]( 0.19 s)
RtM..................................proved - complete [shostak]( 0.02 s)
RowToMat_rows........................proved - complete [shostak]( 0.06 s)
RowToMat_columns.....................proved - complete [shostak]( 0.12 s)
RowToMat_entry.......................proved - complete [shostak]( 0.33 s)
RowToMat_tensor_prod_TCC1............proved - complete [shostak]( 0.07 s)
RowToMat_tensor_prod_TCC2............proved - complete [shostak]( 0.10 s)
RowToMat_tensor_prod_TCC3............proved - complete [shostak]( 0.12 s)
RowToMat_tensor_prod_TCC4............proved - complete [shostak]( 0.03 s)
RowToMat_tensor_prod.................proved - complete [shostak]( 6.30 s)
RowTensor_TCC1.......................proved - complete [shostak]( 0.04 s)
RowTensor_TCC2.......................proved - complete [shostak]( 0.03 s)
RowTensor_TCC3.......................proved - complete [shostak]( 0.07 s)
RowTensors_same_TCC1.................proved - complete [shostak]( 0.07 s)
RowTensors_same_TCC2.................proved - complete [shostak]( 0.02 s)
RowTensors_same......................proved - complete [shostak]( 1.08 s)
RowTensor_is_TensorRow_TCC1..........proved - complete [shostak]( 0.04 s)
RowTensor_is_TensorRow...............proved - complete [shostak](-0.33 s)
RowTensor_is_TensorRow2_TCC1.........proved - complete [shostak]( 0.05 s)
RowTensor_is_TensorRow2..............proved - complete [shostak]( 0.07 s)
tensor_entry_TCC1....................proved - complete [shostak]( 0.10 s)
tensor_entry_TCC2....................proved - complete [shostak]( 0.02 s)
tensor_entry_TCC3....................proved - complete [shostak]( 0.01 s)
tensor_entry_TCC4....................proved - complete [shostak]( 0.10 s)
tensor_entry_TCC5....................proved - complete [shostak]( 0.02 s)
tensor_entry_TCC6....................proved - complete [shostak]( 0.12 s)
tensor_entry.........................proved - complete [shostak]( 3.27 s)
tensor_entry_alt.....................proved - complete [shostak]( 0.00 s)
Theory totals: 87 formulas, 87 attempted, 87 succeeded (64.12 s)
Proof summary for theory linear_dependence
zerow_TCC1............................proved - complete [shostak](0.63 s)
zerow_dim.............................proved - complete [shostak](0.29 s)
zecolumn_dim..........................proved - complete [shostak](0.03 s)
row2mat_TCC1..........................proved - complete [shostak](0.42 s)
row2mat_dim...........................proved - complete [shostak](0.41 s)
sum_rows_TCC1.........................proved - complete [shostak](1.02 s)
sum_rows_TCC2.........................proved - complete [shostak](0.05 s)
sum_rows_TCC3.........................proved - complete [shostak](1.02 s)
sum_rows_TCC4.........................proved - complete [shostak](0.01 s)
sum_rows_TCC5.........................proved - complete [shostak](0.04 s)
sum_rows_TCC6.........................proved - complete [shostak](0.01 s)
sum_rows_eq...........................proved - complete [shostak](0.40 s)
sum_rows_add_start_TCC1...............proved - complete [shostak](0.50 s)
sum_rows_add_start....................proved - complete [shostak](1.90 s)
subtract_same_scal....................proved - complete [shostak](0.71 s)
sum_lem_prep_TCC1.....................proved - complete [shostak](0.08 s)
sum_lem_prep..........................proved - complete [shostak](2.57 s)
sum_lem...............................proved - complete [shostak](0.10 s)
row_dependence_lem....................proved - complete [shostak](1.39 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (11.57 s)
Grand Totals: 541 proofs, 541 attempted, 541 succeeded (362.10 s)
[ Dauer der Verarbeitung: 1.261 Sekunden
]
