Untersuchungsergebnis.summary Download desMT940 {MT940[703] Hlasm[1139] Haskell[1519]}zum Wurzelverzeichnis wechseln
***
*** top (18:48: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 real_order
real_ord_ep_well_founded..............proved - complete [shostak](0.17 s)
real_ord_ep_decreases_halves..........proved - complete [shostak](0.20 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.37 s)
Proof summary for theory system_solvers
rows_fun_TCC1.........................proved - complete [shostak](0.11 s)
entry_fun_TCC1........................proved - complete [shostak](0.01 s)
entry_fun_TCC2........................proved - complete [shostak](0.07 s)
entry_fun_TCC3........................proved - complete [shostak](0.07 s)
entry_is..............................proved - complete [shostak](0.56 s)
TQlist_fun_TCC1.......................proved - complete [shostak](0.02 s)
TQlist_fun_TCC2.......................proved - complete [shostak](0.87 s)
TQlist_lem_TCC1.......................proved - complete [shostak](0.03 s)
TQlist_lem............................proved - complete [shostak](0.25 s)
sturm_tarski_faster_TCC1..............proved - complete [shostak](0.07 s)
sturm_tarski_faster_TCC2..............proved - complete [shostak](0.06 s)
sturm_tarski_faster_TCC3..............proved - complete [shostak](0.29 s)
sturm_tarski_faster_TCC4..............proved - incomplete [shostak](1.24 s)
Test1_TCC1............................proved - complete [shostak](0.44 s)
Test1_TCC2............................proved - complete [shostak](0.42 s)
Test2recurse_TCC1.....................proved - complete [shostak](0.06 s)
Test2recurse_TCC2.....................proved - complete [shostak](0.07 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (4.65 s)
Proof summary for theory poly_systems
system_roots_enum.....................proved - complete [shostak](1.19 s)
strict_poly_system_solvable_TCC1......proved - complete [shostak](0.03 s)
strict_poly_system_solvable_TCC2......proved - complete [shostak](0.05 s)
strict_poly_system_solvable...........proved - complete [shostak](4.62 s)
A63_tensor_power_mat_row_TCC1.........proved - complete [shostak](0.04 s)
A63_tensor_power_mat_row_TCC2.........proved - complete [shostak](-1.54 s)
A63_tensor_power_mat_row_TCC3.........proved - complete [shostak](0.02 s)
A63_tensor_power_mat_row_TCC4.........proved - complete [shostak](0.01 s)
A63_tensor_power_mat_row_TCC5.........proved - complete [shostak](0.04 s)
A63_tensor_power_mat_row_TCC6.........proved - complete [shostak](0.57 s)
A63_tensor_power_mat_row_def_TCC1.....proved - complete [shostak](0.12 s)
A63_tensor_power_mat_row_def..........proved - complete [shostak](6.24 s)
sturm_tarski_solver_slow_basic_TCC1...proved - incomplete [shostak](1.67 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (13.06 s)
Proof summary for theory tarski_query_matrix
TQ_vect3k_TCC1........................proved - complete [shostak](0.46 s)
TQ_vect3k_TCC2........................proved - complete [shostak](0.08 s)
TQ_vect6k_TCC1........................proved - complete [shostak](0.13 s)
TQ_vect6k_TCC2........................proved - complete [shostak](0.13 s)
NSol_vect3k_TCC1......................proved - complete [shostak](0.04 s)
NSol_vect3k_TCC2......................proved - complete [shostak](0.07 s)
NSol_vect6k_TCC1......................proved - complete [shostak](0.05 s)
NSol_vect6k_TCC2......................proved - complete [shostak](0.11 s)
A66_inv_TCC1..........................proved - complete [shostak](0.05 s)
A66_inv_TCC2..........................proved - complete [shostak](0.11 s)
A66_inv_TCC3..........................proved - complete [shostak](0.07 s)
A66_TCC1..............................proved - complete [shostak](0.11 s)
A66_TCC2..............................proved - complete [shostak](0.05 s)
A66_TCC3..............................proved - complete [shostak](0.14 s)
A66_TCC4..............................proved - incomplete [shostak](0.49 s)
multi_sturm_tarski_6by6...............proved - complete [shostak](5.68 s)
multi_sturm_tarski_NSol...............proved - incomplete [shostak](1.70 s)
A63_TCC1..............................proved - complete [shostak](0.02 s)
A63_TCC2..............................proved - complete [shostak](0.01 s)
A63_TCC3..............................proved - complete [shostak](0.06 s)
A63_def...............................proved - incomplete [shostak](0.01 s)
multi_sturm_tarski_NSol63.............proved - incomplete [shostak](7.63 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (17.20 s)
Proof summary for theory tarski_query
NSol_squared_gt......................proved - complete [shostak]( 0.13 s)
NSol_squared_lt......................proved - complete [shostak]( 0.10 s)
NSol_poly1_lt........................proved - complete [shostak]( 0.05 s)
A3_TCC1..............................proved - complete [shostak]( 0.04 s)
A3_TCC2..............................proved - complete [shostak]( 0.08 s)
A3_TCC3..............................proved - complete [shostak]( 1.14 s)
A3_inv_TCC1..........................proved - complete [shostak]( 0.02 s)
A3_inv_TCC2..........................proved - complete [shostak]( 0.04 s)
A3_inv_TCC3..........................proved - complete [shostak]( 0.05 s)
A3_inv_TCC4..........................proved - incomplete [shostak]( 3.52 s)
TQ_vect3_TCC1........................proved - complete [shostak]( 0.01 s)
TQ_vect3_TCC2........................proved - complete [shostak]( 0.38 s)
TQ_vect3_TCC3........................proved - complete [shostak]( 0.10 s)
TQ_vect3_TCC4........................proved - complete [shostak]( 1.13 s)
NSol_vect3_TCC1......................proved - complete [shostak]( 0.82 s)
tarski_query_system_basic_3..........proved - complete [shostak]( 5.43 s)
A6_TCC1..............................proved - complete [shostak]( 0.11 s)
A6_TCC2..............................proved - complete [shostak]( 2.33 s)
NSol_vect6_TCC1......................proved - complete [shostak]( 1.75 s)
tarski_query_system_basic_6..........proved - complete [shostak](15.39 s)
Theory totals: 20 formulas, 20 attempted, 20 succeeded (32.60 s)
Proof summary for theory poly_families
polynomial_prod_int..................proved - complete [shostak]( 0.68 s)
prod_polynomials_TCC1................proved - complete [shostak]( 0.01 s)
prod_polynomials_TCC2................proved - complete [shostak]( 0.23 s)
prod_polynomials_TCC3................proved - complete [shostak]( 0.01 s)
prod_polynomials_TCC4................proved - complete [shostak]( 0.02 s)
prod_polynomials_TCC5................proved - complete [shostak]( 0.02 s)
prod_polynomials_TCC6................proved - complete [shostak]( 0.01 s)
prod_polynomials_TCC7................proved - complete [shostak]( 0.09 s)
prod_polynomials_TCC8................proved - complete [shostak]( 3.22 s)
prod_polynomials_list_TCC1...........proved - complete [shostak]( 0.08 s)
prod_polynomials_list_TCC2...........proved - complete [shostak]( 0.26 s)
prod_polynomials_list_TCC3...........proved - complete [shostak]( 0.71 s)
prod_polynomials_list_TCC4...........proved - complete [shostak]( 0.19 s)
prod_polynomials_list_TCC5...........proved - complete [shostak]( 0.68 s)
prod_polynomials_list_TCC6...........proved - complete [shostak]( 0.71 s)
prod_polynomials_list_TCC7...........proved - complete [shostak]( 0.81 s)
prod_polynomials_list_TCC8...........proved - complete [shostak]( 1.82 s)
TQ_fam_TCC1..........................proved - complete [shostak]( 0.26 s)
TQ_fam_TCC2..........................proved - complete [shostak]( 0.62 s)
TQ_fam_def_TCC1......................proved - complete [shostak]( 1.18 s)
TQ_fam_def...........................proved - complete [shostak]( 0.56 s)
Sol_TCC1.............................proved - complete [shostak]( 0.18 s)
Sol_all_TCC1.........................proved - complete [shostak]( 0.19 s)
sign_prod_TCC1.......................proved - complete [shostak]( 0.02 s)
sign_prod_TCC2.......................proved - complete [shostak]( 2.42 s)
sign_prod_eq.........................proved - complete [shostak]( 0.20 s)
sign_ext_pow_TCC1....................proved - complete [shostak]( 0.01 s)
sign_ext_pow_TCC2....................proved - complete [shostak]( 0.01 s)
sign_ext_pow.........................proved - complete [shostak]( 0.24 s)
sign_ext_prod_polynomials_TCC1.......proved - complete [shostak]( 0.05 s)
sign_ext_prod_polynomials............proved - complete [shostak]( 1.03 s)
unsig_TCC1...........................proved - complete [shostak]( 0.10 s)
sig_unsig............................proved - complete [shostak]( 0.12 s)
sig_seq_unsig_seq....................proved - complete [shostak]( 0.12 s)
base_3_seq_TCC1......................proved - complete [shostak]( 0.03 s)
base_3_seq_TCC2......................proved - complete [shostak]( 0.33 s)
base_6_seq_TCC1......................proved - complete [shostak]( 0.02 s)
sig_seq_base_3_onto..................proved - complete [shostak]( 0.91 s)
sig_seq_base_3_onto_2_TCC1...........proved - complete [shostak]( 0.03 s)
sig_seq_base_3_onto_2................proved - complete [shostak]( 0.22 s)
sig_seq_base_6_onto_TCC1.............proved - complete [shostak]( 0.08 s)
sig_seq_base_6_onto..................proved - complete [shostak]( 1.17 s)
sig_seq_base_6_onto_2_TCC1...........proved - complete [shostak]( 0.07 s)
sig_seq_base_6_onto_2................proved - complete [shostak]( 0.28 s)
base_3_seq_unique....................proved - complete [shostak]( 1.10 s)
base_n_3_seq_unique..................proved - complete [shostak]( 0.07 s)
union_upto_TCC1......................proved - complete [shostak]( 0.03 s)
union_upto_TCC2......................proved - complete [shostak]( 0.01 s)
union_upto_TCC3......................proved - complete [shostak]( 0.01 s)
union_upto_TCC4......................proved - complete [shostak]( 0.07 s)
union_upto_finite....................proved - complete [shostak]( 0.10 s)
real_set_disj_union_cards_TCC1.......proved - complete [shostak]( 0.06 s)
real_set_disj_union_cards............proved - complete [shostak]( 0.38 s)
mult_tarski_query_simple_TCC1........proved - complete [shostak]( 0.07 s)
mult_tarski_query_simple_TCC2........proved - complete [shostak]( 0.03 s)
mult_tarski_query_simple.............proved - complete [shostak]( 7.10 s)
split_index_fun_TCC1.................proved - complete [shostak]( 0.04 s)
split_index_fun_TCC2.................proved - complete [shostak]( 0.14 s)
split_base6_TCC1.....................proved - complete [shostak]( 0.01 s)
splits_to_base3......................proved - complete [shostak]( 0.06 s)
sign_prod_coeff6_TCC1................proved - complete [shostak]( 0.09 s)
NSol_seq6_TCC1.......................proved - complete [shostak]( 0.10 s)
mult_tarski_query_simple_6_0_to_3_TCC1...proved - complete [shostak]( 0.07 s)
mult_tarski_query_simple_6_0_to_3....proved - complete [shostak]( 7.34 s)
sign_coeff6_zero_entry_eq............proved - complete [shostak]( 0.04 s)
sign_coeff6_zero_TCC1................proved - complete [shostak]( 1.66 s)
sigma_disjoinction_6_TCC1............proved - complete [shostak]( 0.15 s)
sigma_disjoinction_6.................proved - complete [shostak](14.95 s)
mult_tarski_query_simple_6_above_2_TCC1...proved - complete [shostak]( 0.03 s)
mult_tarski_query_simple_6_above_2...proved - complete [shostak](41.99 s)
Theory totals: 70 formulas, 70 attempted, 70 succeeded (95.67 s)
Proof summary for theory sturmtarski
constructed_sturm_sequence?_TCC1.....proved - complete [shostak]( 0.02 s)
constructed_sturm_sequence?_TCC2.....proved - complete [shostak]( 0.01 s)
constructed_sturm_sequence?_TCC3.....proved - complete [shostak]( 0.04 s)
constructed_sturm_sequence?_TCC4.....proved - complete [shostak]( 0.10 s)
constructed_sturm_sequence?_TCC5.....proved - complete [shostak]( 0.13 s)
constructed_sturm_sequence?_TCC6.....proved - complete [shostak]( 0.11 s)
constructed_sturm_seq_repeated_root...proved - complete [shostak]( 0.99 s)
default_root_degree?_TCC1............proved - complete [shostak]( 0.20 s)
default_root_degree?_TCC2............proved - complete [shostak]( 0.06 s)
constructed_sturm_seq_root_degrees_TCC1...proved - complete [shostak]( 0.57 s)
constructed_sturm_seq_root_degrees...proved - complete [shostak]( 5.89 s)
default_root_deg_TCC1................proved - complete [shostak]( 0.14 s)
default_root_deg_def.................proved - complete [shostak]( 0.10 s)
constructed_sturm_seq_root_degree_lower_bound...proved - complete [shostak]( 1.93 s)
sturm_tarski_basic_1.................proved - complete [shostak]( 3.72 s)
sturm_tarski_basic_2.................proved - complete [shostak]( 1.92 s)
sturm_tarski_basic_3.................proved - complete [shostak]( 8.54 s)
sturm_tarski_basic_TCC1..............proved - complete [shostak]( 0.08 s)
sturm_tarski_basic...................proved - complete [shostak](18.80 s)
constructed_sturm_roots_between_enum_TCC1...proved - complete [shostak]( 0.06 s)
constructed_sturm_roots_between_enum_TCC2...proved - complete [shostak]( 0.05 s)
constructed_sturm_roots_between_enum...proved - complete [shostak]( 1.36 s)
Sol_TCC1.............................proved - complete [shostak]( 0.09 s)
Sol_union_top........................proved - complete [shostak]( 0.08 s)
NSol_TCC1............................proved - complete [shostak]( 0.03 s)
NSol_union_top.......................proved - complete [shostak]( 0.27 s)
sturm_tarski_TCC1....................proved - complete [shostak]( 0.09 s)
sturm_tarski_TCC2....................proved - complete [shostak]( 0.60 s)
sturm_tarski.........................proved - complete [shostak]( 5.31 s)
Sol_TCC2.............................proved - complete [shostak]( 0.04 s)
NSol_TCC2............................proved - complete [shostak]( 0.13 s)
sturm_tarski_unbounded_TCC1..........proved - complete [shostak]( 0.05 s)
sturm_tarski_unbounded_TCC2..........proved - complete [shostak]( 0.23 s)
sturm_tarski_unbounded...............proved - complete [shostak]( 0.75 s)
NSol_sq_gt...........................proved - complete [shostak]( 0.21 s)
NSol_sq_lt...........................proved - complete [shostak]( 0.10 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (52.81 s)
Proof summary for theory compute_sturm_tarski
der_prod_TCC1........................proved - complete [shostak]( 0.01 s)
der_prod_TCC2........................proved - complete [shostak]( 0.37 s)
finite_bij_real_remove_one...........proved - complete [shostak]( 0.22 s)
finite_bij_real_remove_two...........proved - complete [shostak]( 0.55 s)
computed_sturm_spec_TCC1.............proved - complete [shostak]( 0.09 s)
computed_sturm_spec_TCC2.............proved - complete [shostak]( 0.52 s)
computed_sturm_spec_TCC3.............proved - complete [shostak]( 0.60 s)
computed_sturm_spec_TCC4.............proved - complete [shostak]( 0.23 s)
computed_sturm_spec_TCC5.............proved - complete [shostak]( 0.59 s)
computed_sturm_spec..................proved - complete [shostak](10.01 s)
Eq_computed_remainder?_TCC1..........proved - complete [shostak]( 0.01 s)
Eq_computed_remainder?_TCC2..........proved - complete [shostak]( 0.12 s)
compute_TQ_param_TCC1................proved - complete [shostak]( 0.25 s)
compute_TQ_param_TCC2................proved - complete [shostak]( 0.30 s)
compute_TQ_param_TCC3................proved - complete [shostak]( 0.29 s)
compute_TQ_param_TCC4................proved - complete [shostak]( 0.33 s)
compute_TQ_param_TCC5................proved - complete [shostak]( 0.32 s)
TQ_TCC1..............................proved - complete [shostak]( 0.04 s)
TQ_TCC2..............................proved - complete [shostak]( 0.11 s)
TQ_TCC3..............................proved - complete [shostak]( 0.86 s)
TQ_def...............................proved - complete [shostak]( 3.86 s)
TQ_eq_g..............................proved - complete [shostak]( 0.13 s)
Theory totals: 22 formulas, 22 attempted, 22 succeeded (19.79 s)
Proof summary for theory strategies
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory poly_system_strategy
first_eq_TCC1........................proved - complete [shostak]( 0.01 s)
first_eq_TCC2........................proved - complete [shostak]( 0.03 s)
first_eq_TCC3........................proved - complete [shostak]( 0.07 s)
first_eq_TCC4........................proved - complete [shostak]( 0.06 s)
first_eq_TCC5........................proved - complete [shostak]( 0.05 s)
first_eq_TCC6........................proved - complete [shostak]( 0.02 s)
first_eq_TCC7........................proved - complete [shostak]( 0.00 s)
greatify_poly_TCC1...................proved - complete [shostak]( 0.03 s)
greatify_rel_TCC1....................proved - complete [shostak]( 0.01 s)
greatify_def_TCC1....................proved - complete [shostak]( 0.06 s)
greatify_def.........................proved - complete [shostak]( 0.35 s)
compute_solvable_single_TCC1.........proved - complete [shostak]( 0.04 s)
compute_solvable_single_TCC2.........proved - incomplete [shostak]( 0.38 s)
compute_solvable_single_TCC3.........proved - incomplete [shostak]( 0.42 s)
compute_solvable_single_TCC4.........proved - incomplete [shostak]( 0.07 s)
compute_solvable_single_TCC5.........proved - incomplete [shostak]( 0.08 s)
compute_solvable_single_def..........proved - incomplete [shostak]( 4.32 s)
poly_deriv_integer...................proved - complete [shostak]( 0.04 s)
compute_solvable_TCC1................proved - complete [shostak]( 0.03 s)
compute_solvable_TCC2................proved - complete [shostak]( 0.12 s)
compute_solvable_TCC3................proved - complete [shostak]( 0.14 s)
compute_solvable_TCC4................proved - complete [shostak]( 0.21 s)
compute_solvable_TCC5................proved - complete [shostak]( 0.10 s)
compute_solvable_TCC6................proved - incomplete [shostak]( 0.08 s)
compute_solvable_TCC7................proved - incomplete [shostak]( 0.42 s)
compute_solvable_TCC8................proved - incomplete [shostak]( 0.17 s)
compute_solvable_def.................proved - incomplete [shostak](14.46 s)
poly_system_list_TCC1................proved - complete [shostak]( 0.06 s)
poly_system_list_TCC2................proved - complete [shostak]( 0.13 s)
poly_system_list_TCC3................proved - complete [shostak]( 0.76 s)
tarski_TCC1..........................proved - complete [shostak]( 0.08 s)
tarski_TCC2..........................proved - complete [shostak]( 0.52 s)
tarski_TCC3..........................proved - complete [shostak]( 0.65 s)
tarski_TCC4..........................proved - complete [shostak]( 0.19 s)
tarski_def...........................proved - incomplete [shostak]( 0.80 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (24.93 s)
Proof summary for theory examples
example_fall_TCC1....................proved - complete [shostak]( 0.02 s)
example_fall_TCC2....................proved - complete [shostak]( 0.03 s)
example_fall.........................proved - incomplete [shostak]( 2.48 s)
example_ex_TCC1......................proved - complete [shostak]( 0.01 s)
example_ex...........................proved - incomplete [shostak]( 0.97 s)
example_1_TCC1.......................proved - complete [shostak]( 0.01 s)
example_1_TCC2.......................proved - complete [shostak]( 0.05 s)
example_1_TCC3.......................proved - complete [shostak]( 0.05 s)
example_1_TCC4.......................proved - complete [shostak]( 0.05 s)
example_1_TCC5.......................proved - complete [shostak]( 0.05 s)
example_1............................proved - incomplete [shostak]( 6.00 s)
example_2_TCC1.......................proved - complete [shostak]( 0.01 s)
example_2_TCC2.......................proved - complete [shostak]( 0.01 s)
example_2............................proved - incomplete [shostak]( 1.77 s)
example_3............................proved - incomplete [shostak](12.45 s)
example_4_TCC1.......................proved - complete [shostak]( 0.01 s)
example_4_TCC2.......................proved - complete [shostak]( 0.01 s)
example_4_TCC3.......................proved - complete [shostak]( 0.01 s)
example_4_TCC4.......................proved - complete [shostak]( 0.01 s)
example_4_TCC5.......................proved - complete [shostak]( 0.01 s)
example_4_TCC6.......................proved - complete [shostak]( 0.01 s)
example_4_TCC7.......................proved - complete [shostak]( 0.02 s)
example_4_TCC8.......................proved - complete [shostak]( 0.01 s)
example_4_TCC9.......................proved - complete [shostak]( 0.01 s)
example_4_TCC10......................proved - complete [shostak]( 0.14 s)
example_4_TCC11......................proved - complete [shostak]( 0.14 s)
example_4............................proved - incomplete [shostak](11.74 s)
example_5_TCC1.......................proved - complete [shostak]( 0.01 s)
example_5............................proved - incomplete [shostak]( 1.26 s)
Theory totals: 29 formulas, 29 attempted, 29 succeeded (37.36 s)
Grand Totals: 266 proofs, 266 attempted, 266 succeeded (298.42 s)
[ zur Elbe Produktseite wechseln0.151Quellennavigators
]
