| products/sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: fixed_points.prf Sprache: Unknown
|
Musik.summary BilderMT940 {MT940[634] Hlasm[1132] Haskell[1528]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** top (19:20:38 11/7/2014) *** Generated by proveit - ProofLite-6.0.9 (3/14/14) *** Trusted Oracles *** MetiTarski: MetiTarski Theorem Prover via PVS proof rule metit *** Proof summary for theory top Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory util eq_correct_1..........................proved - complete [shostak](0.48 s) eq_neg................................proved - complete [shostak](0.12 s) gt_correct_1..........................proved - complete [shostak](1.35 s) lt_correct_1..........................proved - complete [shostak](0.06 s) ge_correct_1..........................proved - complete [shostak](0.05 s) le_correct_1..........................proved - complete [shostak](0.04 s) gt_correct_2..........................proved - complete [shostak](0.35 s) lt_correct_2..........................proved - complete [shostak](0.09 s) ge_correct_2..........................proved - complete [shostak](0.08 s) le_correct_2..........................proved - complete [shostak](0.08 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (2.70 s) Proof summary for theory horizontal_dist_convexity horiz_dist_convex_scaf................proved - complete [shostak](1.25 s) horiz_dist_strictly_convex_scaf.......proved - complete [shostak](1.25 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (2.50 s) Proof summary for theory vertical_dist_convexity vert_dist_convex_scaf.................proved - complete [shostak](0.12 s) vert_dist_strictly_convex_scaf........proved - complete [shostak](0.53 s) vert_dist_scaf_quad_eq_0..............proved - complete [shostak](0.31 s) vert_dist_scaf_quad_ge_0..............proved - complete [shostak](0.44 s) vert_dist_scaf_quad_gt_0..............proved - complete [shostak](0.52 s) vert_dist_scaf_quad_le_0..............proved - complete [shostak](0.45 s) vert_dist_scaf_quad_lt_0..............proved - complete [shostak](0.51 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (2.88 s) Proof summary for theory definitions horizontalCoordination_symm...........proved - complete [shostak](0.03 s) Horizontal_Strategy_TCC1..............proved - complete [shostak](0.03 s) horizontalCoordination_strategy.......proved - complete [shostak](0.02 s) horizontal_tca_gt_0_TCC1..............proved - complete [shostak](0.09 s) horizontal_tca_gt_0...................proved - complete [shostak](0.06 s) horizontal_tca_nzv_gt_0...............proved - complete [shostak](0.06 s) horizontal_tca_lt_0_TCC1..............proved - complete [shostak](0.07 s) horizontal_tca_lt_0...................proved - complete [shostak](0.06 s) horizontal_tca_nzv_lt_0...............proved - complete [shostak](0.06 s) horizontal_tca_dot_zero...............proved - complete [shostak](-.03 s) horizontal_sq_dtca_eq.................proved - complete [shostak](0.39 s) horizontal_tca_min....................proved - complete [shostak](0.35 s) sqv_decreasing_before_horizontal_tca...proved - complete [shostak](0.71 s) sqv_increasing_after_horizontal_tca...proved - complete [shostak](0.72 s) le_rel................................proved - complete [shostak](0.08 s) Vdir_perp.............................proved - complete [shostak](0.09 s) W0_dot................................proved - complete [shostak](0.04 s) nz_W0.................................proved - complete [shostak](0.03 s) nz_W..................................proved - complete [shostak](0.08 s) W_dot.................................proved - complete [shostak](0.07 s) dot_W.................................proved - complete [shostak](0.60 s) s_dot_Vdir_eq_0.......................proved - complete [shostak](0.07 s) W0_dot_Vdir_eq_0......................proved - complete [shostak](0.10 s) norm_W0_ge............................proved - complete [shostak](0.58 s) dot_pos_divergent.....................proved - complete [shostak](0.10 s) dot_nneg_divergent....................proved - complete [shostak](0.50 s) gs_nz.................................proved - complete [shostak](0.02 s) gs_only_id............................proved - complete [shostak](0.02 s) gs_only_scal..........................proved - complete [shostak](0.02 s) gs_only_symm..........................proved - complete [shostak](0.08 s) gs_only_trans.........................proved - complete [shostak](0.07 s) gs_only_normalize.....................proved - complete [shostak](0.09 s) gs_only_zero_left.....................proved - complete [shostak](0.03 s) gs_only_zero_right....................proved - complete [shostak](0.03 s) trk_only_id...........................proved - complete [shostak](0.02 s) trk_only_symm.........................proved - complete [shostak](0.16 s) trk_only_zero_left....................proved - complete [shostak](0.03 s) trk_only_zero_right...................proved - complete [shostak](0.02 s) optimal_id............................proved - complete [shostak](0.02 s) z_at_vertical_tau_eq_0................proved - complete [shostak](0.03 s) Theory totals: 40 formulas, 40 attempted, 40 succeeded (5.60 s) Proof summary for theory gs_only k_l_det...............................proved - complete [shostak](0.37 s) k_l_det_nz............................proved - complete [shostak](1.88 s) gs_only_line_k_l_TCC1.................proved - complete [shostak](0.08 s) gs_only_line_k_l_TCC2.................proved - complete [shostak](0.02 s) gs_only_line_k_l_complete.............proved - complete [shostak](0.17 s) gs_only_line_TCC1.....................proved - complete [shostak](0.04 s) same_gs_only_line.....................proved - complete [shostak](0.26 s) gs_only_line_complete.................proved - complete [shostak](0.08 s) gs_only_dot_TCC1......................proved - complete [shostak](0.13 s) gs_only_dot_complete..................proved - complete [shostak](0.25 s) gs_only_circle_TCC1...................proved - complete [shostak](0.17 s) gs_only_circle_TCC2...................proved - complete [shostak](0.03 s) gs_only_circle_TCC3...................proved - complete [shostak](0.03 s) gs_only_circle_solution...............proved - complete [shostak](1.89 s) gs_only_circle_complete...............proved - complete [shostak](0.92 s) gs_only_vertical_TCC1.................proved - complete [shostak](0.03 s) gs_only_vertical_TCC2.................proved - complete [shostak](0.06 s) gs_only_vertical_TCC3.................proved - complete [shostak](0.05 s) gs_only_vertical_TCC4.................proved - complete [shostak](0.02 s) gs_only_vertical_on_D.................proved - complete [shostak](0.85 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (7.33 s) Proof summary for theory horizontal ss_nzv................................proved - complete [shostak](0.09 s) ss_sp.................................proved - complete [shostak](0.12 s) neg_ss................................proved - complete [shostak](0.03 s) neg_sp................................proved - complete [shostak](0.11 s) horizontal_conflict_sum_closed........proved - complete [shostak](1.80 s) horizontal_conflict_neg...............proved - complete [shostak](0.44 s) horizontal_conflict_symm..............proved - complete [shostak](0.03 s) horizontal_conflict_scal..............proved - complete [shostak](0.08 s) horizontal_conflict_ever..............proved - complete [shostak](0.03 s) horizontal_conflict_ever_scal.........proved - complete [shostak](0.07 s) Delta_zero_eq_0.......................proved - complete [shostak](0.05 s) Delta_scal............................proved - complete [shostak](0.18 s) Delta_eq..............................proved - complete [shostak](0.11 s) Delta_symm............................proved - complete [shostak](0.06 s) Delta_discr2b.........................proved - complete [shostak](0.09 s) Delta_gt_0_nzv........................proved - complete [shostak](0.05 s) ground_speed..........................proved - complete [shostak](0.03 s) Delta_gt_0............................proved - complete [shostak](0.31 s) Delta_gt_0_on_D.......................proved - complete [shostak](-1.19 s) Delta_eq_0_dot_on_D...................proved - complete [shostak](0.24 s) Delta_ge_0............................proved - complete [shostak](0.65 s) Delta_ge_0_2..........................proved - complete [shostak](0.06 s) Delta_eq_0_eq_tca.....................proved - complete [shostak](3.14 s) sdotv_lt_0............................proved - complete [shostak](0.62 s) Theta_D_TCC1..........................proved - complete [shostak](0.04 s) Theta_D_on_D..........................proved - complete [shostak](0.63 s) Theta_D_unique_eps....................proved - complete [shostak](0.22 s) Theta_D_unique........................proved - complete [shostak](0.06 s) Theta_D_symm_TCC1.....................proved - complete [shostak](0.03 s) Theta_D_symm..........................proved - complete [shostak](0.05 s) Theta_D_scal_TCC1.....................proved - complete [shostak](0.05 s) Theta_D_scal..........................proved - complete [shostak](-.37 s) Theta_D_neg_nzv_TCC1..................proved - complete [shostak](0.44 s) Theta_D_neg_nzv.......................proved - complete [shostak](0.39 s) Theta_D_le............................proved - complete [shostak](0.15 s) Theta_D_lt_TCC1.......................proved - complete [shostak](0.02 s) Theta_D_lt............................proved - complete [shostak](0.15 s) Theta_D_Delta_eq_0....................proved - complete [shostak](0.12 s) Theta_D_eq_0..........................proved - complete [shostak](0.16 s) Theta_D_ge_0..........................proved - complete [shostak](0.45 s) Theta_D_neq_0.........................proved - complete [shostak](0.34 s) horizontal_conflict...................proved - complete [shostak](0.18 s) horizontal_conflict_on_D..............proved - complete [shostak](1.14 s) horizontal_entry_le...................proved - complete [shostak](0.55 s) not_horizontal_entry_lt...............proved - complete [shostak](0.49 s) horizontal_los_inside_Theta...........proved - complete [shostak](0.10 s) horizontal_sep_outside_Theta..........proved - complete [shostak](0.42 s) not_horiz_sep_inside_closed_Theta.....proved - complete [shostak](0.25 s) Theta_D_entry_gt_0_TCC1...............proved - complete [shostak](0.06 s) Theta_D_entry_gt_0....................proved - complete [shostak](0.06 s) Theta_D_exit_gt_0.....................proved - complete [shostak](0.64 s) Theta_D_entry_lt_t_TCC1...............proved - complete [shostak](0.57 s) Theta_D_entry_lt_t....................proved - complete [shostak](0.79 s) horizontal_conflict_entry_TCC1........proved - complete [shostak](0.05 s) horizontal_conflict_entry.............proved - complete [shostak](0.09 s) not_horizontal_conflict_exit_TCC1.....proved - complete [shostak](0.04 s) not_horizontal_conflict_exit..........proved - complete [shostak](0.09 s) Theta_D_horizontal_dir_TCC1...........proved - complete [shostak](0.41 s) Theta_D_horizontal_dir................proved - complete [shostak](0.60 s) horizontal_tca_midpoint...............proved - complete [shostak](0.33 s) horizontal_tca_entry_exit_TCC1........proved - complete [shostak](0.29 s) horizontal_tca_entry_exit.............proved - complete [shostak](0.06 s) horizontal_tca_los....................proved - complete [shostak](0.05 s) horizontal_tca_le_D...................proved - complete [shostak](0.05 s) horizontal_tca_pos....................proved - complete [shostak](0.06 s) Theta_D_positive_conflict.............proved - complete [shostak](0.09 s) circle_solution_2D_horizontal_sep.....proved - complete [shostak](0.07 s) Theta_D_circle_solution_2D............proved - complete [shostak](0.08 s) circle_solution_2D_Delta_ge_0.........proved - complete [shostak](0.03 s) circle_solution_2D_Theta_D_TCC1.......proved - complete [shostak](0.03 s) circle_solution_2D_Theta_D............proved - complete [shostak](0.60 s) circle_solution_2D_strict_horizontal_sep...proved - complete [shostak](0.06 s) Theta_D_line_intersection.............proved - complete [shostak](-1.32 s) tangent_line_intersection_v_independent...proved - complete [shostak](0.26 s) tangent_vector_not_conflict...........proved - complete [shostak](0.44 s) horizontal_conflict_is_an_open_set....proved - complete [shostak](0.55 s) Theory totals: 76 formulas, 76 attempted, 76 succeeded (18.40 s) Proof summary for theory trk_only trk_only_line_TCC1....................proved - complete [shostak](0.51 s) trk_only_line_TCC2....................proved - complete [shostak](0.03 s) same_trk_only_line....................proved - complete [shostak](0.05 s) trk_only_line_complete................proved - complete [shostak](0.37 s) trk_only_line_lt......................proved - complete [shostak](0.20 s) trk_only_dot_TCC1.....................proved - complete [shostak](0.13 s) trk_only_dot_complete.................proved - complete [shostak](0.25 s) trk_only_circle_eq_dot................proved - complete [shostak](0.67 s) trk_spc_on_D..........................proved - complete [shostak](0.13 s) trk_spc_Delta_ge_0....................proved - complete [shostak](0.05 s) trk_spc_dot...........................proved - complete [shostak](0.20 s) trk_spc_line_solution.................proved - complete [shostak](0.06 s) trk_spc_horizontal_dir................proved - complete [shostak](0.51 s) trk_only_circle_TCC1..................proved - complete [shostak](0.15 s) trk_only_circle_TCC2..................proved - complete [shostak](0.03 s) trk_only_circle_TCC3..................proved - complete [shostak](0.02 s) trk_only_circle_solution..............proved - complete [shostak](0.77 s) trk_only_circle_complete..............proved - complete [shostak](1.24 s) trk_only_vertical_TCC1................proved - complete [shostak](0.03 s) trk_only_vertical_TCC2................proved - complete [shostak](0.06 s) trk_only_vertical_TCC3................proved - complete [shostak](0.06 s) trk_only_vertical_TCC4................proved - complete [shostak](0.02 s) trk_only_vertical_on_D................proved - complete [shostak](0.85 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (6.39 s) Proof summary for theory line_solutions line_solution_dot_neg.................proved - complete [shostak](0.11 s) line_solution_sep_dot_negative........proved - complete [shostak](0.23 s) line_solution_on_D_TCC1...............proved - complete [shostak](0.03 s) line_solution_on_D....................proved - complete [shostak](0.23 s) on_D_line.............................proved - complete [shostak](0.11 s) line_solution_scal....................proved - complete [shostak](1.04 s) line_solution_zero_eps................proved - complete [shostak](0.10 s) line_solution_zero....................proved - complete [shostak](0.20 s) line_solution_Delta...................proved - complete [shostak](1.94 s) det_neq_0.............................proved - complete [shostak](0.15 s) line_solution_eps.....................proved - complete [shostak](0.17 s) line_solution_eps_line................proved - complete [shostak](0.04 s) line_solution_meets_horizontal_criterion...proved - complete [shostak](0.09 s) line_solution_independence............proved - complete [shostak](0.25 s) line_solution_invariant_TCC1..........proved - complete [shostak](0.05 s) line_solution_invariant...............proved - complete [shostak](0.11 s) line_solution_rewrite.................proved - complete [shostak](1.90 s) line_solution_det.....................proved - complete [shostak](0.92 s) line_solution_scal_unique.............proved - complete [shostak](2.71 s) line_solution_coordination............proved - complete [shostak](0.14 s) line_solution_along_line_TCC1.........proved - complete [shostak](0.50 s) line_solution_along_line..............proved - complete [shostak](0.26 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (11.30 s) Proof summary for theory horizontal_criteria R_TCC1................................proved - complete [shostak](0.03 s) R_eq_0................................proved - complete [shostak](0.21 s) R_gt_0................................proved - complete [shostak](0.03 s) R_symm................................proved - complete [shostak](0.04 s) sq_R_det..............................proved - complete [shostak](0.11 s) Delta_sq_det..........................proved - complete [shostak](1.70 s) Delta_sq_det_equality.................proved - complete [shostak](1.18 s) Delta_zero_eps_line_equality..........proved - complete [shostak](0.67 s) horizontal_solution...................proved - complete [shostak](1.50 s) horizontal_criterion_scal.............proved - complete [shostak](0.20 s) horizontal_criterion_eps..............proved - complete [shostak](0.34 s) horizontal_criterion_symmetric........proved - complete [shostak](0.71 s) horizontal_criterion_eps_unique.......proved - complete [shostak](0.15 s) horizontal_criterion_independence.....proved - complete [shostak](0.45 s) horizontal_criterion_sum_closed.......proved - complete [shostak](0.76 s) horizontal_criterion_coordination.....proved - complete [shostak](0.13 s) horizontal_sep_dir....................proved - complete [shostak](0.48 s) horizontal_exit_independence..........proved - complete [shostak](-1.87 s) horizontal_exit_coordination..........proved - complete [shostak](0.27 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (7.09 s) Proof summary for theory predicate_coordination_2D coordinated_symmetric_2D..............proved - complete [shostak](0.10 s) sum_indep_coordinated_2D..............proved - complete [shostak](0.20 s) coordinated_sum_indep_2D..............proved - complete [shostak](0.50 s) sum_indep_coordinated_antisym_2D......proved - complete [shostak](0.20 s) coordinated_antisym_sum_indep_2D......proved - complete [shostak](0.52 s) deriv_0_2D............................proved - complete [shostak](0.03 s) deriv_subset_2D.......................proved - complete [shostak](0.08 s) deriv_coordinated_2D..................proved - complete [shostak](0.35 s) deriv_coordinated_1...................proved - complete [shostak](0.05 s) Comb_coordinated_2D...................proved - complete [shostak](0.15 s) coordinated_implies_independent_2D....proved - complete [shostak](0.04 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.22 s) Proof summary for theory opt_trk_gs k_opt_tangent.........................proved - complete [shostak](0.06 s) opt_trk_gs_line_TCC1..................proved - complete [shostak](0.53 s) opt_trk_gs_line_TCC2..................proved - complete [shostak](0.07 s) opt_trk_gs_dot_TCC1...................proved - complete [shostak](0.12 s) opt_trk_gs_vertical_TCC1..............proved - complete [shostak](0.03 s) opt_trk_gs_vertical_TCC2..............proved - complete [shostak](0.06 s) opt_trk_gs_vertical_on_D..............proved - complete [shostak](0.91 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.78 s) Proof summary for theory horizontal_criterion_line horizontal_criterion_rewrite..........proved - complete [shostak](3.05 s) horizontal_criterion_special_coordination...proved - complete [shostak](0.58 s) horizontal_criterion_dot_equality.....proved - complete [shostak](0.23 s) horizontal_criterion_line_invariance...proved - complete [shostak](0.37 s) horizontal_criterion_line_coordination...proved - complete [shostak](0.04 s) horizontal_criterion_ext_subset.......proved - complete [shostak](0.55 s) horizontal_criterion_ext_restrict.....proved - complete [shostak](0.06 s) horizontal_criterion_ext_restrict_conflict...proved - complete [shostak](0.05 s) horizontal_criterion_ext_independence...proved - complete [shostak](0.03 s) horizontal_criterion_ext_coordinated...proved - complete [shostak](2.00 s) horizontal_criterion_ext_sum_closed...proved - complete [shostak](1.15 s) horizontal_criterion_ext_scal.........proved - complete [shostak](0.34 s) horizontal_criterion_ext_seg_convex...proved - complete [shostak](1.13 s) horizontal_criterion_ext_seg_independence_TCC1...proved - complete [shostak](0.53 s) horizontal_criterion_ext_seg_independence...proved - complete [shostak](0.46 s) horizontal_criterion_ext_seg_coordination_TCC1...proved - complete [shostak](0.87 s) horizontal_criterion_ext_seg_coordination_TCC2...proved - complete [shostak](3.98 s) horizontal_criterion_ext_seg_coordination...proved - complete [shostak](-.58 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (14.86 s) Proof summary for theory tangent_line alpha_TCC1............................proved - complete [shostak](0.12 s) beta_TCC1.............................proved - complete [shostak](0.03 s) alpha_neg.............................proved - complete [shostak](0.03 s) beta_neg..............................proved - complete [shostak](0.09 s) sq_alpha_beta.........................proved - complete [shostak](0.29 s) Q_on_D................................proved - complete [shostak](0.40 s) Q_asymm...............................proved - complete [shostak](0.22 s) Qs_asymm..............................proved - complete [shostak](0.05 s) sqv_Qs................................proved - complete [shostak](0.59 s) Qs_nzv................................proved - complete [shostak](0.04 s) s_dot_Qs_lt_0.........................proved - complete [shostak](0.36 s) det_s_Qs_lt_0.........................proved - complete [shostak](0.54 s) alpha_D...............................proved - complete [shostak](0.04 s) beta_R................................proved - complete [shostak](0.14 s) alpha_beta............................proved - complete [shostak](0.16 s) beta_alpha............................proved - complete [shostak](0.11 s) det_v_Q...............................proved - complete [shostak](0.30 s) s_dot_Q...............................proved - complete [shostak](0.15 s) det_s_Qs..............................proved - complete [shostak](0.17 s) det_Q_s...............................proved - complete [shostak](0.31 s) Q_eq_Qs_perp_TCC1.....................proved - complete [shostak](0.14 s) Q_eq_Qs_perp..........................proved - complete [shostak](1.07 s) line_solution_Qs......................proved - complete [shostak](0.59 s) parallel_nzv_Qs.......................proved - complete [shostak](1.49 s) parallel_nzv_perp.....................proved - complete [shostak](0.80 s) tangent_line_TCC1.....................proved - complete [shostak](0.10 s) tangent_line_TCC2.....................proved - complete [shostak](0.02 s) tangent_line_asymm....................proved - complete [shostak](0.16 s) line_solution_tangent_line............proved - complete [shostak](0.04 s) parallel_nzv_tangent_line.............proved - complete [shostak](0.05 s) tangent_line_solution.................proved - complete [shostak](0.07 s) tangent_line_independence.............proved - complete [shostak](0.03 s) tangent_line_coordination.............proved - complete [shostak](0.05 s) Theory totals: 33 formulas, 33 attempted, 33 succeeded (8.76 s) Proof summary for theory trk_line trk_line_eps_irt_TCC1.................proved - complete [shostak](0.04 s) trk_line_eps_irt_TCC2.................proved - complete [shostak](0.03 s) trk_line_eps_irt_tangent_line.........proved - complete [shostak](0.17 s) trk_line_eps_irt_dot..................proved - complete [shostak](0.51 s) irt_trk_line_eps......................proved - complete [shostak](0.05 s) trk_line_eps_tangent_line.............proved - complete [shostak](0.04 s) trk_line_is_line_solution.............proved - complete [shostak](0.03 s) trk_line_complete.....................proved - complete [shostak](0.07 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.94 s) Proof summary for theory gs_line gs_line_eps_TCC1......................proved - complete [shostak](0.03 s) gs_line_eps_TCC2......................proved - complete [shostak](0.02 s) gs_line_eps_tangent_line..............proved - complete [shostak](0.16 s) gs_line_is_line_solution..............proved - complete [shostak](0.04 s) gs_line_complete......................proved - complete [shostak](0.07 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.32 s) Proof summary for theory opt_line opt_line_eps_TCC1.....................proved - complete [shostak](0.03 s) opt_line_eps_TCC2.....................proved - complete [shostak](0.03 s) opt_line_eps_tangent_line.............proved - complete [shostak](0.17 s) opt_line_is_line_solution.............proved - complete [shostak](0.04 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.27 s) Proof summary for theory horizontal_cr horizontal_cr_is_line_solution........proved - complete [shostak](0.05 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s) Proof summary for theory repulsive tca_TCC1.............................proved - complete [shostak]( 0.02 s) repulsive_simple.....................proved - complete [shostak]( 0.43 s) repulsive_transitive.................proved - complete [shostak]( 0.68 s) not_repulsive_sum_closed.............proved - complete [shostak]( 1.40 s) repulsive_criteria_scal_s............proved - complete [shostak]( 0.62 s) repulsive_criteria_scal_nv...........proved - complete [shostak]( 1.69 s) wedge_containment....................proved - complete [shostak]( 3.27 s) repulsive_criteria_transitive........proved - complete [shostak]( 2.94 s) repulsive_criteria_transitive_odd1...proved - complete [shostak]( 2.15 s) rep_crit_odd2_ax.....................proved - complete [shostak]( 0.77 s) repulsive_criteria_transitive_odd2...proved - complete [shostak]( 3.16 s) repulsive_criteria_transitive_odd3...proved - complete [shostak]( 4.00 s) repulsive_criteria_sum_closed........proved - complete [shostak]( 1.45 s) repulsive_criteria_indep_of_length...proved - complete [shostak]( 0.51 s) repulsive_criteria_repulsive.........proved - complete [shostak]( 3.12 s) repulsive_criteria_repulsive2........proved - complete [shostak]( 3.83 s) repulsive_criteria_symmetric.........proved - complete [shostak]( 0.95 s) repulsive_criteria_coordinately_repulsive...proved - complete [shostak]( 1.56 s) foo..................................proved - complete [shostak](32.74 s) repulsive_increases_dist_TCC1........proved - complete [shostak]( 0.75 s) repulsive_increases_dist.............proved - complete [shostak]( 0.62 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (66.64 s) Proof summary for theory horizontal_los_criterion horizontal_los_criterion_repulsive....proved - complete [shostak](0.03 s) horizontal_los_criterion_coordinately_repulsive...proved - complete [shostak](0.03 s Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.06 s) Proof summary for theory horizontal_los sDs_TCC1..............................proved - complete [shostak](0.38 s) gs_los_TCC1...........................proved - complete [shostak](0.41 s) gs_los_TCC2...........................proved - complete [shostak](0.04 s) gs_los_def............................proved - complete [shostak](2.04 s) trk_los_TCC1..........................proved - complete [shostak](0.33 s) trk_los_TCC2..........................proved - complete [shostak](0.04 s) trk_los_def...........................proved - complete [shostak](1.79 s) los_recovery_meets_criteria...........proved - complete [shostak](0.46 s) los_recovery_independence.............proved - complete [shostak](0.09 s) los_recovery_coordination_TCC1........proved - complete [shostak](0.04 s) los_recovery_coordination.............proved - complete [shostak](0.32 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (5.93 s) Proof summary for theory old_horiz_los_criterion horizontal_los_crit_symm..............proved - complete [shostak](0.43 s) horizontal_los_crit_independent.......proved - complete [shostak](0.03 s) horizontal_los_crit_coordinated.......proved - complete [shostak](0.42 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.88 s) Proof summary for theory circle_optimum_2D intersects_circle_fun_scal...........proved - complete [shostak]( 0.31 s) intersects_circle_fun_def............proved - complete [shostak]( 0.64 s) intersects_circle_fun_inc............proved - complete [shostak]( 1.98 s) inter_circle_max_time_TCC1...........proved - complete [shostak]( 0.38 s) inter_circle_max_time_TCC2...........proved - complete [shostak]( 0.16 s) inter_circle_max_time_scal...........proved - complete [shostak]( 0.38 s) inter_circle_max_time_def............proved - complete [shostak]( 0.71 s) inter_circle_max_norm_scal...........proved - complete [shostak]( 0.60 s) max_norm_increasing..................proved - complete [shostak](12.54 s) max_circle_point_in_slice_TCC1.......proved - complete [shostak]( 0.07 s) lem1.................................proved - complete [shostak]( 0.38 s) lem2.................................proved - complete [shostak]( 0.58 s) max_circle_point_in_slice_intersection...proved - complete [shostak]( 4.14 s) max_circle_point_in_slice_union......proved - complete [shostak]( 0.39 s) dot_gt_dot_equals_slice_intersection...proved - complete [shostak]( 7.79 s) dot_gt_dot_equals_slice_union........proved - complete [shostak]( 7.20 s) max_circle_point_in_slice_lem........proved - complete [shostak]( 3.97 s) max_circle_point_in_slice_lem_eq.....proved - complete [shostak]( 0.61 s) max_circle_point_in_slide_sym_lem....proved - complete [shostak]( 3.94 s) max_circle_point_in_slice_def........proved - complete [shostak]( 6.80 s) max_circle_point_in_slice_complete...proved - complete [shostak]( 1.10 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (54.67 s) Proof summary for theory wedge_optimum_2D intersects_segment_fun?_TCC1..........proved - complete [shostak](0.06 s) intersects_segment_fun?_TCC2..........proved - complete [shostak](0.23 s) intersects_segment_fun?_TCC3..........proved - complete [shostak](0.32 s) intersects_segment_fun?_TCC4..........proved - complete [shostak](0.47 s) intersects_segment_fun_def............proved - complete [shostak](1.61 s) intersects_segment_sym................proved - complete [shostak](-1.98 s) on_segment_in_wedge_sym...............proved - complete [shostak](0.07 s) max_segment_point_in_slice_TCC1.......proved - complete [shostak](0.13 s) max_segment_point_in_slice_TCC2.......proved - complete [shostak](0.43 s) max_segment_point_in_slice_TCC3.......proved - complete [shostak](0.43 s) max_segment_point_in_slice_def........proved - complete [shostak](3.48 s) max_segment_point_in_slice_complete...proved - complete [shostak](0.05 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (5.30 s) Proof summary for theory vertical_los_criterion time_vertical_exit_by_TCC1............proved - complete [shostak](0.13 s) time_vertical_exit_by_TCC2............proved - complete [shostak](0.07 s) time_vertical_exit_by_TCC3............proved - complete [shostak](0.15 s) time_vertical_exit_by_symm............proved - complete [shostak](0.18 s) min_rel_vert_speed_TCC1...............proved - complete [shostak](0.03 s) min_rel_vert_speed_TCC2...............proved - complete [shostak](0.11 s) min_rel_vert_speed_symm...............proved - complete [shostak](0.12 s) vs_bound_crit_indep_TCC1..............proved - complete [shostak](0.04 s) vs_bound_crit_indep_TCC2..............proved - complete [shostak](0.04 s) vs_bound_crit_indep...................proved - complete [shostak](8.20 s) vs_bound_crit_coord...................proved - complete [shostak](7.72 s) vs_bound_dir..........................proved - complete [shostak](0.13 s) vertical_los_criterion_coord..........proved - complete [shostak](1.79 s) vertical_sep_after_def................proved - complete [shostak](0.25 s) z_los_vertical_sep....................proved - complete [shostak](1.26 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (20.22 s) Proof summary for theory vertical nz_spz................................proved - complete [shostak](0.04 s) neg_spz...............................proved - complete [shostak](0.05 s) on_signed_H...........................proved - complete [shostak](0.08 s) vertical_conflict_neg.................proved - complete [shostak](0.57 s) vertical_conflict_symm................proved - complete [shostak](0.04 s) Theta_H_symm..........................proved - complete [shostak](0.18 s) Theta_H_lt............................proved - complete [shostak](0.36 s) Theta_H_on_H..........................proved - complete [shostak](0.31 s) Theta_H_eq_0..........................proved - complete [shostak](0.57 s) Theta_H_ge_0..........................proved - complete [shostak](0.74 s) Theta_H_exit_gt_0.....................proved - complete [shostak](0.34 s) Theta_H_unique_eps....................proved - complete [shostak](0.41 s) Theta_H_unique........................proved - complete [shostak](0.21 s) vertical_los_entry....................proved - complete [shostak](0.62 s) Theta_H_entry_lt_t....................proved - complete [shostak](0.40 s) vertical_conflict.....................proved - complete [shostak](1.05 s) vertical_los_inside_Theta.............proved - complete [shostak](0.77 s) vertical_sep_outside_Theta............proved - complete [shostak](0.16 s) Theta_H_vertical_dir..................proved - complete [shostak](0.38 s) vertical_tau_entry_exit...............proved - complete [shostak](0.33 s) vertical_tau_midpoint.................proved - complete [shostak](0.11 s) vertical_tau_pos......................proved - complete [shostak](0.19 s) vs_at_neg.............................proved - complete [shostak](0.09 s) vs_at_H...............................proved - complete [shostak](0.08 s) vs_at_complete........................proved - complete [shostak](0.15 s) vertical_sep_dir......................proved - complete [shostak](2.43 s) vertical_sep_at_sign..................proved - complete [shostak](0.82 s) vertical_solution_vertical_sep........proved - complete [shostak](0.20 s) vertical_solution_strict_vertical_sep...proved - complete [shostak](0.66 s) Theta_H_vertical_solution.............proved - complete [shostak](0.19 s) vertical_solution_Theta_H.............proved - complete [shostak](0.62 s) vs_at_complete_vertical_solution......proved - complete [shostak](0.41 s) vs_at_complete_dir....................proved - complete [shostak](0.35 s) vertical_solution_exit................proved - complete [shostak](2.14 s) vs_circle_at_direction................proved - complete [shostak](0.84 s) vs_circle_at?_TCC1....................proved - complete [shostak](0.13 s) vs_circle_at_complete_TCC1............proved - complete [shostak](0.04 s) vs_circle_at_complete_TCC2............proved - complete [shostak](0.22 s) vs_circle_at_complete.................proved - complete [shostak](3.03 s) Theory totals: 39 formulas, 39 attempted, 39 succeeded (20.31 s) Proof summary for theory space_3D conflict_symm.........................proved - complete [shostak](0.44 s) conflict_ever.........................proved - complete [shostak](0.11 s) conflict_ever_shift...................proved - complete [shostak](0.51 s) conflict_sum_closed...................proved - complete [shostak](2.57 s) conflict_is_an_open_set...............proved - complete [shostak](1.59 s) vertical_horizontal_conflict..........proved - complete [shostak](0.09 s) neg_spz...............................proved - complete [shostak](0.06 s) neg_sp2...............................proved - complete [shostak](0.12 s) neg_sp................................proved - complete [shostak](0.14 s) spv2..................................proved - complete [shostak](0.13 s) ssv2..................................proved - complete [shostak](0.04 s) sp_nzv................................proved - complete [shostak](0.09 s) verticalCoordinationConflict_TCC1.....proved - complete [shostak](0.48 s) verticalCoordinationConflict_asymm....proved - complete [shostak](1.12 s) Vertical_Strategy_TCC1................proved - complete [shostak](0.04 s) verticalCoordinationConflict_strategy...proved - complete [shostak](0.04 s) verticalCoordinationConflict_correct_TCC1...proved - complete [shostak](0.04 s) verticalCoordinationConflict_correct...proved - complete [shostak](-.64 s) vs_los_strategy_TCC1..................proved - complete [shostak](0.07 s) vs_los_vertical_strategy..............proved - complete [shostak](1.03 s) Theory totals: 20 formulas, 20 attempted, 20 succeeded (8.07 s) Proof summary for theory definitions_3D nzv2..................................proved - complete [shostak](0.02 s) break_symmetry_neg....................proved - complete [shostak](0.12 s) vs_only_symm..........................proved - complete [shostak](0.03 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.17 s) Proof summary for theory vertical_los_crit_CA Decision_Vector_TCC1..................proved - complete [shostak](0.24 s) dv_to_ec_antisymmetric................proved - complete [shostak](0.07 s) vertical_decision_vect_TCC1...........proved - complete [shostak](0.14 s) vertical_decision_vect_TCC2...........proved - complete [shostak](0.22 s) vertical_decision_vect_TCC3...........proved - complete [shostak](0.03 s) vertical_decision_vect_TCC4...........proved - complete [shostak](0.03 s) vertical_decision_vect_TCC5...........proved - complete [shostak](0.25 s) vertical_decision_vect_TCC6...........proved - complete [shostak](0.13 s) vertical_decision_vect_antisymmetric...proved - complete [shostak](2.16 s) vertical_los_crit_CA_independent_TCC1...proved - complete [shostak](0.03 s) vertical_los_crit_CA_independent_TCC2...proved - complete [shostak](0.04 s) vertical_los_crit_CA_independent......proved - complete [shostak](0.16 s) vertical_los_crit_CA_independent_strong_TCC1...proved - complete [shostak](0.03 s) vertical_los_crit_CA_independent_strong_TCC2...proved - complete [shostak](0.04 s) vertical_los_crit_CA_independent_strong...proved - complete [shostak](3.32 s) vertical_los_crit_CA_independent_vspeed...proved - complete [shostak](0.12 s) vertical_los_crit_CA_coordinated_vspeed...proved - complete [shostak](0.32 s) vertical_los_crit_CA_coordinated......proved - complete [shostak](0.20 s) vertical_los_crit_CA_coordinated_strong_TCC1...proved - complete [shostak](0.04 s) vertical_los_crit_CA_coordinated_strong_TCC2...proved - complete [shostak](0.04 s) vertical_los_crit_CA_coordinated_strong...proved - complete [shostak](1.17 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (8.79 s) Proof summary for theory cd3d conflict_3D_2D_stable_TCC1............proved - complete [shostak](0.16 s) conflict_3D_2D_stable_TCC2............proved - complete [shostak](0.32 s) conflict_3D_2D_stable_TCC3............proved - complete [shostak](-1.45 s) conflict_3D_2D_stable.................proved - complete [shostak](4.06 s) conflict_3D_vz_swap...................proved - complete [shostak](0.22 s) conflict_3D_on_open_interval..........proved - complete [shostak](1.77 s) conflict_3D_vertical_TCC1.............proved - complete [shostak](0.06 s) conflict_3D_vertical_TCC2.............proved - complete [shostak](0.22 s) conflict_3D_vertical..................proved - complete [shostak](0.53 s) detection_TCC1........................proved - complete [shostak](0.23 s) detection_TCC2........................proved - complete [shostak](0.19 s) detection_TCC3........................proved - complete [shostak](0.05 s) detection_TCC4........................proved - complete [shostak](0.04 s) detection_TCC5........................proved - complete [shostak](0.05 s) detection_TCC6........................proved - complete [shostak](0.04 s) detection_TCC7........................proved - complete [shostak](0.12 s) detection_TCC8........................proved - complete [shostak](0.12 s) detection_TCC9........................proved - complete [shostak](0.10 s) detection_TCC10.......................proved - complete [shostak](0.09 s) detection_TCC11.......................proved - complete [shostak](0.85 s) detection_TCC12.......................proved - complete [shostak](0.34 s) detection_correct.....................proved - complete [shostak](6.01 s) detection_complete....................proved - complete [shostak](5.11 s) conflict_detection....................proved - complete [shostak](0.29 s) cd3d_rewrite_TCC1.....................proved - complete [shostak](0.08 s) cd3d_rewrite_TCC2.....................proved - complete [shostak](0.17 s) cd3d_rewrite..........................proved - complete [shostak](4.75 s) cd3d_test.............................proved - complete [shostak](1.20 s) cd3d_correct..........................proved - complete [shostak](0.34 s) cd3d_complete.........................proved - complete [shostak](1.35 s) cd3d..................................proved - complete [shostak](0.03 s) cd3d_rewrite_vertical_TCC1............proved - complete [shostak](0.04 s) cd3d_rewrite_vertical_TCC2............proved - complete [shostak](0.07 s) cd3d_rewrite_vertical_TCC3............proved - complete [shostak](0.21 s) cd3d_rewrite_vertical.................proved - complete [shostak](0.94 s) vertical_solution_not_conflict_3D.....proved - complete [shostak](0.13 s) conflict_3D_horizontal_conflict.......proved - complete [shostak](0.09 s) conflict_3D_vertical_conflict.........proved - complete [shostak](0.11 s) circle_solution_2D_not_conflict_3D....proved - complete [shostak](0.12 s) Theory totals: 39 formulas, 39 attempted, 39 succeeded (29.16 s) Proof summary for theory circle_criterion vertical_sep_independence.............proved - complete [shostak](0.08 s) nogs_criterion_independence...........proved - complete [shostak](0.26 s) circle_criterion_independence.........proved - complete [shostak](0.26 s) circle_criterion_at_independence......proved - complete [shostak](0.04 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.64 s) Proof summary for theory vz_criteria vertical_exit_independence............proved - complete [shostak](0.26 s) vertical_exit_coordination............proved - complete [shostak](0.33 s) vertical_sep_dir_at...................proved - complete [shostak](2.88 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (3.47 s) Proof summary for theory cd_vertical cd_vertical_rewrite...................proved - complete [shostak](1.51 s) cd_vertical_correct...................proved - complete [shostak](0.44 s) cd_vertical_complete..................proved - complete [shostak](0.29 s) cd_vertical...........................proved - complete [shostak](0.03 s) conflict_vertical_on_open_interval....proved - complete [shostak](1.55 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (3.82 s) Proof summary for theory Lookahead Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory omega_2D IMP_metric_space_real_fun_TCC1........proved - complete [shostak](0.02 s) IMP_ms_composition_cont_TCC1..........proved - complete [shostak](0.02 s) IMP_ms_composition_cont_TCC2..........proved - complete [shostak](0.03 s) horiz_dist_cont_scaf..................proved - complete [shostak](1.25 s) conflict_2D_on_open_interval..........proved - complete [shostak](1.03 s) circle_hit............................proved - complete [shostak](0.38 s) horiz_dist_scaf_bounded_below.........proved - complete [shostak](0.05 s) omega_2D_TCC1.........................proved - complete [shostak](0.05 s) omega_2D_TCC2.........................proved - complete [shostak](0.03 s) tau_2D_nonempty.......................proved - incomplete [shostak](0.28 s) tau_2D_TCC1...........................proved - incomplete [shostak](0.02 s) tau_2D_def............................proved - incomplete [shostak](0.04 s) omega_2D_min_rew_TCC1.................proved - incomplete [shostak](0.17 s) omega_2D_min_rew......................proved - incomplete [shostak](0.30 s) tau_2D_min............................proved - incomplete [shostak](0.22 s) omega_2D_continuous...................proved - incomplete [shostak](0.29 s) tau_2D_unique.........................proved - incomplete [shostak](0.13 s) tau_2D_connected......................proved - incomplete [shostak](0.15 s) tau_2D_v2.............................proved - incomplete [shostak](0.08 s) omega_2D_horizontal_omega.............proved - incomplete [shostak](0.06 s) omega_2D_conflict.....................proved - incomplete [shostak](0.07 s) omega_2D_eq_0.........................proved - incomplete [shostak](0.04 s) parts_of_v_nonzero_2D.................proved - incomplete [shostak](0.04 s) lower_circle_hit_solution.............proved - incomplete [shostak](0.87 s) circle_hit_solution...................proved - incomplete [shostak](0.99 s) no_horiz_speed_on_D...................proved - incomplete [shostak](0.05 s) omega_2D_Delta........................proved - incomplete [shostak](0.12 s) Theta_Ds_equal_line_sol_2D_TCC1.......proved - incomplete [shostak](0.06 s) Theta_Ds_equal_line_sol_2D_TCC2.......proved - complete [shostak](0.95 s) Theta_Ds_equal_line_sol_2D............proved - incomplete [shostak](0.30 s) critical_points_2D....................proved - incomplete [shostak](0.07 s) Theory totals: 31 formulas, 31 attempted, 31 succeeded (8.15 s) Proof summary for theory cd2d conflict_2D_horizontal................proved - complete [shostak](0.03 s) on_D_conflict.........................proved - complete [shostak](1.74 s) tau_v2_TCC1...........................proved - complete [shostak](0.09 s) tau_vv................................proved - complete [shostak](0.18 s) tau_vv_continuous.....................proved - complete [shostak](0.16 s) horizontal_omega_min..................proved - complete [shostak](0.66 s) horizontal_omega_conflict.............proved - complete [shostak](0.07 s) omega_vv_continuous...................proved - complete [shostak](0.25 s) omega_vv..............................proved - complete [shostak](0.39 s) omega_vv_conflict.....................proved - complete [shostak](0.23 s) omega_vv_zero_TCC1....................proved - complete [shostak](0.05 s) omega_vv_zero.........................proved - complete [shostak](0.26 s) omega_half_line.......................proved - complete [shostak](2.40 s) detection_2D_TCC1.....................proved - complete [shostak](0.04 s) detection_2D_TCC2.....................proved - complete [shostak](0.03 s) detection_2D_TCC3.....................proved - complete [shostak](0.03 s) detection_2D_TCC4.....................proved - complete [shostak](0.58 s) detection_2D_TCC5.....................proved - complete [shostak](0.58 s) detection_2D_TCC6.....................proved - complete [shostak](0.03 s) detection_2D_correct..................proved - complete [shostak](0.30 s) detection_2D_complete.................proved - complete [shostak](-1.71 s) conflict_detection_2D.................proved - complete [shostak](0.22 s) cd2d..................................proved - complete [shostak](0.06 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (6.67 s) Proof summary for theory cd3d_ever conflict_2D_stable_TCC1...............proved - complete [shostak](0.10 s) conflict_2D_stable_TCC2...............proved - complete [shostak](0.17 s) conflict_2D_stable_TCC3...............proved - complete [shostak](0.09 s) conflict_2D_stable....................proved - complete [shostak](2.62 s) conflict_vz_swap......................proved - complete [shostak](0.19 s) conflict_on_open_interval.............proved - complete [shostak](0.96 s) cd3d_ever_rewrite_TCC1................proved - complete [shostak](0.06 s) cd3d_ever_rewrite_TCC2................proved - complete [shostak](0.08 s) cd3d_ever_rewrite.....................proved - complete [shostak](3.48 s) cd3d_ever_correct.....................proved - complete [shostak](0.23 s) cd3d_ever_complete....................proved - complete [shostak](0.68 s) cd3d_ever.............................proved - complete [shostak](0.03 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (8.68 s) Proof summary for theory cd2d_ever cd2d_ever_def.........................proved - complete [shostak](1.23 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (1.23 s) Proof summary for theory omega_v2 omega_v2_generic......................proved - complete [shostak](0.03 s) omega_v2_conflict.....................proved - incomplete [shostak](0.05 s) omega_v2_2D_eq_0......................proved - incomplete [shostak](0.13 s) omega_v2_critical_points..............proved - incomplete [shostak](0.11 s) omega_v2_continuous...................proved - incomplete [shostak](0.83 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.15 s) Proof summary for theory horizontal_sq_dtca IMP_vect_deriv_2D_TCC1................proved - complete [shostak](0.06 s) IMP_vect_deriv_2D_TCC2................proved - complete [shostak](0.02 s) horizontal_sq_dtca_diff_TCC1..........proved - complete [shostak](0.02 s) horizontal_sq_dtca_diff...............proved - complete [shostak](0.10 s) horizontal_sq_dtca_deriv_TCC1.........proved - complete [shostak](0.03 s) horizontal_sq_dtca_deriv_TCC2.........proved - complete [shostak](0.04 s) horizontal_sq_dtca_deriv..............proved - complete [shostak](0.50 s) horizontal_sq_dtca_deriv_simpl........proved - complete [shostak](1.88 s) horizontal_sq_dtca_deriv_sign_TCC1....proved - complete [shostak](0.03 s) horizontal_sq_dtca_deriv_sign.........proved - complete [shostak](2.12 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (4.80 s) Proof summary for theory cd2d_inf detection_2D_inf_TCC1.................proved - complete [shostak](0.28 s) detection_2D_inf_correct..............proved - complete [shostak](0.08 s) detection_2D_inf_complete.............proved - complete [shostak](0.09 s) conflict_detection_2D_inf.............proved - complete [shostak](0.10 s) cd2d_inf..............................proved - complete [shostak](0.15 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.70 s) Proof summary for theory cd3d_inf conflict_3D_2D_inf_stable_TCC1........proved - complete [shostak](0.10 s) conflict_3D_2D_inf_stable_TCC2........proved - complete [shostak](0.13 s) conflict_3D_2D_inf_stable_TCC3........proved - complete [shostak](0.13 s) conflict_3D_2D_inf_stable.............proved - complete [shostak](2.20 s) conflict_vz_swap......................proved - complete [shostak](0.20 s) conflict_on_open_interval.............proved - complete [shostak](1.32 s) detection_inf_TCC1....................proved - complete [shostak](0.05 s) detection_inf_TCC2....................proved - complete [shostak](0.41 s) detection_inf_TCC3....................proved - complete [shostak](0.21 s) detection_inf_TCC4....................proved - complete [shostak](0.07 s) detection_inf_TCC5....................proved - complete [shostak](1.59 s) detection_inf_TCC6....................proved - complete [shostak](1.63 s) detection_inf_correct.................proved - complete [shostak](2.00 s) detection_inf_complete................proved - complete [shostak](2.41 s) conflict_detection_inf................proved - complete [shostak](-1.71 s) cd3d_inf_rewrite_TCC1.................proved - complete [shostak](0.18 s) cd3d_inf_rewrite_TCC2.................proved - complete [shostak](0.18 s) cd3d_inf_rewrite......................proved - complete [shostak](3.40 s) cd3d_inf_correct......................proved - complete [shostak](0.25 s) cd3d_inf_complete.....................proved - complete [shostak](4.77 s) cd3d_inf..............................proved - complete [shostak](0.03 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (19.55 s) Proof summary for theory bands_util trk2v2_TCC1...........................proved - incomplete [shostak](0.24 s) trk2v2_Nzv............................proved - incomplete [shostak](0.05 s) gs2v2_gs_only.........................proved - complete [shostak](0.09 s) gs2v2_id..............................proved - complete [shostak](0.12 s) trk2v3_TCC1...........................proved - incomplete [shostak](0.20 s) vect2_trk2v3..........................proved - incomplete [shostak](0.04 s) trk2v3_Nzv............................proved - incomplete [shostak](0.03 s) Vtrk_3D_TCC1..........................proved - incomplete [shostak](0.24 s) trk2v3_trk2v3.........................proved - incomplete [shostak](0.38 s) trk2v3_0..............................proved - incomplete [shostak](0.08 s) gs2v3_gs_only.........................proved - complete [shostak](0.09 s) vect2_gs2v3...........................proved - complete [shostak](0.03 s) Vgs_3D_TCC1...........................proved - complete [shostak](0.11 s) vs2v3_TCC1............................proved - complete [shostak](0.03 s) vect2_vs2v3...........................proved - complete [shostak](0.03 s) Vs_TCC1...............................proved - complete [shostak](0.04 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (1.81 s) Proof summary for theory track trkgs2vect_TCC1.......................proved - incomplete [shostak](0.60 s) track_TCC1............................proved - complete [shostak](0.04 s) sin_track.............................proved - incomplete [shostak](3.70 s) cos_track.............................proved - incomplete [shostak](2.08 s) norm_id...............................proved - incomplete [shostak](0.23 s) track_id..............................proved - incomplete [shostak](0.09 s) trkgs2vect_id.........................proved - incomplete [shostak](0.08 s) ordered_eps_1_TCC1....................proved - incomplete [shostak](0.45 s) ordered_eps_1.........................proved - incomplete [shostak](2.29 s) ordered_det_ge........................proved - incomplete [shostak](-.13 s) ordered_eps_neg_1.....................proved - incomplete [shostak](0.33 s) ordered_eps_1_dot_gt_0................proved - incomplete [shostak](3.19 s) ordered_eps_1_dot_ge_0................proved - incomplete [shostak](2.91 s) ordered_eps_1_dot_lt_0................proved - incomplete [shostak](1.08 s) ordered_eps_1_dot_le_0................proved - incomplete [shostak](1.09 s) Theory totals: 15 formulas, 15 attempted, 15 succeeded (18.03 s) Proof summary for theory gs_bands_2D gs_band_pos...........................proved - complete [shostak](0.03 s) gs2v2_continuous......................proved - complete [shostak](0.05 s) Vgs_continuous........................proved - complete [shostak](0.06 s) Omega_gs_TCC1.........................proved - incomplete [shostak](0.54 s) Omega_gs_critical.....................proved - incomplete [shostak](0.10 s) gs_green_two_parallel.................proved - complete [shostak](0.29 s) gs_line_color.........................proved - complete [shostak](3.60 s) gs_green_band.........................proved - incomplete [shostak](0.13 s) gs_red_band...........................proved - incomplete [shostak](0.10 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (4.90 s) Proof summary for theory trk_bands_2D trk_band..............................proved - complete [shostak](0.47 s) trk2v2_continuous.....................proved - incomplete [shostak](0.07 s) Vtrk_continuous.......................proved - incomplete [shostak](0.06 s) Omega_trk_spc.........................proved - incomplete [shostak](0.10 s) trk_special_case_invariant............proved - incomplete [shostak](0.09 s) Omega_trk_spc_separated...............proved - incomplete [shostak](0.71 s) Omega_trk_spc_critical_TCC1...........proved - incomplete [shostak](0.05 s) Omega_trk_spc_critical................proved - incomplete [shostak](0.12 s) trk_special_case_conflict_T...........proved - incomplete [shostak](0.36 s) trk_special_case_conflict_B...........proved - incomplete [shostak](0.12 s) Omega_trk_spc_conflict_T..............proved - incomplete [shostak](1.02 s) Omega_trk_spc_conflict_B..............proved - incomplete [shostak](0.89 s) Omega_trk_TCC1........................proved - incomplete [shostak](0.53 s) Omega_trk_critical....................proved - incomplete [shostak](0.11 s) trk_line_sort_eps.....................proved - complete [shostak](0.31 s) trk_line_sort_eps_angle_TCC1..........proved - incomplete [shostak](0.11 s) trk_line_sort_eps_angle_TCC2..........proved - incomplete [shostak](0.17 s) trk_line_sort_eps_angle_TCC3..........proved - incomplete [shostak](0.18 s) trk_line_sort_eps_angle...............proved - incomplete [shostak](0.43 s) trk_line_sort_eps_1_angle_case1_TCC1...proved - incomplete [shostak](0.09 s) trk_line_sort_eps_1_angle_case1_TCC2...proved - incomplete [shostak](0.08 s) trk_line_sort_eps_1_angle_case1.......proved - incomplete [shostak](0.45 s) trk_line_sort_eps_1_angle_case2_TCC1...proved - incomplete [shostak](0.08 s) trk_line_sort_eps_1_angle_case2_TCC2...proved - incomplete [shostak](0.08 s) trk_line_sort_eps_1_angle_case2.......proved - incomplete [shostak](2.10 s) trk_line_color........................proved - complete [shostak](3.02 s) trk_green_band........................proved - incomplete [shostak](0.51 s) trk_red_band..........................proved - incomplete [shostak](0.51 s) Theory totals: 28 formulas, 28 attempted, 28 succeeded (12.83 s) Proof summary for theory bands_2D trk_critical_TCC1....................proved - incomplete [shostak]( 0.15 s) trk_critical_TCC2....................proved - incomplete [shostak]( 0.11 s) trk_critical_rew.....................proved - incomplete [shostak]( 0.88 s) member_trk_critical_TCC1.............proved - incomplete [shostak]( 0.11 s) member_trk_critical..................proved - incomplete [shostak]( 0.10 s) trk_critical_composition.............proved - incomplete [shostak]( 1.05 s) trk_bands_TCC1.......................proved - incomplete [shostak]( 0.23 s) trk_bands_not_empty..................proved - incomplete [shostak](15.79 s) trk_bands_critical...................proved - incomplete [shostak]( 1.53 s) gs_critical_TCC1.....................proved - complete [shostak]( 0.09 s) gs_critical_TCC2.....................proved - complete [shostak]( 0.06 s) gs_critical_rew......................proved - incomplete [shostak]( 0.89 s) member_gs_critical...................proved - incomplete [shostak]( 0.11 s) gs_critical_composition..............proved - incomplete [shostak]( 1.09 s) gs_bands_TCC1........................proved - incomplete [shostak]( 0.06 s) gs_bands_TCC2........................proved - incomplete [shostak]( 0.11 s) gs_bands_TCC3........................proved - incomplete [shostak]( 0.11 s) gs_bands_TCC4........................proved - incomplete [shostak]( 0.15 s) gs_bands_not_empty...................proved - incomplete [shostak]( 2.65 s) gs_bands_critical_TCC1...............proved - complete [shostak]( 0.04 s) gs_bands_critical....................proved - incomplete [shostak]( 1.01 s) red_trk_band?_TCC1...................proved - incomplete [shostak]( 0.04 s) red_trk_band?_TCC2...................proved - incomplete [shostak]( 0.07 s) trk_red_bands........................proved - incomplete [shostak]( 0.39 s) trk_green_bands......................proved - incomplete [shostak]( 0.41 s) red_gs_band?_TCC1....................proved - complete [shostak]( 0.04 s) red_gs_band?_TCC2....................proved - complete [shostak]( 0.07 s) gs_red_bands.........................proved - incomplete [shostak]( 0.37 s) gs_green_bands.......................proved - incomplete [shostak]( 0.41 s) Theory totals: 29 formulas, 29 attempted, 29 succeeded (28.14 s) Proof summary for theory fseqs_aux_2D empty_trk_fseq........................proved - incomplete [shostak](0.08 s) comp_trk_fseq.........................proved - incomplete [shostak](1.14 s) sort_trk_fseq.........................proved - incomplete [shostak](0.12 s) empty_gs_fseq.........................proved - incomplete [shostak](0.04 s) comp_gs_fseq..........................proved - complete [shostak](1.06 s) sort_gs_fseq..........................proved - complete [shostak](0.08 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.52 s) Proof summary for theory vertical_criterion closed_region_3D_t_def................proved - complete [shostak](0.12 s) closed_region_3D_t_direction..........proved - complete [shostak](1.35 s) closed_region_3D_sum_closed...........proved - complete [shostak](3.00 s) vertical_criterion?_TCC1..............proved - complete [shostak](0.08 s) vertical_criterion_sum_closed.........proved - complete [shostak](0.45 s) vertical_criterion_antisymmetric......proved - complete [shostak](1.41 s) vertical_criterion_independence.......proved - complete [shostak](5.49 s) vertical_criterion_coordination.......proved - complete [shostak](0.09 s) horizontal_meets_vertical_criterion_TCC1...proved - complete [shostak](0.09 s) horizontal_meets_vertical_criterion_TCC2...proved - complete [shostak](0.06 s) horizontal_meets_vertical_criterion...proved - complete [shostak](2.14 s) safe_p_TCC1...........................proved - complete [shostak](0.04 s) vertical_criterion_rewrite_TCC1.......proved - complete [shostak](0.04 s) --> -------------------- --> maximum size reached --> -------------------- [ Verzeichnis aufwärts0.234unsichere Verbindung ] |