| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[397] Hlasm[1603] Haskell[1923]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (20:36:40 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 sigma_lemmas sigma_restrict_dom_TCC1...............proved - complete [shostak](0.07 s) sigma_restrict_dom_TCC2...............proved - complete [shostak](0.01 s) sigma_restrict_dom_TCC3...............proved - complete [shostak](0.04 s) sigma_restrict_dom_TCC4...............proved - complete [shostak](0.04 s) sigma_restrict_dom_TCC5...............proved - complete [shostak](0.01 s) sigma_restrict_dom_TCC6...............proved - complete [shostak](0.05 s) sigma_restrict_dom_TCC7...............proved - complete [shostak](0.06 s) sigma_restrict_dom....................proved - complete [shostak](0.35 s) sigma_restrict_dom2_TCC1..............proved - complete [shostak](0.03 s) sigma_restrict_dom2_TCC2..............proved - complete [shostak](0.02 s) sigma_restrict_dom2_TCC3..............proved - complete [shostak](0.04 s) sigma_restrict_dom2_TCC4..............proved - complete [shostak](0.01 s) sigma_restrict_dom2_TCC5..............proved - complete [shostak](0.04 s) sigma_restrict_dom2_TCC6..............proved - complete [shostak](0.06 s) sigma_restrict_dom2...................proved - complete [shostak](0.59 s) sigma_below_shift_TCC1................proved - complete [shostak](0.01 s) sigma_below_shift_TCC2................proved - complete [shostak](0.00 s) sigma_below_shift_TCC3................proved - complete [shostak](0.05 s) sigma_below_shift_TCC4................proved - complete [shostak](0.01 s) sigma_below_shift_TCC5................proved - complete [shostak](0.00 s) sigma_below_shift_TCC6................proved - complete [shostak](0.01 s) sigma_below_shift_TCC7................proved - complete [shostak](0.03 s) sigma_below_shift.....................proved - complete [shostak](0.59 s) sigma_eq_index_TCC1...................proved - complete [shostak](0.02 s) sigma_eq_index_TCC2...................proved - complete [shostak](0.01 s) sigma_eq_index_TCC3...................proved - complete [shostak](0.01 s) sigma_eq_index........................proved - complete [shostak](0.82 s) aux_sigma_TCC1........................proved - complete [shostak](0.00 s) aux_sigma_TCC2........................proved - complete [shostak](0.01 s) aux_sigma_TCC3........................proved - complete [shostak](0.04 s) aux_sigma.............................proved - complete [shostak](1.07 s) aux_sigma2_TCC1.......................proved - complete [shostak](0.03 s) aux_sigma2_TCC2.......................proved - complete [shostak](0.08 s) aux_sigma2............................proved - complete [shostak](0.57 s) sigma_restrict_gen_TCC1...............proved - complete [shostak](0.01 s) sigma_restrict_gen_TCC2...............proved - complete [shostak](0.03 s) sigma_restrict_gen_TCC3...............proved - complete [shostak](0.01 s) sigma_restrict_gen_TCC4...............proved - complete [shostak](-.76 s) sigma_restrict_gen....................proved - complete [shostak](1.05 s) sigma_eq_index2_TCC1..................proved - complete [shostak](0.03 s) sigma_eq_index2_TCC2..................proved - complete [shostak](0.04 s) sigma_eq_index2.......................proved - complete [shostak](0.62 s) sigma_restrict_gen2_TCC1..............proved - complete [shostak](0.04 s) sigma_restrict_gen2_TCC2..............proved - complete [shostak](0.06 s) sigma_restrict_gen2...................proved - complete [shostak](0.19 s) sigma_eq_index3_TCC1..................proved - complete [shostak](0.03 s) sigma_eq_index3_TCC2..................proved - complete [shostak](0.04 s) sigma_eq_index3.......................proved - complete [shostak](0.20 s) sigma_shift_gen_TCC1..................proved - complete [shostak](0.02 s) sigma_shift_gen_TCC2..................proved - complete [shostak](0.01 s) sigma_shift_gen_TCC3..................proved - complete [shostak](0.01 s) sigma_shift_gen_TCC4..................proved - complete [shostak](0.06 s) sigma_shift_gen.......................proved - complete [shostak](1.01 s) Theory totals: 53 formulas, 53 attempted, 53 succeeded (7.47 s) Proof summary for theory linear_map plus_TCC1.............................proved - complete [shostak](0.03 s) plus_TCC2.............................proved - complete [shostak](0.02 s) oh_TCC1...............................proved - complete [shostak](0.02 s) bijective?_TCC1.......................proved - complete [shostak](0.03 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.10 s) Proof summary for theory sigma_vector low_TCC1..............................proved - complete [shostak](0.01 s) oh_TCC1...............................proved - complete [shostak](0.02 s) oh_TCC2...............................proved - complete [shostak](0.02 s) SigmaV_last_TCC1......................proved - complete [shostak](0.11 s) SigmaV_last_TCC2......................proved - complete [shostak](0.04 s) SigmaV_last...........................proved - complete [shostak](0.09 s) SigmaV_scal...........................proved - complete [shostak](0.11 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.40 s) Proof summary for theory linear_map_def vec_expan?_TCC1.......................proved - complete [shostak](0.00 s) vec_expan?_TCC2.......................proved - complete [shostak](0.01 s) vec_expan?_TCC3.......................proved - complete [shostak](0.02 s) vec_repre_bases.......................proved - complete [shostak](0.45 s) cano_base.............................proved - complete [shostak](0.84 s) linear_map_e?_TCC1....................proved - complete [shostak](0.00 s) linear_map_e?_TCC2....................proved - complete [shostak](0.00 s) linear_map_e?_TCC3....................proved - complete [shostak](0.04 s) linear_map_e?_TCC4....................proved - complete [shostak](0.03 s) linear_map_e?_TCC5....................proved - complete [shostak](0.03 s) linear_map_e?_TCC6....................proved - complete [shostak](0.03 s) linear_map_e_comp_TCC1................proved - complete [shostak](0.04 s) linear_map_e_comp.....................proved - complete [shostak](0.85 s) bijecti_fun_equa......................proved - complete [shostak](0.02 s) equa_basis_n_TCC1.....................proved - complete [shostak](0.07 s) equa_basis_n_TCC2.....................proved - complete [shostak](0.08 s) equa_basis_n_TCC3.....................proved - complete [shostak](0.08 s) equa_basis_n..........................proved - complete [shostak](0.80 s) linear_map_characterization...........proved - complete [shostak](3.62 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (7.01 s) Proof summary for theory vect_of_vect Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory matrices Mr2V_TCC1.............................proved - complete [shostak](0.01 s) Mc2V_TCC1.............................proved - complete [shostak](0.01 s) transpose2............................proved - complete [shostak](0.05 s) identity?_TCC1........................proved - complete [shostak](0.02 s) I_TCC1................................proved - complete [shostak](0.01 s) ident_trans...........................proved - complete [shostak](0.09 s) plus_TCC1.............................proved - complete [shostak](0.01 s) plus_TCC2.............................proved - complete [shostak](0.00 s) plus_assoc_TCC1.......................proved - complete [shostak](0.01 s) plus_assoc_TCC2.......................proved - complete [shostak](0.01 s) plus_assoc_TCC3.......................proved - complete [shostak](0.01 s) plus_assoc............................proved - complete [shostak](0.06 s) plus_comm_TCC1........................proved - complete [shostak](0.01 s) plus_comm.............................proved - complete [shostak](0.16 s) zero_left_ident.......................proved - complete [shostak](0.17 s) zero_right_ident_TCC1.................proved - complete [shostak](0.00 s) zero_right_ident......................proved - complete [shostak](0.14 s) times_TCC1............................proved - complete [shostak](0.02 s) times_TCC2............................proved - complete [shostak](0.04 s) times_TCC3............................proved - complete [shostak](0.00 s) times_TCC4............................proved - complete [shostak](0.04 s) times_TCC5............................proved - complete [shostak](0.02 s) times_TCC6............................proved - complete [shostak](0.02 s) zero_times_left_TCC1..................proved - complete [shostak](0.00 s) zero_times_left.......................proved - complete [shostak](0.49 s) zero_times_right_TCC1.................proved - complete [shostak](0.01 s) zero_times_right......................proved - complete [shostak](0.43 s) sigma_lem_TCC1........................proved - complete [shostak](0.01 s) sigma_lem_TCC2........................proved - complete [shostak](0.01 s) sigma_lem_TCC3........................proved - complete [shostak](0.03 s) sigma_lem.............................proved - complete [shostak](0.14 s) right_mult_ident......................proved - complete [shostak](0.38 s) left_mult_ident_TCC1..................proved - complete [shostak](0.00 s) left_mult_ident.......................proved - complete [shostak](0.61 s) ident_vect_TCC1.......................proved - complete [shostak](0.12 s) ident_vect............................proved - complete [shostak](0.57 s) sigma_prop_TCC1.......................proved - complete [shostak](0.01 s) sigma_prop_TCC2.......................proved - complete [shostak](0.00 s) sigma_prop_TCC3.......................proved - complete [shostak](0.01 s) sigma_prop_TCC4.......................proved - complete [shostak](0.01 s) sigma_prop............................proved - complete [shostak](0.61 s) sigma_comm_TCC1.......................proved - complete [shostak](0.01 s) sigma_comm_TCC2.......................proved - complete [shostak](0.00 s) sigma_comm............................proved - complete [shostak](0.32 s) mult_assoc_TCC1.......................proved - complete [shostak](0.04 s) mult_assoc_TCC2.......................proved - complete [shostak](0.03 s) mult_assoc............................proved - complete [shostak](0.82 s) mult_assoc_vect_TCC1..................proved - complete [shostak](0.03 s) mult_assoc_vect_TCC2..................proved - complete [shostak](0.02 s) mult_assoc_vect_TCC3..................proved - complete [shostak](0.04 s) mult_assoc_vect.......................proved - complete [shostak](1.04 s) left_distributive_TCC1................proved - complete [shostak](0.02 s) left_distributive_TCC2................proved - complete [shostak](0.00 s) left_distributive_TCC3................proved - complete [shostak](0.06 s) left_distributive.....................proved - complete [shostak](0.60 s) right_distributive_TCC1...............proved - complete [shostak](0.01 s) right_distributive_TCC2...............proved - complete [shostak](0.00 s) right_distributive_TCC3...............proved - complete [shostak](0.07 s) right_distributive....................proved - complete [shostak](1.00 s) left_distributive_vect................proved - complete [shostak](0.39 s) transpose_product_TCC1................proved - complete [shostak](0.01 s) transpose_product.....................proved - complete [shostak](0.93 s) trans_mat_scal_TCC1...................proved - complete [shostak](0.01 s) trans_mat_scal_TCC2...................proved - complete [shostak](0.01 s) trans_mat_scal........................proved - complete [shostak](1.81 s) inverse?_TCC1.........................proved - complete [shostak](0.02 s) inverse?_TCC2.........................proved - complete [shostak](0.06 s) inverse_unique........................proved - complete [shostak](0.07 s) inverse_TCC1..........................proved - complete [shostak](0.19 s) invertible_product_TCC1...............proved - complete [shostak](0.05 s) invertible_product....................proved - complete [shostak](0.32 s) product_inverse_TCC1..................proved - complete [shostak](1.52 s) product_inverse_TCC2..................proved - complete [shostak](0.83 s) product_inverse.......................proved - complete [shostak](0.74 s) trace_TCC1............................proved - complete [shostak](0.01 s) trace_TCC2............................proved - complete [shostak](0.02 s) trace_TCC3............................proved - complete [shostak](0.02 s) symmetric_part_TCC1...................proved - complete [shostak](0.02 s) symmetric_part_TCC2...................proved - complete [shostak](0.21 s) skew_symmetric_part_TCC1..............proved - complete [shostak](0.25 s) square_decomp_TCC1....................proved - complete [shostak](0.04 s) square_decomp.........................proved - complete [shostak](0.11 s) square_matrix_induct..................proved - complete [shostak](0.02 s) semidef_pos?_TCC1.....................proved - complete [shostak](0.02 s) Theory totals: 84 formulas, 84 attempted, 84 succeeded (16.12 s) Proof summary for theory matrix_operator linear_inverse_map_n..................proved - complete [shostak](4.06 s) linear_comp_TCC1......................proved - complete [shostak](0.01 s) linear_comp...........................proved - complete [shostak](0.38 s) linear_matrix_TCC1....................proved - complete [shostak](0.01 s) linear_matrix_TCC2....................proved - complete [shostak](0.01 s) linear_matrix_TCC3....................proved - complete [shostak](0.04 s) linear_matrix_TCC4....................proved - complete [shostak](0.03 s) linear_matrix.........................proved - complete [shostak](0.54 s) equa_inv_TCC1.........................proved - complete [shostak](0.01 s) equa_inv_TCC2.........................proved - complete [shostak](0.05 s) equa_inv_TCC3.........................proved - complete [shostak](0.01 s) equa_inv_TCC4.........................proved - complete [shostak](0.07 s) equa_inv..............................proved - complete [shostak](0.26 s) inv_uni...............................proved - complete [shostak](1.04 s) L_TCC1................................proved - complete [shostak](0.01 s) L_TCC2................................proved - complete [shostak](0.05 s) T_TCC1................................proved - complete [shostak](0.01 s) T_TCC2................................proved - complete [shostak](0.01 s) T_TCC3................................proved - complete [shostak](0.01 s) T_TCC4................................proved - complete [shostak](0.01 s) T_TCC5................................proved - complete [shostak](0.04 s) T_TCC6................................proved - complete [shostak](0.57 s) T_matr_TCC1...........................proved - complete [shostak](0.03 s) T_matr_TCC2...........................proved - complete [shostak](0.02 s) T_matr_TCC3...........................proved - complete [shostak](0.06 s) T_matr................................proved - complete [shostak](0.19 s) linear_map_T..........................proved - complete [shostak](0.66 s) map_matrix_bij........................proved - complete [shostak](1.32 s) operator_TCC1.........................proved - complete [shostak](0.01 s) operator_TCC2.........................proved - complete [shostak](0.01 s) operator..............................proved - complete [shostak](0.04 s) Iso...................................proved - complete [shostak](0.25 s) iso_map...............................proved - complete [shostak](0.03 s) L_inverse_TCC1........................proved - complete [shostak](0.23 s) L_inverse.............................proved - complete [shostak](0.05 s) Iso_T.................................proved - complete [shostak](0.18 s) mult_comp_TCC1........................proved - complete [shostak](0.01 s) mult_comp_TCC2........................proved - complete [shostak](0.04 s) mult_comp_TCC3........................proved - complete [shostak](0.07 s) mult_comp.............................proved - complete [shostak](0.96 s) comp_mult_TCC1........................proved - complete [shostak](0.04 s) comp_mult_TCC2........................proved - complete [shostak](0.03 s) comp_mult.............................proved - complete [shostak](-.58 s) iso_ide_L_TCC1........................proved - complete [shostak](0.15 s) iso_ide_L.............................proved - complete [shostak](0.15 s) iso_ide_T_TCC1........................proved - complete [shostak](0.01 s) iso_ide_T.............................proved - complete [shostak](1.03 s) Matrix_inv_TCC1.......................proved - complete [shostak](0.02 s) inverse_invertible_TCC1...............proved - complete [shostak](0.02 s) inverse_invertible_TCC2...............proved - complete [shostak](0.10 s) inverse_invertible_TCC3...............proved - complete [shostak](0.18 s) inverse_invertible....................proved - complete [shostak](0.34 s) inv_TCC1..............................proved - complete [shostak](0.01 s) inv_TCC2..............................proved - complete [shostak](0.10 s) inv_TCC3..............................proved - complete [shostak](0.15 s) iso_inv_TCC1..........................proved - complete [shostak](0.19 s) iso_inv_TCC2..........................proved - complete [shostak](0.22 s) iso_inv_TCC3..........................proved - complete [shostak](0.29 s) iso_inv...............................proved - complete [shostak](4.00 s) inv_TCC4..............................proved - complete [shostak](0.22 s) inv...................................proved - complete [shostak](0.03 s) bijec_prod_TCC1.......................proved - complete [shostak](0.36 s) bijec_prod_TCC2.......................proved - complete [shostak](0.38 s) bijec_prod............................proved - complete [shostak](0.89 s) map_matrix_bij_inv_TCC1...............proved - complete [shostak](0.08 s) map_matrix_bij_inv....................proved - complete [shostak](3.10 s) tran_inv_TCC1.........................proved - complete [shostak](0.01 s) tran_inv_TCC2.........................proved - complete [shostak](0.24 s) tran_inv_TCC3.........................proved - complete [shostak](0.18 s) tran_inv..............................proved - complete [shostak](3.62 s) bijec_transpose_TCC1..................proved - complete [shostak](0.19 s) bijec_transpose.......................proved - complete [shostak](0.54 s) tran_inv_oper_TCC1....................proved - complete [shostak](0.33 s) tran_inv_oper.........................proved - complete [shostak](1.15 s) prod_inv_TCC1.........................proved - complete [shostak](0.20 s) prod_inv_TCC2.........................proved - complete [shostak](0.34 s) prod_inv_TCC3.........................proved - complete [shostak](0.35 s) prod_inv_TCC4.........................proved - complete [shostak](0.52 s) prod_inv_TCC5.........................proved - complete [shostak](0.37 s) prod_inv_TCC6.........................proved - complete [shostak](0.37 s) prod_inv..............................proved - complete [shostak](7.02 s) prod_inv_oper_TCC1....................proved - complete [shostak](0.55 s) prod_inv_oper.........................proved - complete [shostak](0.81 s) equa_sol_TCC1.........................proved - complete [shostak](0.02 s) equa_sol_TCC2.........................proved - complete [shostak](0.02 s) equa_sol_TCC3.........................proved - complete [shostak](0.02 s) equa_sol_TCC4.........................proved - complete [shostak](0.19 s) equa_sol_TCC5.........................proved - complete [shostak](0.20 s) equa_sol..............................proved - complete [shostak](1.14 s) Theory totals: 89 formulas, 89 attempted, 89 succeeded (41.22 s) Proof summary for theory matrix_lemmas matrix_prod_zero......................proved - complete [shostak](0.07 s) minus_rows............................proved - complete [shostak](0.02 s) minus_cols............................proved - complete [shostak](0.01 s) transpose_rows........................proved - complete [shostak](0.01 s) transpose_cols........................proved - complete [shostak](0.02 s) product_rows_TCC1.....................proved - complete [shostak](0.00 s) product_rows..........................proved - complete [shostak](0.05 s) product_cols..........................proved - complete [shostak](0.05 s) product_rows2_TCC1....................proved - complete [shostak](0.03 s) product_rows2.........................proved - complete [shostak](0.01 s) product_cols2.........................proved - complete [shostak](0.01 s) product_rows3_TCC1....................proved - complete [shostak](0.10 s) product_rows3.........................proved - complete [shostak](0.02 s) product_cols3.........................proved - complete [shostak](0.01 s) product_rows4_TCC1....................proved - complete [shostak](0.22 s) product_rows4.........................proved - complete [shostak](0.02 s) product_cols4.........................proved - complete [shostak](0.02 s) inverse_ident_TCC1....................proved - complete [shostak](0.39 s) inverse_ident.........................proved - complete [shostak](0.05 s) ident_inverse_TCC1....................proved - complete [shostak](0.39 s) ident_inverse.........................proved - complete [shostak](0.05 s) ident_mat_prod_TCC1...................proved - complete [shostak](0.01 s) ident_mat_prod_TCC2...................proved - complete [shostak](0.01 s) ident_mat_prod........................proved - complete [shostak](0.54 s) inverse_rows..........................proved - complete [shostak](0.60 s) inverse_cols..........................proved - complete [shostak](0.35 s) transp_ident..........................proved - complete [shostak](0.10 s) transp_inv_TCC1.......................proved - complete [shostak](1.44 s) transp_inv............................proved - complete [shostak](1.38 s) invar_inverse_TCC1....................proved - complete [shostak](0.46 s) invar_inverse.........................proved - complete [shostak](0.03 s) invar_inverse_left_TCC1...............proved - complete [shostak](0.79 s) invar_inverse_left....................proved - complete [shostak](0.04 s) simply1_mat_vect_TCC1.................proved - complete [shostak](1.69 s) simply1_mat_vect_TCC2.................proved - complete [shostak](0.48 s) simply1_mat_vect......................proved - complete [shostak](0.02 s) simply2_mat_vect_TCC1.................proved - complete [shostak](0.49 s) simply2_mat_vect_TCC2.................proved - complete [shostak](0.38 s) simply2_mat_vect_TCC3.................proved - complete [shostak](1.18 s) simply2_mat_vect......................proved - complete [shostak](0.03 s) distr_mat_vect_TCC1...................proved - complete [shostak](0.02 s) distr_mat_vect_TCC2...................proved - complete [shostak](0.02 s) distr_mat_vect_TCC3...................proved - complete [shostak](0.02 s) distr_mat_vect_TCC4...................proved - complete [shostak](0.01 s) distr_mat_vect........................proved - complete [shostak](0.82 s) distr_vect_mat........................proved - complete [shostak](0.34 s) matrix_sum_minus_TCC1.................proved - complete [shostak](0.01 s) matrix_sum_minus......................proved - complete [shostak](0.09 s) matrix_prod_minus_TCC1................proved - complete [shostak](0.01 s) matrix_prod_minus_TCC2................proved - complete [shostak](0.01 s) matrix_prod_minus.....................proved - complete [shostak](0.29 s) distr_esc_add_TCC1....................proved - complete [shostak](0.02 s) distr_esc_add.........................proved - complete [shostak](0.05 s) distr_esc_dif_TCC1....................proved - complete [shostak](0.02 s) distr_esc_dif_TCC2....................proved - complete [shostak](0.01 s) distr_esc_dif.........................proved - complete [shostak](0.87 s) distr_add_esc_TCC1....................proved - complete [shostak](0.02 s) distr_add_esc.........................proved - complete [shostak](0.37 s) conv_prod_int_TCC1....................proved - complete [shostak](0.04 s) conv_prod_int_TCC2....................proved - complete [shostak](0.10 s) conv_prod_int_TCC3....................proved - complete [shostak](0.10 s) conv_prod_int_TCC4....................proved - complete [shostak](0.01 s) conv_prod_int_TCC5....................proved - complete [shostak](0.02 s) conv_prod_int_TCC6....................proved - complete [shostak](0.03 s) conv_prod_int.........................proved - complete [shostak](0.20 s) Theory totals: 65 formulas, 65 attempted, 65 succeeded (15.06 s) Proof summary for theory block_matrices Block2M1_TCC1.........................proved - complete [shostak](0.04 s) Block2M1_TCC2.........................proved - complete [shostak](0.05 s) Block2M2_TCC1.........................proved - complete [shostak](0.00 s) Block2M2_TCC2.........................proved - complete [shostak](0.05 s) Block2M3_TCC1.........................proved - complete [shostak](0.04 s) Block2M3_TCC2.........................proved - complete [shostak](0.01 s) Block2M4_TCC1.........................proved - complete [shostak](0.01 s) Block2M4_TCC2.........................proved - complete [shostak](0.00 s) M2Block_TCC1..........................proved - complete [shostak](0.07 s) M2Block_TCC2..........................proved - complete [shostak](0.13 s) M2Block_TCC3..........................proved - complete [shostak](0.14 s) M2Block_TCC4..........................proved - complete [shostak](0.06 s) M2Block_TCC5..........................proved - complete [shostak](0.13 s) M2Block_TCC6..........................proved - complete [shostak](0.14 s) BV1toBV2_TCC1.........................proved - complete [shostak](0.04 s) BV1toBV2_TCC2.........................proved - complete [shostak](0.00 s) BV2toBV1_TCC1.........................proved - complete [shostak](0.05 s) V2Block_TCC1..........................proved - complete [shostak](0.05 s) times_TCC1............................proved - complete [shostak](0.03 s) times_TCC2............................proved - complete [shostak](0.02 s) times_TCC3............................proved - complete [shostak](0.04 s) times_TCC4............................proved - complete [shostak](0.04 s) times_TCC5............................proved - complete [shostak](0.02 s) times_TCC6............................proved - complete [shostak](0.01 s) times_TCC7............................proved - complete [shostak](0.04 s) times_TCC8............................proved - complete [shostak](0.04 s) times_TCC9............................proved - complete [shostak](0.02 s) times_TCC10...........................proved - complete [shostak](0.01 s) plus_TCC1.............................proved - complete [shostak](0.09 s) plus_TCC2.............................proved - complete [shostak](0.09 s) conv_transp_TCC1......................proved - complete [shostak](0.02 s) conv_transp_TCC2......................proved - complete [shostak](0.01 s) conv_transp_TCC3......................proved - complete [shostak](0.01 s) conv_transp_TCC4......................proved - complete [shostak](0.02 s) conv_transp...........................proved - complete [shostak](0.30 s) block_square..........................proved - complete [shostak](0.06 s) block_symmetric.......................proved - complete [shostak](3.97 s) block_symmetric2......................proved - complete [shostak](2.12 s) blockV_equal_TCC1.....................proved - complete [shostak](0.05 s) blockV_equal..........................proved - complete [shostak](0.13 s) VtoBlocktoV1_TCC1.....................proved - complete [shostak](0.01 s) VtoBlocktoV1..........................proved - complete [shostak](0.03 s) VtoBlocktoV2_TCC1.....................proved - complete [shostak](0.01 s) VtoBlocktoV2..........................proved - complete [shostak](0.03 s) VtoBlocktoV_TCC1......................proved - complete [shostak](0.01 s) VtoBlocktoV...........................proved - complete [shostak](0.02 s) Vec_block_Vec_TCC1....................proved - complete [shostak](0.01 s) Vec_block_Vec.........................proved - complete [shostak](0.04 s) block_Vec_block.......................proved - complete [shostak](0.06 s) block_product_TCC1....................proved - complete [shostak](0.07 s) block_product_TCC2....................proved - complete [shostak](0.29 s) block_product.........................proved - complete [shostak](8.72 s) Block2V_product.......................proved - complete [shostak](0.50 s) Theory totals: 53 formulas, 53 attempted, 53 succeeded (17.93 s) Grand Totals: 374 proofs, 374 attempted, 374 succeeded (105.30 s) [ Dauer der Verarbeitung: 0.176 Sekunden ] |