| products/Sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: abstract_min.prf Sprache: Lisp
|
Untersuchungsergebnis.summary Download desMT940 {MT940[853] Hlasm[2357] Haskell[2675]}zum Wurzelverzeichnis wechseln *** *** top (17:34:1 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 vectors times_TCC1............................proved - complete [shostak](0.07 s) sqv_TCC1..............................proved - complete [shostak](0.05 s) sqv_rew...............................proved - complete [shostak](0.04 s) sqv_sos...............................proved - complete [shostak](0.04 s) unity_TCC1............................proved - complete [shostak](0.34 s) comp_distr_add........................proved - complete [shostak](0.01 s) comp_distr_sub........................proved - complete [shostak](0.02 s) comp_distr_scal.......................proved - complete [shostak](0.02 s) comp_distr_neg........................proved - complete [shostak](0.02 s) comp_zero.............................proved - complete [shostak](0.01 s) comps_eq..............................proved - complete [shostak](0.10 s) norm_comp_eq_0........................proved - complete [shostak](0.12 s) norm_sqv_eq_0.........................proved - complete [shostak](0.02 s) norm_eq_0.............................proved - complete [shostak](0.04 s) norm_zero.............................proved - complete [shostak](0.01 s) sqv_zero..............................proved - complete [shostak](0.03 s) sqv_eq_0..............................proved - complete [shostak](0.01 s) v_neq_zero............................proved - complete [shostak](0.02 s) v_neq_0...............................proved - complete [shostak](0.15 s) sq_dot_eq_0...........................proved - complete [shostak](0.03 s) nzv_comp_neq_0........................proved - complete [shostak](0.06 s) nz_norm_gt_0..........................proved - complete [shostak](0.01 s) nz_sqv_gt_0...........................proved - complete [shostak](0.01 s) normalized_nz.........................proved - complete [shostak](0.02 s) neg_nzv...............................proved - complete [shostak](0.05 s) nz_nzv................................proved - complete [shostak](0.09 s) neg_zero..............................proved - complete [shostak](0.03 s) add_zero_left.........................proved - complete [shostak](0.03 s) add_zero_right........................proved - complete [shostak](0.03 s) add_comm..............................proved - complete [shostak](0.03 s) add_assoc.............................proved - complete [shostak](0.06 s) add_move_left.........................proved - complete [shostak](0.07 s) add_move_right........................proved - complete [shostak](0.08 s) add_move_both.........................proved - complete [shostak](0.07 s) add_neg_sub...........................proved - complete [shostak](0.04 s) add_cancel............................proved - complete [shostak](0.04 s) add_cancel_neg........................proved - complete [shostak](0.05 s) add_cancel2...........................proved - complete [shostak](0.04 s) add_cancel_neg2.......................proved - complete [shostak](0.04 s) add_cancel_left.......................proved - complete [shostak](0.08 s) add_cancel_right......................proved - complete [shostak](0.08 s) add_eq_zero...........................proved - complete [shostak](0.07 s) neg_shift.............................proved - complete [shostak](0.06 s) sub_cancel_left.......................proved - complete [shostak](0.07 s) sub_cancel_right......................proved - complete [shostak](0.06 s) sub_zero_left.........................proved - complete [shostak](0.02 s) sub_zero_right........................proved - complete [shostak](0.03 s) sub_eq_args...........................proved - complete [shostak](0.02 s) sub_eq_zero...........................proved - complete [shostak](0.03 s) sub_cancel............................proved - complete [shostak](0.03 s) sub_cancel_neg........................proved - complete [shostak](0.04 s) neg_add_left..........................proved - complete [shostak](0.04 s) neg_add_right.........................proved - complete [shostak](0.04 s) neg_distr_sub.........................proved - complete [shostak](0.03 s) neg_neg...............................proved - complete [shostak](0.02 s) neg_distr_add.........................proved - complete [shostak](0.05 s) dot_neg_left..........................proved - complete [shostak](0.18 s) dot_neg_right.........................proved - complete [shostak](0.19 s) neg_dot_neg...........................proved - complete [shostak](0.02 s) dot_zero_left.........................proved - complete [shostak](0.06 s) dot_zero_right........................proved - complete [shostak](0.05 s) dot_comm..............................proved - complete [shostak](0.05 s) dot_assoc.............................proved - complete [shostak](0.09 s) dot_eq_args_ge........................proved - complete [shostak](0.04 s) add_comm_assoc_left...................proved - complete [shostak](0.02 s) add_comm_assoc_right..................proved - complete [shostak](0.02 s) dot_add_right.........................proved - complete [shostak](0.19 s) dot_add_left..........................proved - complete [shostak](0.20 s) dot_sub_right.........................proved - complete [shostak](0.04 s) dot_sub_left..........................proved - complete [shostak](0.05 s) dot_divby.............................proved - complete [shostak](0.15 s) dot_scal_left.........................proved - complete [shostak](0.10 s) dot_scal_right........................proved - complete [shostak](0.10 s) dot_scal_comm_assoc...................proved - complete [shostak](0.04 s) scal_comm_assoc.......................proved - complete [shostak](0.05 s) dot_scal_canon........................proved - complete [shostak](0.09 s) scal_add_left.........................proved - complete [shostak](0.08 s) scal_sub_left.........................proved - complete [shostak](0.09 s) scal_add_right........................proved - complete [shostak](0.10 s) scal_sub_right........................proved - complete [shostak](0.09 s) scal_assoc............................proved - complete [shostak](0.05 s) scal_neg..............................proved - complete [shostak](0.04 s) scal_cross............................proved - complete [shostak](0.12 s) scal_div_mult_left....................proved - complete [shostak](0.16 s) scal_div_mult_right...................proved - complete [shostak](0.15 s) scal_zero.............................proved - complete [shostak](0.03 s) scal_0................................proved - complete [shostak](0.04 s) scal_1................................proved - complete [shostak](0.05 s) scal_neg_1............................proved - complete [shostak](0.04 s) scal_cancel...........................proved - complete [shostak](0.09 s) scal_eq_zero..........................proved - complete [shostak](0.06 s) dot_ge_dist...........................proved - complete [shostak](0.39 s) dot_gt_dist...........................proved - complete [shostak](0.39 s) idem_right............................proved - complete [shostak](0.10 s) sqv_neg...............................proved - complete [shostak](0.07 s) sqv_add...............................proved - complete [shostak](0.09 s) sqv_scal..............................proved - complete [shostak](0.06 s) sqv_sub...............................proved - complete [shostak](0.12 s) sqv_sub_scal..........................proved - complete [shostak](0.30 s) sqv_sym...............................proved - complete [shostak](0.11 s) sqrt_sqv_sq...........................proved - complete [shostak](0.05 s) norm_sym..............................proved - complete [shostak](0.02 s) norm_neg..............................proved - complete [shostak](0.02 s) dot_sq_norm...........................proved - complete [shostak](0.01 s) sq_norm...............................proved - complete [shostak](0.01 s) sqrt_sqv_norm.........................proved - complete [shostak](0.01 s) norms_eq_sqv..........................proved - complete [shostak](0.03 s) norms_eq_sos..........................proved - complete [shostak](0.02 s) norm_le_sqv...........................proved - complete [shostak](0.02 s) norm_lt_sqv...........................proved - complete [shostak](0.02 s) norm_scal.............................proved - complete [shostak](0.09 s) caret_TCC1............................proved - complete [shostak](0.07 s) norm_normalize........................proved - complete [shostak](0.01 s) dot_normalize.........................proved - complete [shostak](0.08 s) normalize_normalize...................proved - complete [shostak](0.14 s) normalized_id.........................proved - complete [shostak](0.09 s) normalize_scal........................proved - complete [shostak](0.33 s) cauchy_schwarz........................proved - complete [shostak](0.41 s) dot_norm..............................proved - complete [shostak](0.14 s) schwarz...............................proved - complete [shostak](0.05 s) schwarz_cor...........................proved - complete [shostak](0.24 s) norm_triangle.........................proved - complete [shostak](0.09 s) norm_add_le...........................proved - complete [shostak](0.33 s) norm_sub_le...........................proved - complete [shostak](0.34 s) norm_sub_ge...........................proved - complete [shostak](0.04 s) norm_ge_comps.........................proved - complete [shostak](0.26 s) sq_norm_dist..........................proved - complete [shostak](0.29 s) parallel_refl.........................proved - complete [shostak](0.02 s) parallel_symm.........................proved - complete [shostak](0.05 s) parallel_trans........................proved - complete [shostak](0.05 s) parallel_zero.........................proved - complete [shostak](0.02 s) dir_parallel..........................proved - complete [shostak](0.02 s) pythagorean...........................proved - complete [shostak](0.07 s) norm_add_ge_left......................proved - complete [shostak](0.09 s) norm_add_ge_right.....................proved - complete [shostak](0.02 s) Theory totals: 135 formulas, 135 attempted, 135 succeeded (10.86 s) Proof summary for theory nvectors difference_TCC1.......................proved - complete [shostak](0.02 s) difference_TCC2.......................proved - complete [shostak](0.01 s) plus_TCC1.............................proved - complete [shostak](0.04 s) plus_TCC2.............................proved - complete [shostak](0.01 s) difference_TCC3.......................proved - complete [shostak](0.01 s) times_TCC1............................proved - complete [shostak](0.02 s) times_TCC2............................proved - complete [shostak](0.03 s) sqv_TCC1..............................proved - complete [shostak](0.05 s) sq_TCC1...............................proved - complete [shostak](0.01 s) zero_TCC1.............................proved - complete [shostak](0.01 s) zero_TCC2.............................proved - complete [shostak](0.07 s) unity_TCC1............................proved - complete [shostak](0.41 s) const_vec_TCC1........................proved - complete [shostak](0.01 s) comp_distr_add........................proved - complete [shostak](0.02 s) comp_distr_sub........................proved - complete [shostak](0.02 s) comp_distr_scal.......................proved - complete [shostak](0.01 s) comp_zero.............................proved - complete [shostak](0.02 s) comp_eq...............................proved - complete [shostak](0.05 s) add_zero_left_TCC1....................proved - complete [shostak](0.01 s) add_zero_left.........................proved - complete [shostak](0.05 s) add_zero_right_TCC1...................proved - complete [shostak](0.02 s) add_zero_right........................proved - complete [shostak](0.05 s) add_comm_TCC1.........................proved - complete [shostak](0.02 s) add_comm..............................proved - complete [shostak](0.01 s) add_assoc_TCC1........................proved - complete [shostak](0.01 s) add_assoc_TCC2........................proved - complete [shostak](0.02 s) add_assoc_TCC3........................proved - complete [shostak](0.01 s) add_assoc.............................proved - complete [shostak](0.05 s) add_move_right........................proved - complete [shostak](0.13 s) add_move_both.........................proved - complete [shostak](0.14 s) add_neg_sub_TCC1......................proved - complete [shostak](0.01 s) add_neg_sub...........................proved - complete [shostak](0.01 s) add_cancel_TCC1.......................proved - complete [shostak](0.02 s) add_cancel............................proved - complete [shostak](0.09 s) add_cancel_neg_TCC1...................proved - complete [shostak](0.01 s) add_cancel_neg_TCC2...................proved - complete [shostak](0.02 s) add_cancel_neg........................proved - complete [shostak](0.09 s) add_cancel2_TCC1......................proved - complete [shostak](0.02 s) add_cancel2...........................proved - complete [shostak](0.09 s) add_cancel_neg2_TCC1..................proved - complete [shostak](0.01 s) add_cancel_neg2.......................proved - complete [shostak](0.09 s) sub_zero_left.........................proved - complete [shostak](0.04 s) sub_zero_right........................proved - complete [shostak](0.05 s) sub_eq_args...........................proved - complete [shostak](0.03 s) sub_eq_zero_TCC1......................proved - complete [shostak](0.02 s) sub_eq_zero...........................proved - complete [shostak](0.12 s) sub_cancel_TCC1.......................proved - complete [shostak](0.01 s) sub_cancel............................proved - complete [shostak](0.03 s) sub_cancel_neg_TCC1...................proved - complete [shostak](0.02 s) sub_cancel_neg........................proved - complete [shostak](0.02 s) neg_add_left_TCC1.....................proved - complete [shostak](0.01 s) neg_add_left..........................proved - complete [shostak](0.02 s) neg_add_right.........................proved - complete [shostak](0.02 s) neg_distr_sub.........................proved - complete [shostak](0.03 s) neg_neg...............................proved - complete [shostak](0.04 s) neg_distr_add_TCC1....................proved - complete [shostak](0.01 s) neg_distr_add.........................proved - complete [shostak](0.04 s) dot_neg_left..........................proved - complete [shostak](0.11 s) dot_neg_right.........................proved - complete [shostak](0.10 s) dot_neg_sq............................proved - complete [shostak](0.06 s) dot_zero_left_TCC1....................proved - complete [shostak](0.01 s) dot_zero_left.........................proved - complete [shostak](0.10 s) dot_zero_right........................proved - complete [shostak](0.06 s) dot_comm..............................proved - complete [shostak](0.08 s) dot_assoc_TCC1........................proved - complete [shostak](0.02 s) dot_assoc.............................proved - complete [shostak](0.23 s) dot_eq_args_ge........................proved - complete [shostak](0.13 s) dot_distr_add_left....................proved - complete [shostak](0.32 s) dot_distr_add_right_TCC1..............proved - complete [shostak](0.01 s) dot_distr_add_right_TCC2..............proved - complete [shostak](0.02 s) dot_distr_add_right...................proved - complete [shostak](0.19 s) dot_distr_sub_left_TCC1...............proved - complete [shostak](0.02 s) dot_distr_sub_left....................proved - complete [shostak](0.20 s) dot_distr_sub_right_TCC1..............proved - complete [shostak](0.01 s) dot_distr_sub_right...................proved - complete [shostak](0.22 s) dot_divby.............................proved - complete [shostak](0.12 s) dot_scal_left_TCC1....................proved - complete [shostak](0.01 s) dot_scal_left.........................proved - complete [shostak](0.12 s) dot_scal_right_TCC1...................proved - complete [shostak](0.02 s) dot_scal_right........................proved - complete [shostak](0.12 s) dot_scal_assoc........................proved - complete [shostak](0.04 s) dot_scal_canon_TCC1...................proved - complete [shostak](0.01 s) dot_scal_canon........................proved - complete [shostak](0.12 s) dot_scal_distr_add_TCC1...............proved - complete [shostak](0.01 s) dot_scal_distr_add....................proved - complete [shostak](0.06 s) dot_scal_distr_sub....................proved - complete [shostak](0.07 s) scal_add_distr_TCC1...................proved - complete [shostak](0.01 s) scal_add_distr........................proved - complete [shostak](0.07 s) scal_sub_distr........................proved - complete [shostak](0.06 s) scal_zero.............................proved - complete [shostak](0.02 s) scal_0................................proved - complete [shostak](0.02 s) scal_1................................proved - complete [shostak](0.07 s) scal_cancel...........................proved - complete [shostak](0.19 s) scal_dot_eq_0.........................proved - complete [shostak](0.08 s) dot_ge_dist_TCC1......................proved - complete [shostak](0.01 s) dot_ge_dist_TCC2......................proved - complete [shostak](0.05 s) dot_ge_dist...........................proved - complete [shostak](0.33 s) dot_gt_dist_TCC1......................proved - complete [shostak](0.05 s) dot_gt_dist...........................proved - complete [shostak](0.26 s) sq_dot_eq.............................proved - complete [shostak](0.13 s) sqv_sq................................proved - complete [shostak](0.05 s) sq_sqv................................proved - complete [shostak](0.05 s) sq_lem................................proved - complete [shostak](0.04 s) sqv_lem...............................proved - complete [shostak](0.05 s) sqv_zero..............................proved - complete [shostak](0.03 s) sqv_eq_0..............................proved - complete [shostak](0.05 s) sqv_neg...............................proved - complete [shostak](0.05 s) sqv_add_TCC1..........................proved - complete [shostak](0.02 s) sqv_add...............................proved - complete [shostak](0.14 s) sqv_sub...............................proved - complete [shostak](0.14 s) sqv_sym...............................proved - complete [shostak](0.12 s) sqv_scal..............................proved - complete [shostak](0.05 s) sqrt_sqv_sq...........................proved - complete [shostak](0.06 s) norm_sym..............................proved - complete [shostak](0.02 s) norm_neg..............................proved - complete [shostak](0.04 s) dot_sq_norm...........................proved - complete [shostak](0.02 s) sq_norm...............................proved - complete [shostak](0.02 s) sqrt_sqv_norm.........................proved - complete [shostak](0.02 s) norm_eq_0.............................proved - complete [shostak](0.07 s) norms_eq_sqv..........................proved - complete [shostak](0.09 s) norm_scal.............................proved - complete [shostak](0.10 s) idem_right............................proved - complete [shostak](0.11 s) caret_TCC1............................proved - complete [shostak](0.07 s) caret_TCC2............................proved - complete [shostak](0.17 s) dot_normalize_TCC1....................proved - complete [shostak](0.06 s) dot_normalize_TCC2....................proved - complete [shostak](0.17 s) dot_normalize.........................proved - complete [shostak](0.10 s) normalize_normalize_TCC1..............proved - complete [shostak](0.03 s) normalize_normalize...................proved - complete [shostak](0.12 s) sqv_minus_dot_TCC1....................proved - complete [shostak](0.01 s) sqv_minus_dot.........................proved - complete [shostak](0.37 s) cauchy_schwarz........................proved - complete [shostak](0.44 s) dot_norm..............................proved - complete [shostak](0.14 s) norm_add_le...........................proved - complete [shostak](0.34 s) norm_sub_le...........................proved - complete [shostak](0.37 s) norm_sub_ge...........................proved - complete [shostak](0.06 s) norm_ge_comps.........................proved - complete [shostak](0.14 s) norm_triangle_TCC1....................proved - complete [shostak](0.03 s) norm_triangle.........................proved - complete [shostak](0.37 s) nzvec_has_nz..........................proved - complete [shostak](0.05 s) nzvec_neq_zero_TCC1...................proved - complete [shostak](0.01 s) nzvec_neq_zero........................proved - complete [shostak](0.05 s) v_neq_0...............................proved - complete [shostak](0.12 s) Theory totals: 143 formulas, 143 attempted, 143 succeeded (10.87 s) Proof summary for theory vectors_rew Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory vect2D vect2D_0..............................proved - complete [shostak](0.03 s) vect2D_1..............................proved - complete [shostak](0.04 s) Eq2D..................................proved - complete [shostak](0.05 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.12 s) Proof summary for theory vect3D Eq3D..................................proved - complete [shostak](0.07 s) vect3D_0..............................proved - complete [shostak](0.03 s) vect3D_1..............................proved - complete [shostak](0.04 s) vect3D_2..............................proved - complete [shostak](0.03 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.17 s) Proof summary for theory vectors_2D sqv_TCC1..............................proved - complete [shostak](0.03 s) sqv_rew...............................proved - complete [shostak](0.03 s) sqv_sos...............................proved - complete [shostak](0.03 s) iv_TCC1...............................proved - complete [shostak](0.00 s) jv_TCC1...............................proved - complete [shostak](0.01 s) basis.................................proved - complete [shostak](0.01 s) vx_distr_add..........................proved - complete [shostak](0.00 s) vy_distr_add..........................proved - complete [shostak](0.00 s) vx_distr_sub..........................proved - complete [shostak](0.01 s) vy_distr_sub..........................proved - complete [shostak](0.00 s) vx_scal...............................proved - complete [shostak](0.01 s) vy_scal...............................proved - complete [shostak](0.00 s) vx_neg................................proved - complete [shostak](0.01 s) vy_neg................................proved - complete [shostak](0.00 s) comp_eq_x.............................proved - complete [shostak](0.00 s) comp_eq_y.............................proved - complete [shostak](0.01 s) comps_eq..............................proved - complete [shostak](0.02 s) comp_zero_x...........................proved - complete [shostak](0.00 s) comp_zero_y...........................proved - complete [shostak](0.00 s) norm_xy_eq_0..........................proved - complete [shostak](0.08 s) norm_sqv_eq_0.........................proved - complete [shostak](0.02 s) norm_eq_0.............................proved - complete [shostak](0.02 s) norm_zero.............................proved - complete [shostak](0.01 s) sqv_zero..............................proved - complete [shostak](0.00 s) sqv_eq_0..............................proved - complete [shostak](0.02 s) v_neq_zero............................proved - complete [shostak](0.00 s) sq_dot_eq_0...........................proved - complete [shostak](0.04 s) nzv_xy_neq_0..........................proved - complete [shostak](0.03 s) nz_norm_gt_0..........................proved - complete [shostak](0.01 s) nz_sqv_gt_0...........................proved - complete [shostak](0.00 s) nz_nvz_left...........................proved - complete [shostak](0.00 s) nz_nvz_right..........................proved - complete [shostak](0.00 s) normalized_nz.........................proved - complete [shostak](0.01 s) neg_nzv...............................proved - complete [shostak](0.02 s) nz_nzv................................proved - complete [shostak](0.14 s) neg_zero..............................proved - complete [shostak](0.00 s) add_zero_left.........................proved - complete [shostak](0.01 s) add_zero_right........................proved - complete [shostak](0.01 s) add_comm..............................proved - complete [shostak](0.00 s) add_assoc.............................proved - complete [shostak](0.02 s) add_move_left.........................proved - complete [shostak](0.08 s) add_move_right........................proved - complete [shostak](0.09 s) add_move_both.........................proved - complete [shostak](0.10 s) add_neg_sub...........................proved - complete [shostak](0.00 s) add_cancel............................proved - complete [shostak](0.02 s) add_cancel_neg........................proved - complete [shostak](0.07 s) add_cancel2...........................proved - complete [shostak](0.01 s) add_cancel_neg2.......................proved - complete [shostak](0.02 s) add_cancel_left.......................proved - complete [shostak](0.02 s) add_cancel_right......................proved - complete [shostak](0.01 s) add_eq_zero...........................proved - complete [shostak](0.08 s) neg_shift.............................proved - complete [shostak](0.04 s) sub_cancel_left.......................proved - complete [shostak](0.05 s) sub_cancel_right......................proved - complete [shostak](0.03 s) sub_zero_left.........................proved - complete [shostak](0.00 s) sub_zero_right........................proved - complete [shostak](0.00 s) sub_eq_args...........................proved - complete [shostak](0.00 s) sub_eq_zero...........................proved - complete [shostak](0.04 s) sub_cancel............................proved - complete [shostak](0.00 s) sub_cancel_neg........................proved - complete [shostak](0.02 s) neg_add_left..........................proved - complete [shostak](0.00 s) neg_add_right.........................proved - complete [shostak](0.01 s) neg_distr_sub.........................proved - complete [shostak](0.01 s) neg_neg...............................proved - complete [shostak](0.02 s) neg_distr_add.........................proved - complete [shostak](0.03 s) dot_neg_left..........................proved - complete [shostak](0.04 s) dot_neg_right.........................proved - complete [shostak](0.04 s) neg_dot_neg...........................proved - complete [shostak](0.03 s) dot_zero_left.........................proved - complete [shostak](0.01 s) dot_zero_right........................proved - complete [shostak](0.00 s) dot_comm..............................proved - complete [shostak](0.05 s) dot_assoc.............................proved - complete [shostak](0.03 s) dot_eq_args_ge........................proved - complete [shostak](0.02 s) add_comm_assoc_left...................proved - complete [shostak](0.03 s) add_comm_assoc_right..................proved - complete [shostak](0.03 s) dot_add_right.........................proved - complete [shostak](0.06 s) dot_add_left..........................proved - complete [shostak](0.10 s) dot_sub_right.........................proved - complete [shostak](0.06 s) dot_sub_left..........................proved - complete [shostak](0.11 s) add_dot_add...........................proved - complete [shostak](0.11 s) dot_divby.............................proved - complete [shostak](0.09 s) dot_scal_left.........................proved - complete [shostak](0.03 s) dot_scal_right........................proved - complete [shostak](0.06 s) dot_scal_comm_assoc...................proved - complete [shostak](0.03 s) scal_assoc............................proved - complete [shostak](0.03 s) scal_comm_assoc.......................proved - complete [shostak](0.05 s) dot_scal_canon........................proved - complete [shostak](0.02 s) scal_add_left.........................proved - complete [shostak](0.06 s) scal_sub_left.........................proved - complete [shostak](0.05 s) scal_add_right........................proved - complete [shostak](0.05 s) scal_sub_right........................proved - complete [shostak](0.06 s) scal_neg..............................proved - complete [shostak](0.00 s) scal_cross............................proved - complete [shostak](0.10 s) scal_zero.............................proved - complete [shostak](0.01 s) scal_0................................proved - complete [shostak](0.00 s) scal_1................................proved - complete [shostak](0.04 s) scal_neg_1............................proved - complete [shostak](0.01 s) scal_cancel...........................proved - complete [shostak](0.08 s) scal_div_mult_left....................proved - complete [shostak](0.12 s) scal_div_mult_right...................proved - complete [shostak](0.15 s) scal_eq_zero..........................proved - complete [shostak](0.05 s) dot_ge_dist...........................proved - complete [shostak](0.21 s) dot_gt_dist...........................proved - complete [shostak](0.21 s) idem_right............................proved - complete [shostak](0.08 s) sqv_neg...............................proved - complete [shostak](0.03 s) sqv_add...............................proved - complete [shostak](0.13 s) sqv_scal..............................proved - complete [shostak](0.02 s) sqv_sub...............................proved - complete [shostak](0.12 s) sqv_sub_scal..........................proved - complete [shostak](0.32 s) sqv_sym...............................proved - complete [shostak](0.09 s) sqrt_sqv_sq...........................proved - complete [shostak](0.05 s) norm_sym..............................proved - complete [shostak](0.01 s) norm_neg..............................proved - complete [shostak](0.04 s) dot_sq_norm...........................proved - complete [shostak](0.03 s) sq_norm...............................proved - complete [shostak](0.10 s) sqv_eq_norm_eq........................proved - complete [shostak](0.01 s) norm_eq_sqv_eq........................proved - complete [shostak](0.02 s) sqrt_sqv_norm.........................proved - complete [shostak](0.01 s) norms_eq_sqv..........................proved - complete [shostak](0.01 s) norms_eq_sos..........................proved - complete [shostak](0.02 s) norm_le_sqv...........................proved - complete [shostak](0.01 s) norm_lt_sqv...........................proved - complete [shostak](0.00 s) norm_scal.............................proved - complete [shostak](0.09 s) caret_TCC1............................proved - complete [shostak](0.05 s) norm_normalize........................proved - complete [shostak](0.01 s) dot_normalize.........................proved - complete [shostak](0.06 s) normalize_normalize...................proved - complete [shostak](0.09 s) normalized_id.........................proved - complete [shostak](0.08 s) normalize_scal........................proved - complete [shostak](0.30 s) cauchy_schwarz........................proved - complete [shostak](0.49 s) dot_norm..............................proved - complete [shostak](0.13 s) schwarz...............................proved - complete [shostak](0.04 s) schwarz_converse......................proved - complete [shostak](4.22 s) schwarz_cor...........................proved - complete [shostak](0.23 s) norm_triangle.........................proved - complete [shostak](0.50 s) norm_add_le...........................proved - complete [shostak](0.31 s) norm_sub_le...........................proved - complete [shostak](0.34 s) norm_sub_ge...........................proved - complete [shostak](0.04 s) norm_ge_comps.........................proved - complete [shostak](0.11 s) sq_norm_dist..........................proved - complete [shostak](0.42 s) parallel_refl.........................proved - complete [shostak](0.01 s) parallel_symm.........................proved - complete [shostak](0.04 s) parallel_trans........................proved - complete [shostak](0.04 s) parallel_zero.........................proved - complete [shostak](0.02 s) dir_parallel..........................proved - complete [shostak](0.01 s) pythagorean...........................proved - complete [shostak](0.05 s) norm_add_ge_left......................proved - complete [shostak](0.09 s) norm_add_ge_right.....................proved - complete [shostak](0.01 s) bolzano_weierstrass...................proved - complete [shostak](1.12 s) Theory totals: 149 formulas, 149 attempted, 149 succeeded (13.71 s) Proof summary for theory vectors_2D_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory vectors_2D_rew Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory vectors_3D sqv_TCC1..............................proved - complete [shostak](0.04 s) sqv_rew...............................proved - complete [shostak](0.01 s) sqv_sos...............................proved - complete [shostak](0.04 s) basis.................................proved - complete [shostak](0.01 s) vx_distr_add..........................proved - complete [shostak](0.00 s) vy_distr_add..........................proved - complete [shostak](0.00 s) vz_distr_add..........................proved - complete [shostak](0.04 s) vx_distr_sub..........................proved - complete [shostak](0.01 s) vy_distr_sub..........................proved - complete [shostak](0.00 s) vz_distr_sub..........................proved - complete [shostak](0.01 s) vx_scal...............................proved - complete [shostak](0.00 s) vy_scal...............................proved - complete [shostak](0.01 s) vz_scal...............................proved - complete [shostak](0.00 s) vx_neg................................proved - complete [shostak](0.00 s) vy_neg................................proved - complete [shostak](0.01 s) vz_neg................................proved - complete [shostak](0.00 s) comp_eq_x.............................proved - complete [shostak](0.01 s) comp_eq_y.............................proved - complete [shostak](0.00 s) comp_eq_z.............................proved - complete [shostak](0.00 s) comps_eq..............................proved - complete [shostak](0.03 s) comp_zero_x...........................proved - complete [shostak](0.00 s) comp_zero_y...........................proved - complete [shostak](0.01 s) comp_zero_z...........................proved - complete [shostak](0.00 s) norm_xyz_eq_0.........................proved - complete [shostak](0.14 s) norm_sqv_eq_0.........................proved - complete [shostak](0.02 s) norm_eq_0.............................proved - complete [shostak](0.02 s) norm_zero.............................proved - complete [shostak](0.01 s) sqv_zero..............................proved - complete [shostak](0.00 s) sqv_eq_0..............................proved - complete [shostak](0.01 s) v_neq_zero............................proved - complete [shostak](0.01 s) sq_dot_eq_0...........................proved - complete [shostak](0.02 s) nzv_xyz_neq_0.........................proved - complete [shostak](0.03 s) nz_norm_gt_0..........................proved - complete [shostak](0.01 s) nz_sqv_gt_0...........................proved - complete [shostak](0.00 s) nz_nvz_left...........................proved - complete [shostak](0.00 s) nz_nvz_middle.........................proved - complete [shostak](0.01 s) nz_nvz_right..........................proved - complete [shostak](0.00 s) normalized_nz.........................proved - complete [shostak](0.01 s) neg_nzv...............................proved - complete [shostak](0.03 s) nz_nzv................................proved - complete [shostak](0.21 s) neg_zero..............................proved - complete [shostak](0.00 s) add_zero_left.........................proved - complete [shostak](0.02 s) add_zero_right........................proved - complete [shostak](0.01 s) add_comm..............................proved - complete [shostak](0.01 s) add_assoc.............................proved - complete [shostak](0.04 s) add_move_left.........................proved - complete [shostak](0.12 s) add_move_right........................proved - complete [shostak](0.12 s) add_move_both.........................proved - complete [shostak](0.12 s) add_neg_sub...........................proved - complete [shostak](0.01 s) add_cancel............................proved - complete [shostak](0.01 s) add_cancel_neg........................proved - complete [shostak](0.10 s) add_cancel2...........................proved - complete [shostak](0.02 s) add_cancel_neg2.......................proved - complete [shostak](0.02 s) add_cancel_left.......................proved - complete [shostak](0.02 s) add_cancel_right......................proved - complete [shostak](0.02 s) add_eq_zero...........................proved - complete [shostak](0.10 s) neg_shift.............................proved - complete [shostak](0.05 s) sub_cancel_left.......................proved - complete [shostak](0.08 s) sub_cancel_right......................proved - complete [shostak](0.04 s) sub_zero_left.........................proved - complete [shostak](0.01 s) sub_zero_right........................proved - complete [shostak](0.01 s) sub_eq_args...........................proved - complete [shostak](0.01 s) sub_eq_zero...........................proved - complete [shostak](0.05 s) sub_cancel............................proved - complete [shostak](0.01 s) sub_cancel_neg........................proved - complete [shostak](0.02 s) neg_add_left..........................proved - complete [shostak](0.01 s) neg_add_right.........................proved - complete [shostak](0.01 s) neg_distr_sub.........................proved - complete [shostak](0.01 s) neg_neg...............................proved - complete [shostak](0.03 s) neg_distr_add.........................proved - complete [shostak](0.04 s) dot_neg_left..........................proved - complete [shostak](0.05 s) dot_neg_right.........................proved - complete [shostak](0.06 s) neg_dot_neg...........................proved - complete [shostak](0.05 s) dot_zero_left.........................proved - complete [shostak](0.01 s) dot_zero_right........................proved - complete [shostak](0.00 s) dot_comm..............................proved - complete [shostak](0.08 s) dot_assoc.............................proved - complete [shostak](0.05 s) dot_eq_args_ge........................proved - complete [shostak](0.04 s) add_comm_assoc_left...................proved - complete [shostak](0.04 s) add_comm_assoc_right..................proved - complete [shostak](0.04 s) dot_add_right.........................proved - complete [shostak](0.09 s) dot_add_left..........................proved - complete [shostak](0.16 s) dot_sub_right.........................proved - complete [shostak](0.08 s) dot_sub_left..........................proved - complete [shostak](0.15 s) dot_divby.............................proved - complete [shostak](0.12 s) dot_scal_left.........................proved - complete [shostak](0.04 s) dot_scal_right........................proved - complete [shostak](0.09 s) dot_scal_comm_assoc...................proved - complete [shostak](0.05 s) scal_comm_assoc.......................proved - complete [shostak](0.07 s) dot_scal_canon........................proved - complete [shostak](0.03 s) scal_add_left.........................proved - complete [shostak](0.07 s) scal_sub_left.........................proved - complete [shostak](0.08 s) scal_add_right........................proved - complete [shostak](0.07 s) scal_sub_right........................proved - complete [shostak](0.08 s) scal_assoc............................proved - complete [shostak](0.05 s) scal_neg..............................proved - complete [shostak](0.01 s) scal_cross............................proved - complete [shostak](0.14 s) scal_zero.............................proved - complete [shostak](0.01 s) scal_0................................proved - complete [shostak](0.00 s) scal_1................................proved - complete [shostak](0.04 s) scal_neg_1............................proved - complete [shostak](0.01 s) scal_cancel...........................proved - complete [shostak](0.11 s) scal_div_mult_left....................proved - complete [shostak](0.17 s) scal_div_mult_right...................proved - complete [shostak](0.22 s) scal_eq_zero..........................proved - complete [shostak](0.08 s) dot_ge_dist...........................proved - complete [shostak](0.33 s) dot_gt_dist...........................proved - complete [shostak](0.33 s) idem_right............................proved - complete [shostak](0.10 s) sqv_neg...............................proved - complete [shostak](0.05 s) sqv_add...............................proved - complete [shostak](0.17 s) sqv_scal..............................proved - complete [shostak](0.04 s) sqv_sub...............................proved - complete [shostak](0.17 s) sqv_sub_scal..........................proved - complete [shostak](0.37 s) sqv_sym...............................proved - complete [shostak](0.15 s) sqrt_sqv_sq...........................proved - complete [shostak](0.05 s) norm_sym..............................proved - complete [shostak](0.01 s) norm_neg..............................proved - complete [shostak](0.06 s) dot_sq_norm...........................proved - complete [shostak](0.06 s) sq_norm...............................proved - complete [shostak](0.13 s) sqrt_sqv_norm.........................proved - complete [shostak](0.01 s) norms_eq_sqv..........................proved - complete [shostak](0.02 s) norms_eq_sos..........................proved - complete [shostak](0.01 s) norm_le_sqv...........................proved - complete [shostak](0.00 s) norm_lt_sqv...........................proved - complete [shostak](0.01 s) norm_scal.............................proved - complete [shostak](0.08 s) caret_TCC1............................proved - complete [shostak](0.06 s) norm_normalize........................proved - complete [shostak](0.00 s) dot_normalize.........................proved - complete [shostak](0.07 s) normalize_normalize...................proved - complete [shostak](0.08 s) normalized_id.........................proved - complete [shostak](0.08 s) normalize_scal........................proved - complete [shostak](0.29 s) cauchy_schwarz........................proved - complete [shostak](0.64 s) dot_norm..............................proved - complete [shostak](0.13 s) schwarz...............................proved - complete [shostak](0.04 s) schwarz_cor...........................proved - complete [shostak](0.22 s) norm_triangle.........................proved - complete [shostak](0.77 s) norm_add_le...........................proved - complete [shostak](0.31 s) norm_sub_le...........................proved - complete [shostak](0.34 s) norm_sub_ge...........................proved - complete [shostak](0.03 s) norm_ge_comps.........................proved - complete [shostak](0.25 s) sq_norm_dist..........................proved - complete [shostak](0.58 s) parallel_refl.........................proved - complete [shostak](0.01 s) parallel_symm.........................proved - complete [shostak](0.03 s) parallel_trans........................proved - complete [shostak](0.04 s) parallel_zero.........................proved - complete [shostak](0.01 s) dir_parallel..........................proved - complete [shostak](0.01 s) pythagorean...........................proved - complete [shostak](0.05 s) norm_add_ge_left......................proved - complete [shostak](0.08 s) norm_add_ge_right.....................proved - complete [shostak](0.01 s) Theory totals: 149 formulas, 149 attempted, 149 succeeded (10.73 s) Proof summary for theory vectors_3D_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory vectors_3D_rew Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory vectors_4D sqv_TCC1..............................proved - complete [shostak](0.05 s) sqv_rew...............................proved - complete [shostak](0.00 s) sqv_sos...............................proved - complete [shostak](0.05 s) basis.................................proved - complete [shostak](0.01 s) vx_distr_add..........................proved - complete [shostak](0.01 s) vy_distr_add..........................proved - complete [shostak](0.00 s) vz_distr_add..........................proved - complete [shostak](0.05 s) vt_distr_add..........................proved - complete [shostak](0.00 s) vx_distr_sub..........................proved - complete [shostak](0.01 s) vy_distr_sub..........................proved - complete [shostak](0.00 s) vz_distr_sub..........................proved - complete [shostak](0.01 s) vt_distr_sub..........................proved - complete [shostak](0.01 s) vx_scal...............................proved - complete [shostak](0.00 s) vy_scal...............................proved - complete [shostak](0.00 s) vz_scal...............................proved - complete [shostak](0.01 s) vt_scal...............................proved - complete [shostak](0.00 s) vx_neg................................proved - complete [shostak](0.01 s) vy_neg................................proved - complete [shostak](0.00 s) vz_neg................................proved - complete [shostak](0.00 s) vt_neg................................proved - complete [shostak](0.01 s) comp_eq_x.............................proved - complete [shostak](0.00 s) comp_eq_y.............................proved - complete [shostak](0.01 s) comp_eq_z.............................proved - complete [shostak](0.00 s) comp_eq_t.............................proved - complete [shostak](0.01 s) comps_eq..............................proved - complete [shostak](0.02 s) comp_zero_x...........................proved - complete [shostak](0.01 s) comp_zero_y...........................proved - complete [shostak](0.00 s) comp_zero_z...........................proved - complete [shostak](0.00 s) comp_zero_t...........................proved - complete [shostak](0.01 s) norm_xyz_eq_0.........................proved - complete [shostak](0.21 s) norm_sqv_eq_0.........................proved - complete [shostak](0.02 s) norm_eq_0.............................proved - complete [shostak](0.03 s) norm_zero.............................proved - complete [shostak](0.01 s) sqv_zero..............................proved - complete [shostak](0.00 s) sqv_eq_0..............................proved - complete [shostak](0.01 s) v_neq_zero............................proved - complete [shostak](0.00 s) sq_dot_eq_0...........................proved - complete [shostak](0.02 s) nzv_xyz_neq_0.........................proved - complete [shostak](0.03 s) nz_norm_gt_0..........................proved - complete [shostak](0.01 s) nz_sqv_gt_0...........................proved - complete [shostak](0.00 s) nz_nvz_left...........................proved - complete [shostak](0.00 s) nz_nvz_middle.........................proved - complete [shostak](0.01 s) nz_nvz_right..........................proved - complete [shostak](0.00 s) nz_nvz_time...........................proved - complete [shostak](0.01 s) normalized_nz.........................proved - complete [shostak](0.01 s) neg_nzv...............................proved - complete [shostak](0.03 s) nz_nzv................................proved - complete [shostak](0.28 s) neg_zero..............................proved - complete [shostak](0.01 s) add_zero_left.........................proved - complete [shostak](0.02 s) add_zero_right........................proved - complete [shostak](0.01 s) add_comm..............................proved - complete [shostak](0.01 s) add_assoc.............................proved - complete [shostak](0.05 s) add_move_left.........................proved - complete [shostak](0.16 s) add_move_right........................proved - complete [shostak](0.16 s) add_move_both.........................proved - complete [shostak](0.17 s) add_neg_sub...........................proved - complete [shostak](0.01 s) add_cancel............................proved - complete [shostak](0.02 s) add_cancel_neg........................proved - complete [shostak](0.12 s) add_cancel2...........................proved - complete [shostak](0.02 s) add_cancel_neg2.......................proved - complete [shostak](0.01 s) add_cancel_left.......................proved - complete [shostak](0.03 s) add_cancel_right......................proved - complete [shostak](0.02 s) add_eq_zero...........................proved - complete [shostak](0.14 s) neg_shift.............................proved - complete [shostak](0.07 s) sub_cancel_left.......................proved - complete [shostak](0.10 s) sub_cancel_right......................proved - complete [shostak](0.05 s) sub_zero_left.........................proved - complete [shostak](0.00 s) sub_zero_right........................proved - complete [shostak](0.02 s) sub_eq_args...........................proved - complete [shostak](0.00 s) sub_eq_zero...........................proved - complete [shostak](0.08 s) sub_cancel............................proved - complete [shostak](0.01 s) sub_cancel_neg........................proved - complete [shostak](0.02 s) neg_add_left..........................proved - complete [shostak](0.01 s) neg_add_right.........................proved - complete [shostak](0.01 s) neg_distr_sub.........................proved - complete [shostak](0.02 s) neg_neg...............................proved - complete [shostak](0.03 s) neg_distr_add.........................proved - complete [shostak](0.05 s) dot_neg_left..........................proved - complete [shostak](0.07 s) dot_neg_right.........................proved - complete [shostak](0.07 s) neg_dot_neg...........................proved - complete [shostak](0.07 s) dot_zero_left.........................proved - complete [shostak](0.01 s) dot_zero_right........................proved - complete [shostak](0.00 s) dot_comm..............................proved - complete [shostak](0.10 s) dot_assoc.............................proved - complete [shostak](0.07 s) dot_eq_args_ge........................proved - complete [shostak](0.05 s) add_comm_assoc_left...................proved - complete [shostak](0.06 s) add_comm_assoc_right..................proved - complete [shostak](0.05 s) dot_add_right.........................proved - complete [shostak](0.12 s) dot_add_left..........................proved - complete [shostak](0.21 s) dot_sub_right.........................proved - complete [shostak](0.12 s) dot_sub_left..........................proved - complete [shostak](0.22 s) dot_divby.............................proved - complete [shostak](0.16 s) dot_scal_left.........................proved - complete [shostak](0.06 s) dot_scal_right........................proved - complete [shostak](0.12 s) dot_scal_comm_assoc...................proved - complete [shostak](0.06 s) scal_comm_assoc.......................proved - complete [shostak](0.09 s) dot_scal_canon........................proved - complete [shostak](0.05 s) scal_add_left.........................proved - complete [shostak](0.09 s) scal_sub_left.........................proved - complete [shostak](0.10 s) scal_add_right........................proved - complete [shostak](0.09 s) scal_sub_right........................proved - complete [shostak](0.10 s) scal_assoc............................proved - complete [shostak](0.06 s) scal_neg..............................proved - complete [shostak](0.01 s) scal_cross............................proved - complete [shostak](0.17 s) scal_zero.............................proved - complete [shostak](0.00 s) scal_0................................proved - complete [shostak](0.01 s) scal_1................................proved - complete [shostak](0.05 s) scal_neg_1............................proved - complete [shostak](0.01 s) scal_cancel...........................proved - complete [shostak](0.16 s) scal_div_mult_left....................proved - complete [shostak](0.24 s) scal_div_mult_right...................proved - complete [shostak](0.29 s) scal_eq_zero..........................proved - complete [shostak](0.09 s) dot_ge_dist...........................proved - complete [shostak](0.46 s) dot_gt_dist...........................proved - complete [shostak](0.46 s) idem_right............................proved - complete [shostak](0.13 s) sqv_neg...............................proved - complete [shostak](0.07 s) sqv_add...............................proved - complete [shostak](0.24 s) sqv_scal..............................proved - complete [shostak](0.05 s) sqv_sub...............................proved - complete [shostak](0.23 s) sqv_sub_scal..........................proved - complete [shostak](0.42 s) sqv_sym...............................proved - complete [shostak](0.21 s) sqrt_sqv_sq...........................proved - complete [shostak](0.04 s) norm_sym..............................proved - complete [shostak](0.02 s) norm_neg..............................proved - complete [shostak](0.09 s) dot_sq_norm...........................proved - complete [shostak](0.06 s) sq_norm...............................proved - complete [shostak](0.17 s) sqrt_sqv_norm.........................proved - complete [shostak](0.01 s) norms_eq_sqv..........................proved - complete [shostak](0.02 s) norms_eq_sos..........................proved - complete [shostak](0.01 s) norm_le_sqv...........................proved - complete [shostak](0.01 s) norm_lt_sqv...........................proved - complete [shostak](0.01 s) norm_scal.............................proved - complete [shostak](0.08 s) caret_TCC1............................proved - complete [shostak](0.06 s) norm_normalize........................proved - complete [shostak](0.00 s) dot_normalize.........................proved - complete [shostak](0.07 s) normalize_normalize...................proved - complete [shostak](0.08 s) normalized_id.........................proved - complete [shostak](0.08 s) normalize_scal........................proved - complete [shostak](0.29 s) cauchy_schwarz........................proved - complete [shostak](0.82 s) dot_norm..............................proved - complete [shostak](0.13 s) schwartz..............................proved - complete [shostak](0.04 s) schwartz_cor..........................proved - complete [shostak](0.22 s) norm_triangle.........................proved - complete [shostak](0.07 s) norm_add_le...........................proved - complete [shostak](0.31 s) norm_sub_le...........................proved - complete [shostak](0.34 s) norm_sub_ge...........................proved - complete [shostak](0.03 s) norm_ge_comps.........................proved - complete [shostak](0.43 s) sq_norm_dist..........................proved - complete [shostak](0.74 s) parallel_refl.........................proved - complete [shostak](0.01 s) parallel_symm.........................proved - complete [shostak](0.04 s) parallel_trans........................proved - complete [shostak](0.05 s) parallel_zero.........................proved - complete [shostak](0.02 s) dir_parallel..........................proved - complete [shostak](0.01 s) pythagorean...........................proved - complete [shostak](0.05 s) norm_add_ge_left......................proved - complete [shostak](0.09 s) norm_add_ge_right.....................proved - complete [shostak](0.01 s) Theory totals: 156 formulas, 156 attempted, 156 succeeded (12.54 s) Proof summary for theory vectors_4D_def Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory vectors_cos cosines_law...........................proved - complete [shostak](0.84 s) angle_exists..........................proved - complete [shostak](0.37 s) angle_between_TCC1....................proved - complete [shostak](0.13 s) cosines_law_bnd.......................proved - complete [shostak](0.51 s) cosines_law_ge........................proved - complete [shostak](0.09 s) cosines_law_le........................proved - complete [shostak](0.04 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.99 s) Proof summary for theory vectors_2D_cos cosines_law...........................proved - complete [shostak](0.79 s) angle_exists..........................proved - complete [shostak](0.35 s) angle_between_TCC1....................proved - complete [shostak](0.11 s) cosines_law_bnd.......................proved - complete [shostak](0.50 s) cosines_law_ge........................proved - complete [shostak](0.08 s) cosines_law_le........................proved - complete [shostak](0.03 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.87 s) Proof summary for theory vectors_3D_cos cosines_law...........................proved - complete [shostak](0.80 s) angle_exists..........................proved - complete [shostak](0.36 s) angle_between_TCC1....................proved - complete [shostak](0.11 s) cosines_law_bnd.......................proved - complete [shostak](0.49 s) cosines_law_ge........................proved - complete [shostak](0.08 s) cosines_law_le........................proved - complete [shostak](0.04 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.89 s) Proof summary for theory distance sq_dist_TCC1..........................proved - complete [shostak](0.01 s) sq_dist_TCC2..........................proved - complete [shostak](0.01 s) sq_dist_TCC3..........................proved - complete [shostak](0.01 s) dist_eq_args..........................proved - complete [shostak](0.06 s) dist_zero_l...........................proved - complete [shostak](0.04 s) dist_zero_r...........................proved - complete [shostak](0.04 s) dist_sym..............................proved - complete [shostak](0.11 s) dist_eq_0.............................proved - complete [shostak](0.12 s) dist_norm.............................proved - complete [shostak](0.13 s) dist_rel..............................proved - complete [shostak](0.09 s) sq_dist_is_dist_sq....................proved - complete [shostak](0.21 s) sq_dist_norm..........................proved - complete [shostak](0.02 s) sq_dist_sym...........................proved - complete [shostak](0.02 s) sq_dist_le............................proved - complete [shostak](0.02 s) sq_dist_lt............................proved - complete [shostak](0.01 s) dist_gt_comp..........................proved - complete [shostak](0.12 s) sq_dist_dist..........................proved - complete [shostak](0.18 s) on_segment_beg........................proved - complete [shostak](0.02 s) on_segment_end........................proved - complete [shostak](0.05 s) on_line_beg...........................proved - complete [shostak](0.01 s) on_line_end...........................proved - complete [shostak](0.03 s) on_segment_on_line....................proved - complete [shostak](0.01 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (1.33 s) Proof summary for theory distance_2D dist_eq_args..........................proved - complete [shostak](0.03 s) dist_zero_l...........................proved - complete [shostak](0.04 s) dist_zero_r...........................proved - complete [shostak](0.04 s) dist_sym..............................proved - complete [shostak](0.16 s) dist_eq_0.............................proved - complete [shostak](0.08 s) dist_norm.............................proved - complete [shostak](0.21 s) dist_rel..............................proved - complete [shostak](0.20 s) sq_dist_is_dist_sq....................proved - complete [shostak](0.32 s) sq_dist_norm..........................proved - complete [shostak](0.01 s) sq_dist_sym...........................proved - complete [shostak](0.01 s) sq_dist_le............................proved - complete [shostak](0.02 s) sq_dist_lt............................proved - complete [shostak](0.01 s) dist_ge_x.............................proved - complete [shostak](0.06 s) dist_ge_y.............................proved - complete [shostak](0.06 s) --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.220Quellennavigators ] |