| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: finite_sets_card_from.prf Sprache: Lisp
|
Untersuchungsergebnis.summary Download desMT940 {MT940[881] Hlasm[2385] Haskell[2705]}zum Wurzelverzeichnis wechseln *** *** top (18:17:21 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 interval Member_Proper.........................proved - complete [shostak](0.05 s) Proper_Member.........................proved - complete [shostak](0.04 s) r2i_Proper............................proved - complete [shostak](0.02 s) Proper_eq_NonEmpty....................proved - complete [shostak](0.02 s) Proper_NonEmpty.......................proved - complete [shostak](0.02 s) eq_Incl...............................proved - complete [shostak](0.05 s) Incl_Member...........................proved - complete [shostak](0.04 s) Member_Incl...........................proved - complete [shostak](0.04 s) Incl_Proper...........................proved - complete [shostak](0.03 s) midpoint_inclusion....................proved - complete [shostak](0.05 s) Lt_Ge.................................proved - complete [shostak](0.03 s) Le_Gt.................................proved - complete [shostak](0.03 s) Trichotomy............................proved - complete [shostak](0.05 s) Abs_TCC1..............................proved - complete [shostak](0.06 s) Abs_TCC2..............................proved - complete [shostak](0.09 s) Sq_TCC1...............................proved - complete [shostak](0.03 s) Sq_TCC2...............................proved - complete [shostak](0.02 s) Sq_TCC3...............................proved - complete [shostak](0.05 s) Pow_TCC1..............................proved - complete [shostak](0.06 s) Pow_TCC2..............................proved - complete [shostak](0.05 s) Pow_TCC3..............................proved - complete [shostak](0.06 s) Pow_TCC4..............................proved - complete [shostak](0.05 s) Pow_TCC5..............................proved - complete [shostak](0.06 s) Pow_TCC6..............................proved - complete [shostak](0.05 s) Intersection_inclusion................proved - complete [shostak](0.08 s) Intersection_left_Empty...............proved - complete [shostak](0.04 s) Intersection_right_Empty..............proved - complete [shostak](0.04 s) Add_comm..............................proved - complete [shostak](0.02 s) Mult_comm.............................proved - complete [shostak](-1.30 s) Neg_Incl..............................proved - complete [shostak](0.03 s) Zeroless0.............................proved - complete [shostak](0.03 s) Neg_Ge_0..............................proved - complete [shostak](0.03 s) Strict_Lt.............................proved - complete [shostak](0.04 s) Halves................................proved - complete [shostak](0.09 s) Halves_Incl...........................proved - complete [shostak](0.05 s) Halves_inclusion......................proved - complete [shostak](0.06 s) Incl_trans............................proved - complete [shostak](0.04 s) Pow2_Sq...............................proved - complete [shostak](0.07 s) Mult_Neg_Neg..........................proved - complete [shostak](0.98 s) Mult_Neg_left.........................proved - complete [shostak](0.79 s) Mult_Neg_right........................proved - complete [shostak](0.54 s) Sq_Neg_eq.............................proved - complete [shostak](0.13 s) Union_id..............................proved - complete [shostak](0.04 s) Union_symm............................proved - complete [shostak](0.06 s) Union_Incl_left.......................proved - complete [shostak](0.03 s) Union_Incl_right......................proved - complete [shostak](0.04 s) Add_0_r...............................proved - complete [shostak](0.03 s) Add_0_l...............................proved - complete [shostak](0.06 s) Mult_1_r..............................proved - complete [shostak](0.10 s) Mult_1_l..............................proved - complete [shostak](0.09 s) Div_1.................................proved - complete [shostak](0.09 s) Pow_0.................................proved - complete [shostak](0.03 s) Pow_1.................................proved - complete [shostak](0.09 s) lb_interval...........................proved - complete [shostak](0.02 s) lb_r2i................................proved - complete [shostak](0.02 s) ub_interval...........................proved - complete [shostak](0.02 s) ub_r2i................................proved - complete [shostak](0.01 s) Incl_reflx............................proved - complete [shostak](0.02 s) Incl_r2i..............................proved - complete [shostak](0.02 s) Neg_Neg...............................proved - complete [shostak](0.04 s) ub_inclusion..........................proved - complete [shostak](0.02 s) lb_inclusion..........................proved - complete [shostak](0.02 s) Neg_interval..........................proved - complete [shostak](0.02 s) Pos_Gt_0..............................proved - complete [shostak](0.03 s) NonNeg_Ge_0...........................proved - complete [shostak](0.02 s) Pos_Neg_Lt_0..........................proved - complete [shostak](0.03 s) NonNeg_Neg_Le_0.......................proved - complete [shostak](0.03 s) r2i_sharp_eq..........................proved - complete [shostak](0.04 s) r2i_Le................................proved - complete [shostak](0.02 s) r2i_Lt................................proved - complete [shostak](0.03 s) r2i_Ge................................proved - complete [shostak](0.03 s) r2i_Gt................................proved - complete [shostak](0.03 s) Lt_Le.................................proved - complete [shostak](0.03 s) Gt_Ge.................................proved - complete [shostak](0.03 s) inclusion_Gt..........................proved - complete [shostak](0.03 s) inclusion_Ge..........................proved - complete [shostak](0.03 s) inclusion_Lt..........................proved - complete [shostak](0.04 s) inclusion_Le..........................proved - complete [shostak](0.03 s) r2i_trans.............................proved - complete [shostak](0.04 s) add2sub...............................proved - complete [shostak](0.06 s) sub2add...............................proved - complete [shostak](0.06 s) Member_trans..........................proved - complete [shostak](0.04 s) r2i_inclusion.........................proved - complete [shostak](0.02 s) Add_inclusion.........................proved - complete [shostak](0.06 s) Sub_inclusion.........................proved - complete [shostak](0.06 s) Neg_inclusion.........................proved - complete [shostak](0.03 s) pXp...................................proved - complete [shostak](0.23 s) nXp...................................proved - complete [shostak](0.06 s) pXn...................................proved - complete [shostak](0.04 s) nXn...................................proved - complete [shostak](0.23 s) pXm...................................proved - complete [shostak](0.49 s) mXp...................................proved - complete [shostak](0.04 s) nXm...................................proved - complete [shostak](0.05 s) mXn...................................proved - complete [shostak](0.03 s) mXm...................................proved - complete [shostak](1.89 s) Mult_inclusion........................proved - complete [shostak](0.77 s) Abs_inclusion.........................proved - complete [shostak](0.15 s) abs_sharp_le..........................proved - complete [shostak](0.04 s) abs_sharp_lt..........................proved - complete [shostak](0.04 s) pow_0_0...............................proved - complete [shostak](0.03 s) pow_sq_TCC1...........................proved - complete [shostak](0.02 s) pow_sq................................proved - complete [shostak](0.03 s) pow_neg_n_odd_TCC1....................proved - complete [shostak](0.05 s) pow_neg_n_odd_TCC2....................proved - complete [shostak](0.06 s) pow_neg_n_odd.........................proved - complete [shostak](0.28 s) pow_neg_odd_TCC1......................proved - complete [shostak](0.06 s) pow_neg_odd_TCC2......................proved - complete [shostak](0.05 s) pow_neg_odd...........................proved - complete [shostak](0.11 s) pow_neg_n_even_TCC1...................proved - complete [shostak](0.02 s) pow_neg_n_even_TCC2...................proved - complete [shostak](0.02 s) pow_neg_n_even........................proved - complete [shostak](0.12 s) pow_neg_even_TCC1.....................proved - complete [shostak](0.03 s) pow_neg_even_TCC2.....................proved - complete [shostak](0.02 s) pow_neg_even..........................proved - complete [shostak](0.07 s) pow_pos_TCC1..........................proved - complete [shostak](0.02 s) pow_pos...............................proved - complete [shostak](0.07 s) pow_even_n_pos........................proved - complete [shostak](0.07 s) pow_even_pos..........................proved - complete [shostak](0.06 s) pow_odd_n_neg.........................proved - complete [shostak](0.22 s) pow_odd_neg...........................proved - complete [shostak](0.09 s) pow_incr_pos_TCC1.....................proved - complete [shostak](0.02 s) pow_incr_pos..........................proved - complete [shostak](0.12 s) pow_incr_odd_TCC1.....................proved - complete [shostak](0.06 s) pow_incr_odd..........................proved - complete [shostak](0.19 s) pow_decr_even_TCC1....................proved - complete [shostak](0.02 s) pow_decr_even.........................proved - complete [shostak](0.13 s) Pow_Neg_even..........................proved - complete [shostak](0.46 s) Pow_inclusion_TCC1....................proved - complete [shostak](0.02 s) Pow_inclusion.........................proved - complete [shostak](0.25 s) Sq_inclusion..........................proved - complete [shostak](0.09 s) Div_inclusion_TCC1....................proved - complete [shostak](0.04 s) Div_inclusion.........................proved - complete [shostak](0.36 s) Union_inclusion.......................proved - complete [shostak](0.07 s) Reunion...............................proved - complete [shostak](0.27 s) Sigma_TCC1............................proved - complete [shostak](0.03 s) Sigma_TCC2............................proved - complete [shostak](0.06 s) Sigma_inclusion_TCC1..................proved - complete [shostak](0.02 s) Sigma_inclusion_TCC2..................proved - complete [shostak](0.04 s) Sigma_inclusion.......................proved - complete [shostak](0.24 s) Add_fundamental.......................proved - complete [shostak](0.07 s) Sub_fundamental.......................proved - complete [shostak](0.05 s) Abs_fundamental.......................proved - complete [shostak](0.35 s) Neg_fundamental.......................proved - complete [shostak](0.03 s) pXp_fundamental.......................proved - complete [shostak](0.50 s) pXpm_fundamental......................proved - complete [shostak](0.61 s) pXmm_fundamental......................proved - complete [shostak](0.66 s) pX_fundamental........................proved - complete [shostak](1.31 s) nX_fundamental........................proved - complete [shostak](0.14 s) pmXpm_fundamental.....................proved - complete [shostak](0.93 s) pmXmm_fundamental.....................proved - complete [shostak](0.81 s) mmXmm_fundamental.....................proved - complete [shostak](1.51 s) mX_fundamental........................proved - complete [shostak](2.17 s) Mult_fundamental......................proved - complete [shostak](0.07 s) Sq_p_fundamental......................proved - complete [shostak](0.24 s) Sq_pm_fundamental.....................proved - complete [shostak](0.29 s) Sq_fundamental........................proved - complete [shostak](0.75 s) Div_fundamental.......................proved - complete [shostak](0.62 s) Pow_p_fundamental.....................proved - complete [shostak](0.12 s) Pow_pm_fundamental....................proved - complete [shostak](0.18 s) Pow_m_fundamental.....................proved - complete [shostak](0.54 s) Pow_fundamental.......................proved - complete [shostak](0.23 s) Union_fundamental.....................proved - complete [shostak](0.09 s) Mult_Strict_r2i.......................proved - complete [shostak](0.65 s) Mult_r2i_Strict.......................proved - complete [shostak](0.65 s) Pos_Zeroless..........................proved - complete [shostak](0.03 s) Neg_Zeroless..........................proved - complete [shostak](0.03 s) Pos_NonNeg............................proved - complete [shostak](0.03 s) Pos_Add_NonNeg........................proved - complete [shostak](0.06 s) NonNeg_Add_Pos........................proved - complete [shostak](0.07 s) Neg_Add...............................proved - complete [shostak](0.07 s) NonNeg_Add............................proved - complete [shostak](0.07 s) Neg_Pos...............................proved - complete [shostak](0.03 s) Pos_Neg...............................proved - complete [shostak](0.03 s) Pos_Mult..............................proved - complete [shostak](0.87 s) Neg_Mult..............................proved - complete [shostak](0.85 s) NonNeg_Mult...........................proved - complete [shostak](-1.28 s) Pos_Div...............................proved - complete [shostak](1.50 s) Neg_Div...............................proved - complete [shostak](1.64 s) NonNeg_Div............................proved - complete [shostak](0.80 s) r2i_Pos...............................proved - complete [shostak](0.02 s) r2i_Neg...............................proved - complete [shostak](0.03 s) r2i_Nneg..............................proved - complete [shostak](0.02 s) Sq_Pos................................proved - complete [shostak](0.20 s) Sq_Neg................................proved - complete [shostak](0.19 s) Abs_Pos...............................proved - complete [shostak](0.10 s) Abs_Neg...............................proved - complete [shostak](0.10 s) Proper_midpoint.......................proved - complete [shostak](0.06 s) Includes_Proper.......................proved - complete [shostak](0.04 s) Strict_Proper.........................proved - complete [shostak](0.04 s) Strict_Add............................proved - complete [shostak](0.06 s) Add_Strict............................proved - complete [shostak](0.06 s) Proper_Add............................proved - complete [shostak](0.07 s) Strict_Sub............................proved - complete [shostak](0.05 s) Sub_Strict............................proved - complete [shostak](0.05 s) Proper_Sub............................proved - complete [shostak](0.05 s) Strict_Neg............................proved - complete [shostak](0.03 s) Proper_Neg............................proved - complete [shostak](0.04 s) Strict_Abs............................proved - complete [shostak](0.09 s) Proper_Abs............................proved - complete [shostak](0.11 s) Proper_Mult...........................proved - complete [shostak](0.06 s) Proper_Div............................proved - complete [shostak](0.08 s) Strict_Sq.............................proved - complete [shostak](0.27 s) Proper_Pow............................proved - complete [shostak](0.06 s) Proper_Sq.............................proved - complete [shostak](0.27 s) Proper_size...........................proved - complete [shostak](0.05 s) Strict_size...........................proved - complete [shostak](0.04 s) Proper_HalfLeft.......................proved - complete [shostak](0.07 s) Strict_HalfLeft.......................proved - complete [shostak](0.07 s) Proper_HalfRight......................proved - complete [shostak](0.07 s) Strict_HalfRightt.....................proved - complete [shostak](0.07 s) Zeroless_Precondition.................proved - complete [shostak](0.05 s) NonNeg_Precondition...................proved - complete [shostak](0.05 s) Pos_Precondition......................proved - complete [shostak](0.05 s) Neg_Precondition......................proved - complete [shostak](0.05 s) Theory totals: 214 formulas, 214 attempted, 214 succeeded (33.64 s) Proof summary for theory proper_arith Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory safe_arith Proper_Safe1..........................proved - complete [shostak](0.03 s) Proper_Safe1_pre......................proved - complete [shostak](0.04 s) Proper_Safe2..........................proved - complete [shostak](0.04 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.11 s) Proof summary for theory box proper_box............................proved - complete [shostak](0.03 s) proper_append.........................proved - complete [shostak](0.22 s) vars_in_box_rec_TCC1..................proved - complete [shostak](0.03 s) vars_in_box_rec_TCC2..................proved - complete [shostak](0.02 s) vars_in_box_rec_TCC3..................proved - complete [shostak](0.07 s) vars_in_box_rec_TCC4..................proved - complete [shostak](0.14 s) vars_in_box_rec_TCC5..................proved - complete [shostak](0.08 s) vars_in_box_rec_TCC6..................proved - complete [shostak](0.33 s) vars_in_box...........................proved - complete [shostak](0.45 s) midvars_TCC1..........................proved - complete [shostak](0.04 s) Lbbox_TCC1............................proved - complete [shostak](0.02 s) length_Lbbox..........................proved - complete [shostak](0.03 s) Ubbox_TCC1............................proved - complete [shostak](0.02 s) length_Ubbox..........................proved - complete [shostak](0.02 s) Midbox_TCC1...........................proved - complete [shostak](0.03 s) length_Midbox.........................proved - complete [shostak](0.02 s) Inclusion?_TCC1.......................proved - complete [shostak](0.03 s) Inclusion_reflx.......................proved - complete [shostak](0.03 s) Inclusion_trans.......................proved - complete [shostak](0.06 s) Inclusion_Proper......................proved - complete [shostak](0.06 s) Lbbox_Proper..........................proved - complete [shostak](0.10 s) Ubbox_Proper..........................proved - complete [shostak](0.09 s) Midbox_Proper.........................proved - complete [shostak](0.16 s) Lbbox_Inclusion.......................proved - complete [shostak](0.07 s) Ubbox_Inclusion.......................proved - complete [shostak](0.08 s) Midbox_Inclusion......................proved - complete [shostak](0.10 s) vars_in_box_Inclusion.................proved - complete [shostak](0.07 s) Theory totals: 27 formulas, 27 attempted, 27 succeeded (2.40 s) Proof summary for theory interval_expr r2E_TCC1..............................proved - complete [shostak](0.02 s) I2E_TCC1..............................proved - complete [shostak](0.06 s) PreTrue_TCC1..........................proved - complete [shostak](0.02 s) real_bool_expr........................proved - complete [shostak](0.19 s) eval_TCC1.............................proved - complete [shostak](0.07 s) eval_TCC2.............................proved - complete [shostak](0.06 s) eval_TCC3.............................proved - complete [shostak](0.07 s) eval_TCC4.............................proved - complete [shostak](0.06 s) eval_TCC5.............................proved - complete [shostak](0.08 s) eval_TCC6.............................proved - complete [shostak](0.07 s) eval_TCC7.............................proved - complete [shostak](0.07 s) eval_TCC8.............................proved - complete [shostak](0.08 s) eval_TCC9.............................proved - complete [shostak](0.07 s) eval_TCC10............................proved - complete [shostak](0.09 s) eval_TCC11............................proved - complete [shostak](0.08 s) eval_TCC12............................proved - complete [shostak](0.08 s) eval_TCC13............................proved - complete [shostak](0.09 s) eval_TCC14............................proved - complete [shostak](0.08 s) eval_TCC15............................proved - complete [shostak](0.09 s) eval_TCC16............................proved - complete [shostak](0.10 s) eval_TCC17............................proved - complete [shostak](0.09 s) eval_TCC18............................proved - complete [shostak](0.10 s) eval_TCC19............................proved - complete [shostak](0.11 s) eval_TCC20............................proved - complete [shostak](0.10 s) eval_TCC21............................proved - complete [shostak](0.13 s) eval_TCC22............................proved - complete [shostak](0.12 s) eval_TCC23............................proved - complete [shostak](0.10 s) eval_TCC24............................proved - complete [shostak](0.09 s) eval_TCC25............................proved - complete [shostak](0.11 s) eval_TCC26............................proved - complete [shostak](0.10 s) eval_TCC27............................proved - complete [shostak](0.12 s) eval_TCC28............................proved - complete [shostak](0.10 s) eval_TCC29............................proved - complete [shostak](0.14 s) eval_TCC30............................proved - complete [shostak](0.08 s) eval_TCC31............................proved - complete [shostak](0.12 s) Eval_TCC1.............................proved - complete [shostak](0.05 s) Eval_TCC2.............................proved - complete [shostak](0.11 s) Eval_TCC3.............................proved - complete [shostak](0.14 s) well_typed?_TCC1......................proved - complete [shostak](0.06 s) well_typed?_TCC2......................proved - complete [shostak](0.09 s) well_typed?_TCC3......................proved - complete [shostak](0.09 s) well_typed?_TCC4......................proved - complete [shostak](0.10 s) well_typed?_TCC5......................proved - complete [shostak](0.10 s) well_typed?_TCC6......................proved - complete [shostak](0.11 s) well_typed?_TCC7......................proved - complete [shostak](0.11 s) well_typed?_TCC8......................proved - complete [shostak](0.13 s) well_typed?_TCC9......................proved - complete [shostak](0.14 s) Proper_well_typed.....................proved - complete [shostak](1.36 s) Eval_inclusion........................proved - complete [shostak](1.78 s) Eval_inclusion_Proper.................proved - complete [shostak](0.04 s) well_typed_Proper.....................proved - complete [shostak](0.03 s) Eval_fundamental_aux..................proved - complete [shostak](2.06 s) well_typed_Inclusion_aux..............proved - complete [shostak](1.74 s) well_typed_Inclusion..................proved - complete [shostak](0.03 s) Proper_Inclusion......................proved - complete [shostak](0.05 s) Eval_fundamental......................proved - complete [shostak](0.05 s) Eval_fundamental_proper...............proved - complete [shostak](0.05 s) split_TCC1............................proved - complete [shostak](0.05 s) split_TCC2............................proved - complete [shostak](0.08 s) split_TCC3............................proved - complete [shostak](0.05 s) split_TCC4............................proved - complete [shostak](0.05 s) split_TCC5............................proved - complete [shostak](0.09 s) split_TCC6............................proved - complete [shostak](0.03 s) split_TCC7............................proved - complete [shostak](0.17 s) split_TCC8............................proved - complete [shostak](0.06 s) split_TCC9............................proved - complete [shostak](0.28 s) split_TCC10...........................proved - complete [shostak](0.04 s) split_TCC11...........................proved - complete [shostak](0.03 s) split_TCC12...........................proved - complete [shostak](0.03 s) split_eq_TCC1.........................proved - complete [shostak](0.03 s) split_eq_TCC2.........................proved - complete [shostak](0.10 s) split_eq_TCC3.........................proved - complete [shostak](0.07 s) split_eq_TCC4.........................proved - complete [shostak](0.07 s) split_vars_in_box.....................proved - complete [shostak](0.17 s) split_Inclusion.......................proved - complete [shostak](0.28 s) split_Proper..........................proved - complete [shostak](0.12 s) length_split_1........................proved - complete [shostak](0.03 s) length_split_2........................proved - complete [shostak](0.04 s) Theory totals: 78 formulas, 78 attempted, 78 succeeded (13.44 s) Proof summary for theory interval_bexpr beval_TCC1...........................proved - complete [shostak]( 0.06 s) beval_TCC2...........................proved - complete [shostak]( 0.06 s) beval_TCC3...........................proved - complete [shostak]( 0.05 s) beval_TCC4...........................proved - complete [shostak]( 0.07 s) beval_TCC5...........................proved - complete [shostak]( 0.07 s) beval_TCC6...........................proved - complete [shostak]( 0.06 s) beval_TCC7...........................proved - complete [shostak]( 0.07 s) beval_TCC8...........................proved - complete [shostak]( 0.08 s) beval_TCC9...........................proved - complete [shostak]( 0.07 s) beval_TCC10..........................proved - complete [shostak]( 0.07 s) beval_TCC11..........................proved - complete [shostak]( 0.09 s) beval_TCC12..........................proved - complete [shostak]( 0.07 s) beval_TCC13..........................proved - complete [shostak]( 0.09 s) beval_TCC14..........................proved - complete [shostak]( 0.20 s) beval_TCC15..........................proved - complete [shostak]( 0.22 s) beval_TCC16..........................proved - complete [shostak]( 0.26 s) beval_TCC17..........................proved - complete [shostak]( 0.32 s) beval_TCC18..........................proved - complete [shostak]( 0.24 s) beval_TCC19..........................proved - complete [shostak]( 0.07 s) beval_TCC20..........................proved - complete [shostak]( 0.10 s) beval_TCC21..........................proved - complete [shostak]( 0.11 s) beval_TCC22..........................proved - complete [shostak]( 0.11 s) BEval_TCC1...........................proved - complete [shostak]( 0.06 s) BEval_TCC2...........................proved - complete [shostak]( 0.07 s) BEval_TCC3...........................proved - complete [shostak]( 0.08 s) BEval_TCC4...........................proved - complete [shostak]( 0.08 s) BEval_TCC5...........................proved - complete [shostak]( 0.08 s) BEval_TCC6...........................proved - complete [shostak]( 0.08 s) BEval_TCC7...........................proved - complete [shostak]( 0.09 s) BEval_TCC8...........................proved - complete [shostak]( 0.22 s) BEval_TCC9...........................proved - complete [shostak]( 0.24 s) BEval_TCC10..........................proved - complete [shostak]( 0.25 s) BEval_TCC11..........................proved - complete [shostak]( 0.12 s) BEval_TCC12..........................proved - complete [shostak]( 0.12 s) BEval_TCC13..........................proved - complete [shostak]( 0.12 s) BEval_TCC14..........................proved - complete [shostak]( 0.13 s) BEval_inclusion......................proved - complete [shostak]( 3.18 s) BEval_inclusion_Proper...............proved - complete [shostak]( 0.04 s) BEval_fundamental....................proved - complete [shostak](18.51 s) Theory totals: 39 formulas, 39 attempted, 39 succeeded (26.01 s) Proof summary for theory simple_bandb altvar_TCC1...........................proved - complete [shostak](0.14 s) altvar_TCC2...........................proved - complete [shostak](0.22 s) simple_interval_soundness.............proved - complete [shostak](0.86 s) simple_test...........................proved - complete [shostak](1.10 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (2.31 s) Proof summary for theory numerical_bandb evaluate_TCC1.........................proved - complete [shostak](0.05 s) evaluate_TCC2.........................proved - complete [shostak](0.05 s) mindir_maxvar_aux_TCC1................proved - complete [shostak](0.07 s) mindir_maxvar_aux_TCC2................proved - complete [shostak](0.74 s) max_rec_TCC1..........................proved - complete [shostak](0.03 s) max_rec_TCC2..........................proved - complete [shostak](0.11 s) max_rec_TCC3..........................proved - complete [shostak](0.12 s) max_rec_TCC4..........................proved - complete [shostak](0.09 s) max_rec_TCC5..........................proved - complete [shostak](0.12 s) max_rec_TCC6..........................proved - complete [shostak](0.11 s) max_rec_TCC7..........................proved - complete [shostak](0.12 s) max_rec_TCC8..........................proved - complete [shostak](0.09 s) max_rec_TCC9..........................proved - complete [shostak](-1.59 s) max_rec_TCC10.........................proved - complete [shostak](0.11 s) max_rec_TCC11.........................proved - complete [shostak](0.08 s) max_aux_TCC1..........................proved - complete [shostak](0.03 s) max_aux_TCC2..........................proved - complete [shostak](0.04 s) max_aux_TCC3..........................proved - complete [shostak](0.03 s) max_aux_TCC4..........................proved - complete [shostak](0.05 s) max_aux_TCC5..........................proved - complete [shostak](0.07 s) altvar_TCC1...........................proved - complete [shostak](0.05 s) altvar_TCC2...........................proved - complete [shostak](0.05 s) interval_minmax_soundness.............proved - complete [shostak](3.59 s) numerical_soundness...................proved - complete [shostak](0.03 s) Theory totals: 24 formulas, 24 attempted, 24 succeeded (4.25 s) Proof summary for theory interval_bandb evaluate_TCC1.........................proved - complete [shostak](0.09 s) combine_TCC1..........................proved - complete [shostak](0.11 s) max_rec_TCC1..........................proved - complete [shostak](0.03 s) max_rec_TCC2..........................proved - complete [shostak](0.11 s) max_rec_TCC3..........................proved - complete [shostak](0.12 s) max_rec_TCC4..........................proved - complete [shostak](0.08 s) max_rec_TCC5..........................proved - complete [shostak](0.12 s) max_rec_TCC6..........................proved - complete [shostak](0.11 s) max_rec_TCC7..........................proved - complete [shostak](0.12 s) max_rec_TCC8..........................proved - complete [shostak](0.09 s) max_rec_TCC9..........................proved - complete [shostak](0.12 s) max_rec_TCC10.........................proved - complete [shostak](0.11 s) max_rec_TCC11.........................proved - complete [shostak](0.07 s) max_aux_TCC1..........................proved - complete [shostak](0.03 s) max_aux_TCC2..........................proved - complete [shostak](0.05 s) max_aux_TCC3..........................proved - complete [shostak](0.03 s) max_aux_TCC4..........................proved - complete [shostak](0.04 s) max_aux_TCC5..........................proved - complete [shostak](0.08 s) altvar_TCC1...........................proved - complete [shostak](0.05 s) altvar_TCC2...........................proved - complete [shostak](0.05 s) interval_soundness....................proved - complete [shostak](2.44 s) Theory totals: 21 formulas, 21 attempted, 21 succeeded (4.06 s) Proof summary for theory interval_bolzano bolzano_bisect_TCC1...................proved - complete [shostak](0.16 s) bolzano_bisect_TCC2...................proved - complete [shostak](0.12 s) bolzano_bisect_TCC3...................proved - complete [shostak](0.06 s) bolzano_bisect_TCC4...................proved - complete [shostak](0.16 s) bolzano_bisect_TCC5...................proved - complete [shostak](0.12 s) bolzano_bisect_TCC6...................proved - complete [shostak](0.11 s) bolzano_bisect_TCC7...................proved - complete [shostak](0.12 s) bolzano_bisect_TCC8...................proved - complete [shostak](0.13 s) SqrtProp..............................proved - complete [shostak](0.13 s) sqrt_bisect_TCC1......................proved - complete [shostak](0.28 s) sqrt_bisect_TCC2......................proved - complete [shostak](0.05 s) sqrt_bisect_inclusion.................proved - complete [shostak](0.20 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.64 s) Proof summary for theory interval_sqrt Sqrt_TCC1.............................proved - complete [shostak](0.03 s) Sqrt_TCC2.............................proved - complete [shostak](0.02 s) Sqrt_TCC3.............................proved - complete [shostak](0.03 s) Sqrt_TCC4.............................proved - complete [shostak](0.02 s) Sqrt_inclusion_TCC1...................proved - complete [shostak](0.04 s) Sqrt_inclusion........................proved - complete [shostak](0.09 s) Sqrt_fundamental......................proved - complete [shostak](0.35 s) Proper_Sqrt...........................proved - complete [shostak](0.06 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.64 s) Proof summary for theory interval_trig cos_error_pi_lbn_bound................proved - incomplete [shostak](-.99 s) Pi_TCC1...............................proved - incomplete [shostak](0.03 s) Cos_fundamental.......................proved - incomplete [shostak](3.77 s) Sin_fundamental.......................proved - incomplete [shostak](8.64 s) tan_0_pi2_TCC1........................proved - complete [shostak](0.03 s) tan_0_pi2_TCC2........................proved - complete [shostak](0.03 s) tan_npi2_pi2_TCC1.....................proved - complete [shostak](0.03 s) tan_npi2_pi2_TCC2.....................proved - complete [shostak](0.03 s) tan_npi2_pi2_union....................proved - incomplete [shostak](3.41 s) Tan_proper............................proved - incomplete [shostak](1.20 s) Atan_fundamental......................proved - incomplete [shostak](0.05 s) Pi_inclusion..........................proved - incomplete [shostak](0.04 s) Pi_proper.............................proved - incomplete [shostak](0.03 s) sin_npi2_pi2..........................proved - incomplete [shostak](0.40 s) sin_pi2_pi............................proved - incomplete [shostak](0.35 s) sin_0_pi..............................proved - incomplete [shostak](0.19 s) sin_npi_0.............................proved - incomplete [shostak](0.09 s) sin_npi_npi2..........................proved - incomplete [shostak](0.10 s) cos_0_pi..............................proved - incomplete [shostak](0.08 s) cos_npi_0.............................proved - incomplete [shostak](0.07 s) cos_npi2_pi2..........................proved - incomplete [shostak](0.17 s) Cos_inclusion.........................proved - incomplete [shostak](0.41 s) Sin_inclusion.........................proved - incomplete [shostak](-.69 s) Tan_pi2_def...........................proved - incomplete [shostak](0.11 s) cos_lb_gt_0_pos.......................proved - incomplete [shostak](0.10 s) cos_lb_gt_0...........................proved - incomplete [shostak](0.09 s) cos_ub_gt_0...........................proved - incomplete [shostak](0.06 s) cos_lb_ub_gt_0........................proved - incomplete [shostak](0.15 s) tan_0_pi2_TCC3........................proved - incomplete [shostak](0.08 s) tan_0_pi2.............................proved - incomplete [shostak](0.24 s) tan_npi2_0_TCC1.......................proved - incomplete [shostak](0.07 s) tan_npi2_0............................proved - incomplete [shostak](0.09 s) tan_npi2_pi2_TCC3.....................proved - incomplete [shostak](0.06 s) tan_npi2_pi2..........................proved - incomplete [shostak](0.25 s) TAN?_TCC1.............................proved - complete [shostak](0.03 s) TAN_Tan...............................proved - incomplete [shostak](0.17 s) Tan_inclusion_TCC1....................proved - incomplete [shostak](0.03 s) Tan_inclusion.........................proved - incomplete [shostak](0.27 s) Tan_fundamental.......................proved - incomplete [shostak](7.26 s) Atan_inclusion........................proved - incomplete [shostak](0.08 s) Strict_Tan............................proved - incomplete [shostak](0.99 s) Proper_Sin............................proved - incomplete [shostak](0.04 s) Proper_Cos............................proved - incomplete [shostak](0.04 s) Proper_Tan............................proved - incomplete [shostak](0.05 s) Proper_Atan...........................proved - incomplete [shostak](0.05 s) Theory totals: 45 formulas, 45 attempted, 45 succeeded (27.78 s) Proof summary for theory interval_lnexp Exp_TCC1..............................proved - incomplete [shostak](0.05 s) Exp_fundamental.......................proved - incomplete [shostak](0.05 s) Ln_TCC1...............................proved - complete [shostak](0.04 s) Ln_TCC2...............................proved - complete [shostak](0.03 s) Ln_fundamental........................proved - incomplete [shostak](0.06 s) Exp_inclusion.........................proved - incomplete [shostak](0.07 s) Ln_inclusion_TCC1.....................proved - complete [shostak](0.04 s) Ln_inclusion..........................proved - incomplete [shostak](0.10 s) Proper_Ln.............................proved - incomplete [shostak](0.09 s) Proper_Exp............................proved - incomplete [shostak](0.04 s) proper_Exp_TCC1.......................proved - incomplete [shostak](0.05 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.62 s) Proof summary for theory interval_deriv deriv_domain_Xt.......................proved - complete [shostak](0.17 s) IMP_derivatives_TCC1..................proved - complete [shostak](0.03 s) IMP_derivatives_TCC2..................proved - complete [shostak](0.06 s) D_TCC1................................proved - complete [shostak](0.03 s) Diffn?_TCC1...........................proved - complete [shostak](0.04 s) Diffn?_TCC2...........................proved - complete [shostak](0.03 s) Diffn_derivn..........................proved - complete [shostak](0.21 s) Dn_TCC1...............................proved - complete [shostak](0.04 s) Dn_TCC2...............................proved - complete [shostak](0.03 s) Dn_TCC3...............................proved - complete [shostak](0.04 s) Dn_TCC4...............................proved - complete [shostak](0.04 s) Dn_nderiv_TCC1........................proved - complete [shostak](0.03 s) Dn_nderiv.............................proved - complete [shostak](0.23 s) Diff_id...............................proved - complete [shostak](0.03 s) D_id_TCC1.............................proved - complete [shostak](0.03 s) D_id..................................proved - complete [shostak](0.03 s) Diff_const............................proved - complete [shostak](0.69 s) D_const_TCC1..........................proved - complete [shostak](0.03 s) D_const...............................proved - complete [shostak](0.03 s) Diff_add..............................proved - complete [shostak](0.05 s) D_add_TCC1............................proved - complete [shostak](0.04 s) D_add.................................proved - complete [shostak](0.04 s) Diff_mult.............................proved - complete [shostak](0.05 s) D_mult_TCC1...........................proved - complete [shostak](0.03 s) D_mult................................proved - complete [shostak](0.04 s) Diff_pow_TCC1.........................proved - complete [shostak](0.04 s) Diff_pow..............................proved - complete [shostak](0.14 s) D_pow_TCC1............................proved - complete [shostak](0.03 s) D_pow_TCC2............................proved - complete [shostak](0.03 s) D_pow_TCC3............................proved - complete [shostak](0.03 s) D_pow.................................proved - complete [shostak](0.14 s) Diff_scal1............................proved - complete [shostak](0.05 s) D_scal1_TCC1..........................proved - complete [shostak](0.03 s) D_scal1...............................proved - complete [shostak](0.04 s) Diff_scal2............................proved - complete [shostak](0.06 s) D_scal2_TCC1..........................proved - complete [shostak](0.03 s) D_scal2...............................proved - complete [shostak](0.07 s) Diff_neg..............................proved - complete [shostak](0.04 s) D_neg_TCC1............................proved - complete [shostak](0.03 s) D_neg.................................proved - complete [shostak](0.04 s) Diff_sub..............................proved - complete [shostak](0.04 s) D_sub_TCC1............................proved - complete [shostak](0.03 s) D_sub.................................proved - complete [shostak](0.05 s) Diff_sq...............................proved - complete [shostak](0.06 s) D_sq_TCC1.............................proved - complete [shostak](0.03 s) D_sq..................................proved - complete [shostak](0.12 s) Diff_div_TCC1.........................proved - complete [shostak](0.04 s) Diff_div..............................proved - complete [shostak](0.05 s) D_div_TCC1............................proved - complete [shostak](0.04 s) D_div_TCC2............................proved - complete [shostak](0.09 s) D_div.................................proved - complete [shostak](0.14 s) Diff_scald1...........................proved - complete [shostak](0.06 s) D_scald1_TCC1.........................proved - complete [shostak](0.03 s) D_scald1..............................proved - complete [shostak](0.10 s) Diff_scald2...........................proved - complete [shostak](0.07 s) D_scald2_TCC1.........................proved - complete [shostak](0.03 s) D_scald2..............................proved - complete [shostak](0.09 s) Diff_sin..............................proved - incomplete [shostak](0.04 s) D_sin_TCC1............................proved - incomplete [shostak](0.03 s) D_sin.................................proved - incomplete [shostak](0.07 s) Diff_cos..............................proved - incomplete [shostak](0.04 s) D_cos_TCC1............................proved - incomplete [shostak](0.02 s) D_cos.................................proved - incomplete [shostak](0.28 s) Diff_tan_TCC1.........................proved - complete [shostak](0.03 s) Diff_tan_TCC2.........................proved - incomplete [shostak](0.79 s) Diff_tan..............................proved - incomplete [shostak](0.13 s) D_tan_TCC1............................proved - incomplete [shostak](0.10 s) D_tan_TCC2............................proved - incomplete [shostak](0.12 s) D_tan.................................proved - incomplete [shostak](0.25 s) Diff_atan.............................proved - incomplete [shostak](0.04 s) D_atan_TCC1...........................proved - incomplete [shostak](0.03 s) D_atan................................proved - incomplete [shostak](0.17 s) Diff_sqrt_TCC1........................proved - complete [shostak](0.04 s) Diff_sqrt.............................proved - complete [shostak](0.11 s) D_sqrt_TCC1...........................proved - complete [shostak](0.03 s) D_sqrt_TCC2...........................proved - complete [shostak](0.09 s) D_sqrt................................proved - complete [shostak](0.47 s) Diff_exp..............................proved - incomplete [shostak](0.04 s) D_exp_TCC1............................proved - incomplete [shostak](0.03 s) D_exp.................................proved - incomplete [shostak](0.07 s) Diff_ln_TCC1..........................proved - complete [shostak](0.05 s) Diff_ln...............................proved - incomplete [shostak](0.11 s) D_ln_TCC1.............................proved - incomplete [shostak](0.03 s) D_ln_TCC2.............................proved - complete [shostak](0.05 s) D_ln..................................proved - incomplete [shostak](0.38 s) Diff_I................................proved - complete [shostak](0.02 s) D_I_TCC1..............................proved - complete [shostak](0.04 s) D_I_TCC2..............................proved - complete [shostak](0.04 s) D_I...................................proved - complete [shostak](0.04 s) Theory totals: 89 formulas, 89 attempted, 89 succeeded (7.71 s) Proof summary for theory subinterval_deriv deriv_domain_Xt.......................proved - complete [shostak](0.17 s) subinterval_deriv_TCC1................proved - complete [shostak](1.68 s) subinterval_deriv.....................proved - complete [shostak](0.25 s) subinterval_derivn_TCC1...............proved - complete [shostak](0.08 s) subinterval_derivn....................proved - complete [shostak](0.23 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.41 s) Proof summary for theory interval_chain IMP_chain_rule_TCC1...................proved - complete [shostak](0.02 s) IMP_chain_rule_TCC2...................proved - complete [shostak](0.06 s) IMP_chain_rule_TCC3...................proved - complete [shostak](0.02 s) IMP_chain_rule_TCC4...................proved - complete [shostak](0.07 s) Diff_comp_TCC1........................proved - complete [shostak](0.03 s) Diff_comp.............................proved - complete [shostak](0.05 s) Deriv_comp_TCC1.......................proved - complete [shostak](0.03 s) Deriv_comp............................proved - complete [shostak](0.08 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.36 s) Proof summary for theory interval_taylor IMP_taylors_TCC1......................proved - complete [shostak](0.05 s) IMP_taylors_TCC2......................proved - complete [shostak](0.06 s) Taylor_TCC1...........................proved - complete [shostak](0.05 s) Taylor................................proved - complete [shostak](0.61 s) Taylor1_Midpoint......................proved - complete [shostak](0.07 s) Taylor2_Midpoint_TCC1.................proved - complete [shostak](0.03 s) Taylor2_Midpoint_TCC2.................proved - complete [shostak](0.05 s) Taylor2_Midpoint......................proved - complete [shostak](0.10 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (1.03 s) Proof summary for theory interval_io Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory interval_expr_sqrt sqrt_is_safe..........................proved - complete [shostak](0.03 s) Sqrt_Inclusion........................proved - complete [shostak](0.05 s) Sqrt_Fundamental......................proved - complete [shostak](0.03 s) SQRT_n_TCC1...........................proved - complete [shostak](0.02 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.13 s) Proof summary for theory interval_expr_trig Pi_Inclusion..........................proved - incomplete [shostak](0.03 s) Sin_Inclusion.........................proved - incomplete [shostak](0.03 s) Sin_Fundamental.......................proved - incomplete [shostak](0.04 s) SIN_n_TCC1............................proved - incomplete [shostak](0.03 s) Cos_Inclusion.........................proved - incomplete [shostak](0.03 s) Cos_Fundamental.......................proved - incomplete [shostak](0.03 s) COS_n_TCC1............................proved - incomplete [shostak](0.03 s) Tan_Inclusion.........................proved - incomplete [shostak](0.04 s) Tan_Fundamental.......................proved - incomplete [shostak](0.03 s) TAN_Precondition......................proved - incomplete [shostak](0.13 s) TAN_n_TCC1............................proved - incomplete [shostak](0.06 s) Atan_Inclusion........................proved - incomplete [shostak](0.04 s) Atan_Fundamental......................proved - incomplete [shostak](0.03 s) ATAN_n_TCC1...........................proved - incomplete [shostak](0.03 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.57 s) Proof summary for theory interval_expr_lnexp ln_safe_TCC1..........................proved - complete [shostak](0.03 s) Ln_Inclusion..........................proved - incomplete [shostak](0.08 s) Ln_Fundamental........................proved - incomplete [shostak](0.03 s) LN_n_TCC1.............................proved - incomplete [shostak](0.03 s) Exp_Inclusion.........................proved - incomplete [shostak](0.04 s) Exp_Fundamental.......................proved - incomplete [shostak](0.04 s) EXP_n_TCC1............................proved - incomplete [shostak](0.05 s) E_Inclusion...........................proved - incomplete [shostak](0.07 s) Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.37 s) Proof summary for theory strategies4Q Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory examples4Q zero_to_one_quarter...................proved - complete [shostak](-.97 s) Heart_TCC1............................proved - complete [shostak](0.03 s) Heart_TCC2............................proved - complete [shostak](0.02 s) hdp_mm_TCC1...........................proved - complete [shostak](0.03 s) hdp_mm_TCC2...........................proved - complete [shostak](0.03 s) hdp_mm_TCC3...........................proved - complete [shostak](0.03 s) hdp_mm_TCC4...........................proved - complete [shostak](0.03 s) hdp_mm_TCC5...........................proved - complete [shostak](0.02 s) hdp_mm_TCC6...........................proved - complete [shostak](0.03 s) hdp_mm................................proved - complete [shostak](4.69 s) hdp_minmax............................proved - complete [shostak](7.04 s) common_point_TCC1.....................proved - complete [shostak](0.03 s) common_point..........................proved - complete [shostak](0.51 s) simple_ite............................proved - complete [shostak](0.50 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (12.02 s) Proof summary for theory strategies Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory examples sqrt23................................proved - incomplete [shostak](1.35 s) sin6sqrt2.............................proved - incomplete [shostak](1.59 s) sqrtx3_TCC1...........................proved - complete [shostak](0.04 s) sqrtx3................................proved - incomplete [shostak](1.24 s) tr_TCC1...............................proved - incomplete [shostak](0.09 s) tr_250_35_TCC1........................proved - incomplete [shostak](1.16 s) tr_250_35.............................proved - incomplete [shostak](2.19 s) tr_200_250_abs_35.....................proved - incomplete [shostak](2.45 s) G_TCC1................................proved - complete [shostak](0.03 s) A_and_S_TCC1..........................proved - complete [shostak](0.05 s) A_and_S_TCC2..........................proved - complete [shostak](0.06 s) A_and_S...............................proved - incomplete [shostak](1.03 s) common_point_TCC1.....................proved - complete [shostak](0.04 s) common_point_TCC2.....................proved - complete [shostak](0.03 s) common_point_TCC3.....................proved - incomplete [shostak](-1.51 s) common_point_TCC4.....................proved - incomplete [shostak](0.21 s) common_point..........................proved - incomplete [shostak](4.70 s) r_TCC1................................proved - complete [shostak](0.03 s) r_TCC2................................proved - complete [shostak](0.03 s) atan_implementation...................proved - incomplete [shostak](0.26 s) ex1_ba_TCC1...........................proved - complete [shostak](0.04 s) ex1_ba_TCC2...........................proved - complete [shostak](0.06 s) ex1_ba................................proved - incomplete [shostak](1.20 s) ex2_ba_TCC1...........................proved - complete [shostak](0.05 s) ex2_ba................................proved - incomplete [shostak](1.10 s) ex3_ba_TCC1...........................proved - complete [shostak](0.05 s) ex3_ba................................proved - incomplete [shostak](1.23 s) ex4_ba................................proved - incomplete [shostak](1.26 s) ex5_ba_TCC1...........................proved - complete [shostak](0.08 s) ex5_ba................................proved - incomplete [shostak](1.35 s) ex6_ba................................proved - incomplete [shostak](1.23 s) ex7_ba................................proved - incomplete [shostak](1.17 s) Tunnel_3_IL...........................proved - incomplete [shostak](1.80 s) Tunnel_3_IL_LU........................proved - incomplete [shostak](1.97 s) Theory totals: 34 formulas, 34 attempted, 34 succeeded (27.65 s) Proof summary for theory top_allen Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory allen_interval Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory allen_interval_properties before_before.........................proved - complete [shostak](0.04 s) before_during.........................proved - complete [shostak](0.04 s) before_contains.......................proved - complete [shostak](0.03 s) before_overlaps.......................proved - complete [shostak](0.03 s) before_overlapped_by..................proved - complete [shostak](0.04 s) before_meets..........................proved - complete [shostak](0.03 s) before_met_by.........................proved - complete [shostak](0.04 s) before_starts.........................proved - complete [shostak](0.03 s) before_started_by.....................proved - complete [shostak](0.03 s) before_finishes.......................proved - complete [shostak](0.04 s) before_finished_by....................proved - complete [shostak](0.03 s) after_after...........................proved - complete [shostak](0.03 s) after_during..........................proved - complete [shostak](0.04 s) after_contains........................proved - complete [shostak](0.04 s) after_overlaps........................proved - complete [shostak](0.04 s) after_meets...........................proved - complete [shostak](0.04 s) after_met_by..........................proved - complete [shostak](0.03 s) after_starts..........................proved - complete [shostak](0.04 s) after_started_by......................proved - complete [shostak](0.03 s) after_finishes........................proved - complete [shostak](0.03 s) after_finished_by.....................proved - complete [shostak](0.04 s) during_before.........................proved - complete [shostak](0.03 s) during_after..........................proved - complete [shostak](0.03 s) during_during.........................proved - complete [shostak](0.03 s) during_overlaps.......................proved - complete [shostak](0.05 s) during_overlapped_by..................proved - complete [shostak](0.05 s) during_meets..........................proved - complete [shostak](0.03 s) during_t_meet_bay.....................proved - complete [shostak](0.03 s) during_starts.........................proved - complete [shostak](0.03 s) during_started_by.....................proved - complete [shostak](0.05 s) during_finished_by....................proved - complete [shostak](0.04 s) during_finishes.......................proved - complete [shostak](0.04 s) contains_before.......................proved - complete [shostak](0.05 s) contains_after........................proved - complete [shostak](0.04 s) contains_during.......................proved - complete [shostak](0.07 s) contains_contains.....................proved - complete [shostak](0.03 s) contains_overlaps.....................proved - complete [shostak](0.05 s) contains_overlapped_by................proved - complete [shostak](0.04 s) contains_meets........................proved - complete [shostak](0.04 s) contains_meet_by......................proved - complete [shostak](0.04 s) contains_starts.......................proved - complete [shostak](0.04 s) contains_started_by...................proved - complete [shostak](0.04 s) contains_finishes.....................proved - complete [shostak](0.04 s) contains_finished_by..................proved - complete [shostak](0.04 s) overlaps_before.......................proved - complete [shostak](0.03 s) overlaps_after........................proved - complete [shostak](0.05 s) overlaps_during.......................proved - complete [shostak](0.05 s) overlaps_overlapped_by................proved - complete [shostak](0.07 s) overlaps_contains.....................proved - complete [shostak](0.05 s) overlaps_overlaps.....................proved - complete [shostak](0.04 s) overlaps_meets........................proved - complete [shostak](0.03 s) overlaps_met_by.......................proved - complete [shostak](0.04 s) overlaps_starts.......................proved - complete [shostak](0.04 s) overlaps_start_by.....................proved - complete [shostak](0.05 s) overlaps_finishes.....................proved - complete [shostak](0.04 s) overlaps_finished_by..................proved - complete [shostak](0.04 s) overlapped_by_before..................proved - complete [shostak](0.05 s) overlapped_by_after...................proved - complete [shostak](0.03 s) overlapped_by_during..................proved - complete [shostak](0.04 s) overlapped_by_contains................proved - complete [shostak](0.05 s) overlapped_by_overlaps................proved - complete [shostak](0.07 s) overlapped_by_overlapped_by...........proved - complete [shostak](0.05 s) overlapped_by_meets...................proved - complete [shostak](0.04 s) overlapped_by_meet_by.................proved - complete [shostak](0.03 s) overlapped_by_starts..................proved - complete [shostak](0.05 s) overlapped_by_started_by..............proved - complete [shostak](0.04 s) overlapped_by_finishes................proved - complete [shostak](0.04 s) overlapped_by_finished_by.............proved - complete [shostak](0.04 s) meets_before..........................proved - complete [shostak](0.03 s) meets_after...........................proved - complete [shostak](0.04 s) meets_during..........................proved - complete [shostak](0.04 s) meets_contains........................proved - complete [shostak](0.03 s) meets_overlaps........................proved - complete [shostak](0.03 s) meets_overlapped_by...................proved - complete [shostak](0.04 s) meets_meets...........................proved - complete [shostak](0.03 s) meets_meet_by.........................proved - complete [shostak](0.03 s) meets_starts..........................proved - complete [shostak](0.03 s) meets_started_by......................proved - complete [shostak](0.03 s) meets_finishes........................proved - complete [shostak](0.04 s) meets_finished_by.....................proved - complete [shostak](0.03 s) meet_by_before........................proved - complete [shostak](0.05 s) meet_by_after.........................proved - complete [shostak](0.02 s) meet_by_during........................proved - complete [shostak](0.05 s) meet_by_contains......................proved - complete [shostak](0.03 s) meet_by_overlaps......................proved - complete [shostak](0.04 s) meet_by_meet..........................proved - complete [shostak](0.03 s) meet_by_overlapped_by.................proved - complete [shostak](0.03 s) meet_by_meet_by.......................proved - complete [shostak](0.03 s) meet_by_starts........................proved - complete [shostak](0.04 s) meet_by_started_by....................proved - complete [shostak](0.04 s) meet_by_finishes......................proved - complete [shostak](0.03 s) met_by_finished.......................proved - complete [shostak](0.03 s) starts_by_before......................proved - complete [shostak](0.03 s) starts_by_after.......................proved - complete [shostak](0.03 s) starts_by_during......................proved - complete [shostak](0.04 s) starts_by_contains....................proved - complete [shostak](0.04 s) starts_by_overlaps....................proved - complete [shostak](0.04 s) starts_by_overlapped_by...............proved - complete [shostak](0.05 s) starts_by_meet........................proved - complete [shostak](0.03 s) starts_by_meet_by.....................proved - complete [shostak](0.02 s) starts_by_starts......................proved - complete [shostak](0.02 s) starts_by_started_by..................proved - complete [shostak](0.02 s) starts_by_finishes....................proved - complete [shostak](0.03 s) starts_by_finished_by.................proved - complete [shostak](0.04 s) started_by_before.....................proved - complete [shostak](0.04 s) started_by_after......................proved - complete [shostak](0.03 s) started_by_during.....................proved - complete [shostak](0.05 s) started_by_contains...................proved - complete [shostak](0.03 s) started_by_overlaps...................proved - complete [shostak](0.05 s) --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.273Quellennavigators ] |