Proof summary for theory statements abort_is_bottom.......................proved - complete [shostak](0.31 s) while_TCC1............................proved - complete [shostak](0.13 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.44 s) Proof summary for theory statements_pre add_exists...........................proved - complete [shostak]( 0.05 s) add_valalloc.........................proved - complete [shostak]( 0.03 s) add_valx.............................proved - complete [shostak]( 0.04 s) liftpred_normfinpred.................proved - complete [shostak]( 0.21 s) qFORALL_TCC1.........................proved - complete [shostak]( 0.38 s) qEXISTS_TCC1.........................proved - complete [shostak]( 0.34 s) MTran_qFORALL........................proved - complete [shostak]( 0.17 s) MTran_qEXISTS........................proved - complete [shostak]( 0.17 s) qFORALL_valdet.......................proved - complete [shostak]( 0.40 s) qEXISTS_valdet.......................proved - complete [shostak]( 0.40 s) dAssignAnother_TCC1..................proved - complete [shostak]( 0.51 s) MTran_abort..........................proved - complete [shostak]( 2.60 s) MTran_magic..........................proved - complete [shostak]( 2.59 s) MTran_skip...........................proved - complete [shostak]( 2.58 s) abort_least..........................proved - complete [shostak]( 0.50 s) magic_greatest.......................proved - complete [shostak]( 0.50 s) abort_S_abort........................proved - complete [shostak]( 0.52 s) magic_S_magic........................proved - complete [shostak]( 0.52 s) MTran_dAssign........................proved - complete [shostak]( 0.16 s) MTran_aAssign........................proved - complete [shostak]( 0.15 s) MTran_dAssignAnother.................proved - complete [shostak]( 0.17 s) doubletimes_TCC1.....................proved - complete [shostak]( 0.17 s) doubleplus_TCC1......................proved - complete [shostak]( 0.17 s) MTran_dchoice........................proved - complete [shostak]( 1.64 s) MTran_achoice........................proved - complete [shostak]( 1.63 s) assert_TCC1..........................proved - complete [shostak]( 0.17 s) assume_TCC1..........................proved - complete [shostak]( 0.20 s) MTran_assert.........................proved - complete [shostak]( 0.56 s) MTran_assume.........................proved - complete [shostak]( 0.56 s) IfThenElse_TCC1......................proved - complete [shostak]( 0.30 s) MTran_ifthenelse.....................proved - complete [shostak]( 2.44 s) MTran_assert_sp......................proved - complete [shostak]( 0.88 s) MTran_assume_sp......................proved - complete [shostak]( 0.75 s) Add_TCC1.............................proved - complete [shostak]( 0.43 s) Del_TCC1.............................proved - complete [shostak]( 0.20 s) MTran_Add............................proved - complete [shostak]( 0.16 s) MTran_Del............................proved - complete [shostak]( 0.15 s) MTran_block..........................proved - complete [shostak]( 0.13 s) delx_setindependent..................proved - complete [shostak]( 0.20 s) Del_TCC2.............................proved - complete [shostak]( 0.39 s) MTran_Dels...........................proved - complete [shostak]( 0.19 s) Delxs2...............................proved - complete [shostak]( 0.19 s) Assign_TCC1..........................proved - complete [shostak]( 0.35 s) MTran_Assign.........................proved - complete [shostak]( 0.18 s) Add0_TCC1............................proved - complete [shostak]( 0.33 s) MTran_Add0...........................proved - complete [shostak]( 0.13 s) Lookup_def_TCC1......................proved - complete [shostak]( 0.25 s) MTran_Lookup.........................proved - complete [shostak]( 0.30 s) MTran_Mutate.........................proved - complete [shostak]( 0.25 s) Alloc_def_TCC1.......................proved - complete [shostak]( 0.18 s) MTran_Alloc..........................proved - complete [shostak]( 0.30 s) MTran_Alloc_e........................proved - complete [shostak]( 0.31 s) MTran_Free...........................proved - complete [shostak]( 0.18 s) disjunctive?_TCC1....................proved - complete [shostak]( 0.22 s) compose_conjunctive..................proved - complete [shostak]( 0.34 s) compose_disjunctive..................proved - complete [shostak]( 0.13 s) assert_conjunctive...................proved - complete [shostak]( 0.64 s) assume_conjunctive...................proved - complete [shostak]( 0.68 s) assume_sp_conjunctive................proved - complete [shostak]( 0.53 s) Assign_conjunctive...................proved - complete [shostak]( 0.31 s) Add_conjunctive......................proved - complete [shostak]( 0.25 s) Del_conjunctive......................proved - complete [shostak]( 0.28 s) Alloc_conjunctive....................proved - complete [shostak]( 0.35 s) Alloc_e_finvar_conjunctive...........proved - complete [shostak]( 0.84 s) Free_conjunctive.....................proved - complete [shostak]( 0.36 s) Del_disjunctive......................proved - complete [shostak]( 0.34 s) Free_disjunctive.....................proved - complete [shostak]( 0.53 s) o_feasible...........................proved - complete [shostak]( 3.30 s) feasible_abort.......................proved - complete [shostak]( 0.25 s) feasible_abort_alt...................proved - complete [shostak]( 0.26 s) abort_feasible.......................proved - complete [shostak]( 0.55 s) assert_feasible......................proved - complete [shostak]( 0.26 s) Assign_feasible......................proved - complete [shostak]( 0.23 s) dAssign_feasible.....................proved - complete [shostak]( 0.28 s) aAssign_feasible.....................proved - complete [shostak]( 0.23 s) Del_feasible.........................proved - complete [shostak]( 0.23 s) Add_feasible.........................proved - complete [shostak]( 0.25 s) Alloc_e_feasible.....................proved - complete [shostak]( 2.17 s) assert_false_abort...................proved - complete [shostak]( 0.40 s) assume_false_magic...................proved - complete [shostak]( 0.36 s) assert_monotonic.....................proved - complete [shostak]( 3.20 s) assume_antimonotonic.................proved - complete [shostak]( 2.44 s) assume_assert_galois.................proved - complete [shostak]( 3.25 s) assume_assert_skip...................proved - complete [shostak]( 3.24 s) skip_assume_assert...................proved - complete [shostak]( 3.23 s) assume_assert_assume.................proved - complete [shostak]( 0.42 s) assert_assume_quasi_commut...........proved - complete [shostak]( 0.70 s) assert_commut........................proved - complete [shostak]( 0.60 s) assume_commut........................proved - complete [shostak]( 0.56 s) assert_conj_TCC1.....................proved - complete [shostak]( 0.42 s) assert_conj..........................proved - complete [shostak]( 0.64 s) assume_conj..........................proved - complete [shostak]( 0.63 s) assume_suffix_assert.................proved - complete [shostak]( 0.60 s) sp_assert_monotonic..................proved - complete [shostak]( 3.32 s) sp_assume_antimonotonic..............proved - complete [shostak]( 3.38 s) sp_assume_assert_galois1.............proved - complete [shostak]( 0.30 s) sp_assume_assert_galois2.............proved - complete [shostak]( 0.30 s) sp_assume_assert_galois..............proved - complete [shostak]( 0.23 s) sp_assume_assert_skip................proved - complete [shostak]( 0.27 s) sp_skip_assume_assert................proved - complete [shostak]( 0.26 s) sp_assert_assume_quasi_commut........proved - complete [shostak]( 0.27 s) sp_assert_commut.....................proved - complete [shostak]( 0.28 s) sp_assume_commut.....................proved - complete [shostak]( 0.34 s) sp_assert_conj.......................proved - complete [shostak]( 0.44 s) sp_assume_conj.......................proved - complete [shostak]( 0.46 s) assert_refines_assert_sp.............proved - complete [shostak]( 0.24 s) assume_sp_refines_assume.............proved - complete [shostak]( 0.36 s) assert_sp_pure_assert_commut.........proved - complete [shostak]( 0.44 s) assert_sp_pure_assert_compose_TCC1...proved - complete [shostak]( 0.49 s) assert_sp_pure_assert_compose........proved - complete [shostak]( 0.49 s) assert_sp_precise_promote_assert.....proved - complete [shostak]( 0.69 s) assert_precise_promote_assume_sp.....proved - complete [shostak]( 0.49 s) assert_sp_assume_promote.............proved - complete [shostak]( 0.49 s) assert_inexactpointo_is_assertsp_assume_spproved - complete [shostak]( 0.39 s) stm_Add_Del_is_skip..................proved - complete [shostak]( 0.58 s) stm_Delxp_is_delx_p..................proved - complete [shostak]( 0.31 s) stm_Addx_delx_p_is_p_TCC1............proved - complete [shostak]( 0.24 s) stm_Addx_delx_p_is_p.................proved - complete [shostak]( 0.46 s) stm_qFORALL_Del_is_skip..............proved - complete [shostak]( 0.47 s) skip_idem_left.......................proved - complete [shostak]( 0.22 s) skip_idem_right......................proved - complete [shostak]( 0.21 s) skip_commut..........................proved - complete [shostak]( 0.23 s) assert_true_skip.....................proved - complete [shostak]( 0.34 s) assert_refin_skip....................proved - complete [shostak]( 0.23 s) assume_true_skip.....................proved - complete [shostak]( 0.37 s) skip_refin_assume....................proved - complete [shostak]( 0.69 s) x_set_x_is_skip_TCC1.................proved - complete [shostak]( 0.28 s) x_set_x_is_skip......................proved - complete [shostak]( 0.31 s) double_assignment_TCC1...............proved - complete [shostak]( 0.69 s) double_assignment....................proved - complete [shostak]( 0.44 s) cancel_first_assignment..............proved - complete [shostak]( 0.34 s) dchoice_left_semidistrib.............proved - complete [shostak]( 0.46 s) dchoice_left_distrib_conjunctive.....proved - complete [shostak]( 0.37 s) dchoice_right_distrib................proved - complete [shostak]( 0.31 s) dchoice_monotonic....................proved - complete [shostak]( 3.27 s) dchoice_idem.........................proved - complete [shostak]( 0.70 s) achoice_left_semidistrib.............proved - complete [shostak]( 0.52 s) achoice_left_distrib_disjunctive.....proved - complete [shostak]( 0.38 s) achoice_right_distrib................proved - complete [shostak]( 0.32 s) achoice_monotonic....................proved - complete [shostak]( 3.20 s) achoice_idem.........................proved - complete [shostak]( 0.70 s) achoice_exclude_middle_TCC1..........proved - complete [shostak]( 0.38 s) achoice_exclude_middle...............proved - complete [shostak]( 0.97 s) ifthenelse_monotonic.................proved - complete [shostak]( 0.37 s) assert_ifthenelse_distrib............proved - complete [shostak]( 1.18 s) assert_promote_ifthenelse_guarded_TCC1proved - complete [shostak]( 0.47 s) assert_promote_ifthenelse_guarded_TCC2proved - complete [shostak]( 0.47 s) assert_promote_ifthenelse_guarded....proved - complete [shostak]( 1.14 s) Add_Assign_Add0......................proved - complete [shostak]( 0.40 s) abort_Add_commut.....................proved - complete [shostak]( 0.55 s) magic_Add_commut.....................proved - complete [shostak]( 0.33 s) skip_Add_commut......................proved - complete [shostak]( 0.28 s) dchoice_Add_left_distrib.............proved - complete [shostak]( 0.48 s) dchoice_Add_right_distrib............proved - complete [shostak]( 0.30 s) dchoice_Del_left_distrib.............proved - complete [shostak]( 0.49 s) dchoice_Del_right_distrib............proved - complete [shostak]( 0.23 s) dchoice_scope_distrib................proved - complete [shostak]( 0.28 s) chance_Add_commut_lr.................proved - complete [shostak]( 0.32 s) assert_Add_commut....................proved - complete [shostak]( 1.11 s) assume_Add_commut....................proved - complete [shostak]( 0.89 s) assert_sp_Add_refines_Add_assert_sp..proved - complete [shostak]( 1.79 s) Add_assert_sp_refines_assert_sp_Add_with_Delproved - complete [shostak]( 0.94 s) Add_assert_sp_refines_assert_sp_Add..proved - complete [shostak]( 2.19 s) assert_sp_Add_commut.................proved - complete [shostak]( 0.31 s) assume_sp_Add_refines_Add_assume_sp..proved - complete [shostak]( 1.26 s) Add_assume_sp_refines_assume_sp_Add_with_Delproved - complete [shostak]( 3.97 s) Add_assume_sp_refines_assume_sp_Add..proved - complete [shostak]( 1.24 s) assume_sp_Add_commut.................proved - complete [shostak]( 0.33 s) Assign_Add_commut....................proved - complete [shostak]( 1.66 s) Lookup_Add_commut....................proved - complete [shostak]( 8.18 s) Mutate_Add_commut....................proved - complete [shostak]( 0.63 s) Alloc_Add_commut.....................proved - complete [shostak]( 9.79 s) Free_Add_commut......................proved - complete [shostak]( 0.40 s) Alloc_e_Add_commut_lr................proved - complete [shostak]( 3.22 s) Alloc_e_Add_commut_rl................proved - complete [shostak](10.11 s) Alloc_e_Add_commut...................proved - complete [shostak]( 0.35 s) abort_Del_commut.....................proved - complete [shostak]( 0.30 s) magic_Del_commut.....................proved - complete [shostak]( 0.22 s) skip_Del_commut......................proved - complete [shostak]( 0.28 s) chance_Del_commut....................proved - complete [shostak]( 0.44 s) assert_Del_commut....................proved - complete [shostak]( 0.38 s) assume_Del_commut....................proved - complete [shostak]( 0.37 s) assert_sp_Del_commut.................proved - complete [shostak]( 0.63 s) assume_sp_Del_commut.................proved - complete [shostak]( 3.43 s) Assign_Del_commut....................proved - complete [shostak]( 0.43 s) Lookup_Del_commut....................proved - complete [shostak]( 2.25 s) Mutate_Del_commut....................proved - complete [shostak]( 0.59 s) Alloc_Del_commut_lr..................proved - complete [shostak]( 5.87 s) Alloc_Del_commut_rl..................proved - complete [shostak]( 2.43 s) Alloc_Del_commut.....................proved - complete [shostak]( 0.35 s) Alloc_e_Del_commut_lr................proved - complete [shostak]( 9.39 s) Alloc_e_Del_commut_rl................proved - complete [shostak]( 3.27 s) Alloc_e_Del_commut...................proved - complete [shostak]( 0.35 s) Free_Del_commut......................proved - complete [shostak]( 0.40 s) member_Assign_Delxs..................proved - complete [shostak]( 2.11 s) Assign_Delx_cancel...................proved - complete [shostak]( 0.42 s) sety2x_Dely_Delx.....................proved - complete [shostak]( 0.49 s) Lookup_Delx_cancel...................proved - complete [shostak]( 0.95 s) assert_promote_assign_TCC1...........proved - complete [shostak]( 0.24 s) assert_promote_assign_TCC2...........proved - complete [shostak]( 0.32 s) assert_promote_assign................proved - complete [shostak]( 1.06 s) assert_promote_assign_exp_TCC1.......proved - complete [shostak]( 0.31 s) assert_promote_assign_exp............proved - complete [shostak]( 0.53 s) assume_promote_assign_exp............proved - complete [shostak]( 0.76 s) assert_sp_promote_assign_exp.........proved - complete [shostak]( 0.84 s) assume_sp_promote_assign_exp.........proved - complete [shostak]( 1.42 s) member_assert_Delxs_specialize.......proved - complete [shostak]( 0.47 s) assert_assign_commut_free_TCC1.......proved - complete [shostak]( 0.62 s) assert_assign_commut_free............proved - complete [shostak]( 0.97 s) assert_assign_commut_TCC1............proved - complete [shostak]( 1.20 s) assert_assign_commut.................proved - complete [shostak]( 4.61 s) assign_promote_assert_free_TCC1......proved - complete [shostak]( 0.38 s) assign_promote_assert_free...........proved - complete [shostak]( 3.23 s) assert_subste_promote_assign.........proved - complete [shostak]( 0.32 s) assert_subst_promote_assign_TCC1.....proved - complete [shostak]( 0.56 s) assert_subst_promote_assign..........proved - complete [shostak]( 0.25 s) assert_sp_subste_promote_assign......proved - complete [shostak]( 0.57 s) assert_sp_subst_promote_assign.......proved - complete [shostak]( 0.30 s) assign_assign........................proved - complete [shostak]( 0.49 s) assign_del_assign....................proved - complete [shostak]( 0.68 s) add_assign_add.......................proved - complete [shostak]( 0.37 s) add_dassiganother_add................proved - complete [shostak]( 0.37 s) dassiganother_assert_neq.............proved - complete [shostak]( 0.49 s) assign_assign_commut.................proved - complete [shostak]( 0.62 s) assign_assert_commut.................proved - complete [shostak]( 0.73 s) assign_assume_commut.................proved - complete [shostak]( 0.62 s) chance_assert_commut.................proved - complete [shostak]( 0.60 s) assign_chance_commut.................proved - complete [shostak]( 0.74 s) assign_assert_sp_commut..............proved - complete [shostak]( 1.03 s) assign_assume_sp_commut..............proved - complete [shostak]( 1.42 s) chance_assume_sp_promote.............proved - complete [shostak]( 0.71 s) assert_pointosome_promote_mutation...proved - complete [shostak]( 0.89 s) assert_mutsame_value.................proved - complete [shostak]( 1.26 s) mutate_dangling_abort_TCC1...........proved - complete [shostak]( 0.79 s) mutate_dangling_abort................proved - complete [shostak]( 0.77 s) assert_lookup_setx...................proved - complete [shostak]( 4.51 s) assert_lookup_commut_free............proved - complete [shostak]( 2.16 s) assert_lookup_commut_br_TCC1.........proved - complete [shostak]( 0.57 s) assert_lookup_commut_br..............proved - complete [shostak]( 7.56 s) assert_promote_lookup................proved - complete [shostak]( 1.80 s) lookup_dangling_abort................proved - complete [shostak]( 1.79 s) assert_promote_alloc.................proved - complete [shostak]( 4.19 s) assert_promote_alloc_e...............proved - complete [shostak]( 2.12 s) lookup_assign_commut_free............proved - complete [shostak]( 1.00 s) assign_alloc_commut..................proved - complete [shostak]( 1.07 s) lookup_promote_alloc_free............proved - complete [shostak]( 5.28 s) feasieble_dassignanother_assume_sp...proved - complete [shostak]( 3.52 s) dangling_alloc_promote_lookup_free_TCC1proved - complete [shostak]( 0.88 s) dangling_alloc_promote_lookup_free...proved - complete [shostak]( 3.90 s) nondangling_alloc_promote_lookup_free_lemmaproved - complete [shostak]( 0.47 s) nondangling_alloc_promote_lookup_freeproved - complete [shostak]( 4.39 s) alloc_promote_lookup_free............proved - complete [shostak]( 0.74 s) lookup_alloc_commut..................proved - complete [shostak]( 0.32 s) assert_promote_free..................proved - complete [shostak]( 0.66 s) delx_refine_alloc_free_delx..........proved - complete [shostak]( 3.08 s) free_alloce_refine_mutate............proved - complete [shostak]( 6.58 s) free_dangling_abort..................proved - complete [shostak]( 0.56 s) Theory totals: 257 formulas, 257 attempted, 257 succeeded (273.38 s) Proof summary for theory refinment id_is_mtran...........................proved - complete [shostak](2.28 s) mtran_partial_order...................proved - complete [shostak](4.51 s) mtran_complete_lattice................proved - complete [shostak](2.88 s) mtran_complete_lattices...............proved - complete [shostak](2.21 s) o_mtran...............................proved - complete [shostak](2.25 s) refin_reflexive.......................proved - complete [shostak](2.64 s) refin_transitive......................proved - complete [shostak](3.76 s) refin_antisymmetric...................proved - complete [shostak](2.24 s) refin_assoc...........................proved - complete [shostak](2.28 s) refin_monotonic.......................proved - complete [shostak](2.32 s) refin_monotonic_l.....................proved - complete [shostak](2.28 s) refin_monotonic_r.....................proved - complete [shostak](2.28 s) refin_monotonic_c.....................proved - complete [shostak](2.30 s) refin_context.........................proved - complete [shostak](2.29 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (36.52 s) Proof summary for theory mtrans MTran_TCC1............................proved - complete [shostak](0.04 s) monotone_compose......................proved - complete [shostak](0.26 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.30 s) Proof summary for theory separation sp_conj_subst_distrib................proved - complete [shostak]( 0.91 s) pointo_subst_distrib_TCC1............proved - complete [shostak]( 0.04 s) pointo_subst_distrib_TCC2............proved - complete [shostak]( 0.04 s) pointo_subst_distrib.................proved - complete [shostak]( 0.68 s) valvar_subst.........................proved - complete [shostak]( 0.28 s) exp_setindep_subst...................proved - complete [shostak]( 0.14 s) pred_setindep_subst..................proved - complete [shostak]( 0.15 s) emp_valdet...........................proved - complete [shostak]( 0.06 s) aone_valdet..........................proved - complete [shostak]( 0.05 s) pointo_valdet........................proved - complete [shostak]( 0.22 s) sp_conj_valdet.......................proved - complete [shostak]( 0.31 s) sp_impl_valdet.......................proved - complete [shostak]( 0.40 s) inexact_pointo_valdet................proved - complete [shostak]( 0.07 s) pointo_some_valdet...................proved - complete [shostak]( 0.11 s) inexact_pointo_some_valdet...........proved - complete [shostak]( 0.26 s) eq_valdet............................proved - complete [shostak]( 0.08 s) emp_setindep.........................proved - complete [shostak]( 0.28 s) aone_setindep........................proved - complete [shostak]( 0.14 s) pointo_setindep......................proved - complete [shostak]( 0.71 s) sp_conj_setindep.....................proved - complete [shostak]( 0.63 s) sp_impl_setindep.....................proved - complete [shostak]( 0.74 s) inexact_pointo_setindep..............proved - complete [shostak]( 0.24 s) pointo_some_setindep.................proved - complete [shostak]( 0.50 s) inexact_pointo_some_setindep.........proved - complete [shostak]( 0.12 s) eq_setindep..........................proved - complete [shostak]( 0.22 s) pointo_finvardep.....................proved - complete [shostak]( 0.25 s) pointo_some_finvardep................proved - complete [shostak]( 0.10 s) inexact_pointo_finvardep.............proved - complete [shostak]( 0.28 s) inexact_pointo_some_finvardep........proved - complete [shostak]( 0.13 s) sp_conj_finvardep....................proved - complete [shostak]( 0.32 s) eq_finvardep.........................proved - complete [shostak]( 0.34 s) emp_nalloc...........................proved - complete [shostak]( 0.14 s) aone_nalloc..........................proved - complete [shostak]( 0.28 s) pointo_nalloc........................proved - complete [shostak]( 1.24 s) sp_conj_nalloc.......................proved - complete [shostak]( 0.79 s) sp_impl_nalloc.......................proved - complete [shostak]( 1.24 s) inexact_pointo_nalloc................proved - complete [shostak]( 0.17 s) pointo_some_nalloc...................proved - complete [shostak]( 0.24 s) inexact_pointo_some_nalloc...........proved - complete [shostak]( 0.18 s) eq_nalloc............................proved - complete [shostak]( 0.37 s) emp_norm_pred........................proved - complete [shostak]( 0.20 s) aone_norm_pred.......................proved - complete [shostak]( 0.16 s) pointo_norm_pred.....................proved - complete [shostak]( 0.35 s) sp_conj_norm_pred....................proved - complete [shostak]( 0.31 s) sp_impl_norm_pred....................proved - complete [shostak]( 0.42 s) inexact_pointo_norm_pred.............proved - complete [shostak]( 0.47 s) pointo_some_norm_pred................proved - complete [shostak]( 0.37 s) inexact_pointo_some_norm_pred........proved - complete [shostak]( 0.45 s) eq_norm_pred.........................proved - complete [shostak]( 0.21 s) pure_setalloc_independent............proved - complete [shostak]( 0.34 s) pure_setaddr_independent.............proved - complete [shostak]( 0.36 s) pure_allocsub_independent............proved - complete [shostak]( 1.59 s) pure_copya_independent...............proved - complete [shostak]( 1.46 s) purepred_setalloc_independent........proved - complete [shostak]( 0.45 s) purepred_setaddr_independent.........proved - complete [shostak]( 0.36 s) purepred_allocsub_independent........proved - complete [shostak]( 0.90 s) purepred_const.......................proved - complete [shostak]( 0.40 s) purepred_and.........................proved - complete [shostak]( 0.76 s) purepred_or..........................proved - complete [shostak]( 0.81 s) purepred_not.........................proved - complete [shostak]( 0.68 s) purepred_impl........................proved - complete [shostak]( 0.83 s) purepred_iff.........................proved - complete [shostak]( 0.89 s) purepred_eq..........................proved - complete [shostak]( 0.97 s) purepred_qforall.....................proved - complete [shostak]( 0.92 s) purepred_qexists.....................proved - complete [shostak]( 0.96 s) alt_precise..........................proved - complete [shostak]( 0.55 s) spax_monotonic.......................proved - complete [shostak]( 1.72 s) spax_antimonotonic...................proved - complete [shostak]( 0.69 s) spax_triv_strengthening..............proved - complete [shostak]( 0.43 s) spax_triv_weakening..................proved - complete [shostak]( 0.41 s) spax_assoc...........................proved - complete [shostak]( 1.56 s) vspax_assoc..........................proved - complete [shostak]( 0.54 s) spax_commut..........................proved - complete [shostak]( 0.54 s) vspax_commut.........................proved - complete [shostak]( 0.53 s) spax_emp_unit........................proved - complete [shostak]( 0.83 s) vspax_emp_unit.......................proved - complete [shostak]( 0.58 s) spax_disj_distrib....................proved - complete [shostak]( 0.51 s) vspax_disj_distrib...................proved - complete [shostak]( 0.54 s) spax_conj_semidistrib................proved - complete [shostak]( 1.16 s) spax_forall_semidistrib..............proved - complete [shostak]( 0.71 s) spax_curry...........................proved - complete [shostak]( 0.46 s) spax_uncurry.........................proved - complete [shostak]( 0.46 s) spax_unbeta_modus....................proved - complete [shostak]( 0.51 s) spax_unbeta..........................proved - complete [shostak]( 0.41 s) spax_beta............................proved - complete [shostak]( 0.44 s) spax_beta_modus......................proved - complete [shostak]( 0.47 s) spax_spimpl_curry....................proved - complete [shostak]( 0.61 s) spax_spimpl_commut...................proved - complete [shostak]( 0.50 s) spax_spand_promotion.................proved - complete [shostak]( 0.47 s) spax_pure_and_impl_spand.............proved - complete [shostak]( 0.69 s) spax_pure_spand_impl_and.............proved - complete [shostak]( 0.45 s) spax_pure_spand_is_and...............proved - complete [shostak]( 0.41 s) spax_pure_spand_distribute...........proved - complete [shostak]( 0.60 s) spax_pure_spimpl_impl_impl...........proved - complete [shostak]( 0.44 s) spax_pure_spimpl_is_impl.............proved - complete [shostak]( 0.53 s) pure_implies_intuitionistic..........proved - complete [shostak]( 0.40 s) intuitionistic_and...................proved - complete [shostak]( 0.54 s) intuitionistic_or....................proved - complete [shostak]( 1.24 s) intuitionistic_forall................proved - complete [shostak]( 0.66 s) intuitionistic_exists................proved - complete [shostak]( 0.66 s) intuitionistic_spand.................proved - complete [shostak]( 0.70 s) intuitionistic_spimpl_neg............proved - complete [shostak]( 0.79 s) intuitionistic_spimpl_pos............proved - complete [shostak]( 1.11 s) intutitionistic_star_true............proved - complete [shostak]( 0.77 s) intutitionistic_true_spimpl..........proved - complete [shostak]( 0.76 s) intuitionistic_inexact_pointo........proved - complete [shostak]( 1.14 s) intuitionistic_inexact_pointo_some...proved - complete [shostak]( 1.17 s) intutitionistic_weakening............proved - complete [shostak]( 0.81 s) intutitionistic_strengthening........proved - complete [shostak]( 0.78 s) intutitionistic_spand_impl_and.......proved - complete [shostak]( 0.87 s) intutitionistic_triv_weakening.......proved - complete [shostak]( 0.95 s) intutitionistic_triv_strengthening...proved - complete [shostak]( 0.91 s) strictly_exact_emp...................proved - complete [shostak]( 1.11 s) strictly_exact_pointo................proved - complete [shostak]( 1.94 s) strictly_exact_spand.................proved - complete [shostak]( 2.54 s) strictly_exact_starand_starimpl......proved - complete [shostak]( 1.56 s) inexact_pointo_as_pointo.............proved - complete [shostak]( 0.87 s) strictly_exact_implies_domain_exact..proved - complete [shostak]( 0.88 s) domain_exact_pointo_some.............proved - complete [shostak]( 0.99 s) strictly_exact_implies_precise.......proved - complete [shostak]( 1.08 s) precise_pointo_some..................proved - complete [shostak]( 1.05 s) precise_spand........................proved - complete [shostak]( 1.84 s) precise_distrib......................proved - complete [shostak]( 1.56 s) precise_forall_distrib...............proved - complete [shostak]( 1.86 s) pointo_pointo_some...................proved - complete [shostak]( 1.13 s) inexact_pointo_inexact_pointo_some...proved - complete [shostak]( 1.39 s) sp_conj_not_inexact_pointo_somes.....proved - complete [shostak]( 3.05 s) pointo_neq_not_inexact_pointo_some...proved - complete [shostak]( 1.39 s) pointo_sp_conj_neq_not_inexact_pointo_some_inexactproved - complete [shostak]( 1.65 s) allocated_spimpl_commut..............proved - complete [shostak](11.06 s) Theory totals: 130 formulas, 130 attempted, 130 succeeded (99.03 s) Proof summary for theory preds norm_pred_TCC1........................proved - complete [shostak](0.11 s) nallocpred_subtypof_normpred..........proved - complete [shostak](0.02 s) normpred_allocsub.....................proved - complete [shostak](0.60 s) lift_implies_partial_order............proved - complete [shostak](3.06 s) lift_implies_complete_lattice.........proved - complete [shostak](0.64 s) predimpl_is_complete_lattice..........proved - complete [shostak](0.25 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (4.68 s) Proof summary for theory pred_simp booexp_partial_order..................proved - complete [shostak](4.69 s) booexp_complete_lattice...............proved - complete [shostak](3.27 s) valdet_exp_extend.....................proved - complete [shostak](2.78 s) valdet_pred_extend....................proved - complete [shostak](2.76 s) pureexp_seta_independent..............proved - complete [shostak](2.82 s) pureexp_seth_independent..............proved - complete [shostak](2.95 s) pureexp_subst_pure....................proved - complete [shostak](3.11 s) liftval_valdet........................proved - complete [shostak](2.76 s) liftvar_valdet........................proved - complete [shostak](2.75 s) liftpred_valdet.......................proved - complete [shostak](2.80 s) eqvalof_valdet........................proved - complete [shostak](2.79 s) and_valdet............................proved - complete [shostak](2.98 s) or_valdet.............................proved - complete [shostak](2.97 s) not_valdet............................proved - complete [shostak](2.85 s) impl_valdet...........................proved - complete [shostak](2.96 s) iff_valdet............................proved - complete [shostak](3.10 s) qFORALL_valdet........................proved - complete [shostak](2.86 s) qEXISTS_valdet........................proved - complete [shostak](3.70 s) subst_valdet..........................proved - complete [shostak](3.18 s) normexp_subst_valdet..................proved - complete [shostak](3.10 s) subst_setindep........................proved - complete [shostak](2.89 s) valdet_setindep_preddeleq.............proved - complete [shostak](2.88 s) valdet_setindep_preddeleq_loc.........proved - complete [shostak](2.89 s) liftval_setindep......................proved - complete [shostak](2.82 s) liftvar_setindep......................proved - complete [shostak](2.84 s) liftpred_setindep.....................proved - complete [shostak](2.81 s) and_setindep..........................proved - complete [shostak](2.92 s) or_setindep...........................proved - complete [shostak](2.90 s) not_setindep..........................proved - complete [shostak](2.84 s) impl_setindep.........................proved - complete [shostak](2.91 s) iff_setindep..........................proved - complete [shostak](2.95 s) qFORALL_setindep......................proved - complete [shostak](3.12 s) qEXISTS_setindep......................proved - complete [shostak](3.16 s) finvardep_valof.......................proved - complete [shostak](3.63 s) finvardep_const.......................proved - complete [shostak](2.90 s) finvardep_eqvalof.....................proved - complete [shostak](3.01 s) finvardep_lift........................proved - complete [shostak](2.88 s) subst_finvardep_exp...................proved - complete [shostak](3.27 s) subst_valdet_exp......................proved - complete [shostak](3.05 s) and_finvardep.........................proved - complete [shostak](3.19 s) or_finvardep..........................proved - complete [shostak](3.13 s) not_finvardep.........................proved - complete [shostak](3.08 s) impl_finvardep........................proved - complete [shostak](2.93 s) iff_finvardep.........................proved - complete [shostak](2.97 s) qFORALL_finvardep.....................proved - complete [shostak](3.29 s) qEXISTS_finvardep.....................proved - complete [shostak](3.28 s) subst_finvardep.......................proved - complete [shostak](3.39 s) liftpred_nalloc.......................proved - complete [shostak](2.89 s) and_nalloc............................proved - complete [shostak](3.50 s) or_nalloc.............................proved - complete [shostak](3.48 s) not_nalloc............................proved - complete [shostak](3.14 s) impl_nalloc...........................proved - complete [shostak](3.51 s) iff_nalloc............................proved - complete [shostak](3.91 s) qFORALL_nalloc........................proved - complete [shostak](3.11 s) qEXISTS_nalloc........................proved - complete [shostak](3.12 s) subst_nalloc..........................proved - complete [shostak](3.16 s) setac_nalloc..........................proved - complete [shostak](3.83 s) copya_nalloc..........................proved - complete [shostak](4.00 s) validimpl_derives_order...............proved - complete [shostak](2.96 s) order_derives_validimpl...............proved - complete [shostak](2.94 s) order_equal_validimpl.................proved - complete [shostak](2.92 s) validimpl_reflexive...................proved - complete [shostak](2.93 s) predand_monotonic.....................proved - complete [shostak](3.00 s) predor_monotonic......................proved - complete [shostak](3.00 s) predimpl_monotonic....................proved - complete [shostak](3.02 s) predimpl_curry........................proved - complete [shostak](2.98 s) predimpl_uncurry......................proved - complete [shostak](2.97 s) predimpl_beta.........................proved - complete [shostak](2.95 s) predimpl_unbeta.......................proved - complete [shostak](2.96 s) eq_derives_validimpl..................proved - complete [shostak](2.93 s) validimpl_derives_eq..................proved - complete [shostak](2.94 s) validimpl_chain.......................proved - complete [shostak](2.98 s) predimpl_true.........................proved - complete [shostak](2.93 s) predimpl_false........................proved - complete [shostak](2.94 s) predimpl_negor........................proved - complete [shostak](2.98 s) predimpl_contrapositive...............proved - complete [shostak](2.96 s) predand_assoc.........................proved - complete [shostak](2.98 s) predand_commut........................proved - complete [shostak](2.96 s) predand_idem..........................proved - complete [shostak](2.96 s) predand_true..........................proved - complete [shostak](2.96 s) predand_elim..........................proved - complete [shostak](2.94 s) predand_false.........................proved - complete [shostak](2.95 s) predand_impl..........................proved - complete [shostak](3.06 s) predand_impl_both.....................proved - complete [shostak](2.98 s) predor_assoc..........................proved - complete [shostak](2.96 s) predor_commut.........................proved - complete [shostak](2.96 s) predor_idem...........................proved - complete [shostak](2.96 s) predor_intro..........................proved - complete [shostak](2.95 s) predor_false..........................proved - complete [shostak](2.96 s) predor_true...........................proved - complete [shostak](2.95 s) predor_impl...........................proved - complete [shostak](3.02 s) Theory totals: 91 formulas, 91 attempted, 91 succeeded (278.60 s) Proof summary for theory expressions noemp_ExpVar..........................proved - complete [shostak](0.04 s) subst_TCC1............................proved - complete [shostak](0.10 s) valx_substx...........................proved - complete [shostak](0.14 s) valy_substx...........................proved - complete [shostak](0.16 s) delx_subst............................proved - complete [shostak](0.21 s) delx_e_subst_exc......................proved - complete [shostak](0.20 s) setx_independence.....................proved - complete [shostak](0.04 s) nonallocindep_allocsub................proved - complete [shostak](0.74 s) nonallocindep_copya...................proved - complete [shostak](0.69 s) nonallocindep_copya_sub...............proved - complete [shostak](1.00 s) val_expvar_closed.....................proved - complete [shostak](0.38 s) lift_val_pure_closed..................proved - complete [shostak](0.12 s) pure_closed_subst.....................proved - complete [shostak](0.82 s) Theory totals: 13 formulas, 13 attempted, 13 succeeded (4.64 s) Proof summary for theory states_plus st_seta_setb_is_setb_eta..............proved - complete [shostak](0.14 s) st_exch_setx_sety_eta.................proved - complete [shostak](0.09 s) st_delx_valy_is_valy_eta..............proved - complete [shostak](0.14 s) st_setx_delx_eta......................proved - complete [shostak](0.07 s) st_setx_dely_is_dely_setx_eta.........proved - complete [shostak](0.08 s) st_del_change_var_TCC1................proved - complete [shostak](0.12 s) st_del_change_var.....................proved - complete [shostak](0.13 s) val_alloc_TCC1........................proved - complete [shostak](0.11 s) set_alloc_TCC1........................proved - complete [shostak](0.03 s) fix_valofalloc........................proved - complete [shostak](0.06 s) fix_setalloc_TCC1.....................proved - complete [shostak](0.03 s) fix_setalloc..........................proved - complete [shostak](0.04 s) fix_valalloc_eq.......................proved - complete [shostak](0.03 s) fix_valalloc_eqv......................proved - complete [shostak](0.12 s) fix_valalloc_def......................proved - complete [shostak](0.02 s) fix_setindep_alloc....................proved - complete [shostak](0.16 s) valh_seth.............................proved - complete [shostak](0.11 s) seth_valh_stable......................proved - complete [shostak](0.07 s) seth1_seth2_is_seth2..................proved - complete [shostak](0.03 s) seth1_seth2_is_seth2_eta..............proved - complete [shostak](0.07 s) valalloc_set..........................proved - complete [shostak](0.07 s) valalloc_set_eta......................proved - complete [shostak](0.07 s) valh_setx_is_valh.....................proved - complete [shostak](0.08 s) valx_seth_is_valx.....................proved - complete [shostak](0.07 s) setx_seth_is_seth_setx................proved - complete [shostak](0.09 s) setx_diffa_is_diffa_setx..............proved - complete [shostak](0.10 s) valh_delx_is_valh.....................proved - complete [shostak](0.14 s) delx_seth_is_seth_delx................proved - complete [shostak](0.14 s) nomem_addr_varlist....................proved - complete [shostak](0.14 s) dels_append...........................proved - complete [shostak](0.61 s) dels_seth_is_seth_dels................proved - complete [shostak](0.11 s) dels_seta_is_seta_dels................proved - complete [shostak](0.14 s) delx_dels_setx_is_delx_dels...........proved - complete [shostak](0.19 s) valy_dels_setx_is_valy_dels...........proved - complete [shostak](0.25 s) member_dels_set_cancel................proved - complete [shostak](0.20 s) member_dels_setx_cancel...............proved - complete [shostak](0.19 s) member_valx_dels......................proved - complete [shostak](0.04 s) nonmember_valx_dels_skip..............proved - complete [shostak](0.15 s) nonmember_valx_dels...................proved - complete [shostak](0.09 s) valaddr_dels_skip.....................proved - complete [shostak](0.14 s) val_dels_set_is_val_dels..............proved - complete [shostak](0.23 s) reverse_dels_snoc.....................proved - complete [shostak](0.08 s) unfold_dels_snoc......................proved - complete [shostak](0.10 s) filter_not_nonmem.....................proved - complete [shostak](0.15 s) nonmem_filter_not_nonmem..............proved - complete [shostak](0.10 s) neq_filter_not_mem....................proved - complete [shostak](0.20 s) pure_setalloc.........................proved - complete [shostak](0.10 s) pure_setaddr..........................proved - complete [shostak](0.11 s) add_valeqv_left.......................proved - complete [shostak](0.29 s) add_valeqv_right......................proved - complete [shostak](0.10 s) add_valeqv_both.......................proved - complete [shostak](0.14 s) valeqv_valheq.........................proved - complete [shostak](0.03 s) seth_valeqv...........................proved - complete [shostak](0.05 s) diffah_valeqv.........................proved - complete [shostak](0.06 s) valdet_setindep_deleq.................proved - complete [shostak](0.24 s) valdet_setindep_deleq_loc.............proved - complete [shostak](0.25 s) del_valdet_setindep_eq................proved - complete [shostak](0.25 s) vala_diffah_is_diffh..................proved - complete [shostak](0.05 s) diffalloc_diff_is_setalloc............proved - complete [shostak](0.05 s) diffa_vala_diffah_is_setah............proved - complete [shostak](0.08 s) alloc_sub_TCC1........................proved - complete [shostak](0.27 s) allocsub_reflexive....................proved - complete [shostak](0.04 s) allocsub_subset.......................proved - complete [shostak](0.16 s) allocsub_valheq_eq....................proved - complete [shostak](0.04 s) allocsub_emp..........................proved - complete [shostak](0.52 s) allocsub_valeq........................proved - complete [shostak](0.07 s) allocsub_valx.........................proved - complete [shostak](0.85 s) allocsub_valeqvvar....................proved - complete [shostak](0.12 s) allocsub_setvar.......................proved - complete [shostak](1.05 s) allocsub_addreqv......................proved - complete [shostak](0.86 s) allocsub_setaddr_any..................proved - complete [shostak](1.33 s) allocsub_setaddr_any_cancel...........proved - complete [shostak](0.12 s) allocsub_setaddr_any_both.............proved - complete [shostak](1.04 s) allocsub_setaddr_any_left.............proved - complete [shostak](0.88 s) allocsub_setaddr_any_para.............proved - complete [shostak](0.28 s) allocsub_setaddr......................proved - complete [shostak](0.86 s) allocsub_addalloc.....................proved - complete [shostak](1.43 s) allocsub_remalloc.....................proved - complete [shostak](0.34 s) allocsub_remalloc_any.................proved - complete [shostak](0.27 s) allocsub_remalloc_eq..................proved - complete [shostak](1.31 s) allocsub_remalloc_both................proved - complete [shostak](1.32 s) allocsub_remalloc_left................proved - complete [shostak](0.86 s) allocsub_restrict_alloc2..............proved - complete [shostak](0.95 s) allocsub_restrict_alloc...............proved - complete [shostak](0.04 s) allocsub_restrict_alloc_both..........proved - complete [shostak](0.84 s) allocsub_addalloc_both................proved - complete [shostak](1.55 s) allocsub_extend_alloc2................proved - complete [shostak](1.33 s) allocsub_extend_alloc.................proved - complete [shostak](0.04 s) allocsub_diffalloc....................proved - complete [shostak](2.23 s) mem_allocsub_setaddr..................proved - complete [shostak](1.30 s) delx_allocsub_commut..................proved - complete [shostak](1.13 s) allocsub_preserves_pure...............proved - complete [shostak](0.81 s) allocsub_valeqv.......................proved - complete [shostak](1.19 s) allocsub_purexpr_independent..........proved - complete [shostak](0.67 s) allocsub_transitive...................proved - complete [shostak](0.73 s) allocsub_partial_order................proved - complete [shostak](0.12 s) allocsub_valvar_dels..................proved - complete [shostak](0.16 s) copy_alloc_TCC1.......................proved - complete [shostak](0.06 s) copy_alloc_TCC2.......................proved - complete [shostak](0.22 s) valalloc_copya........................proved - complete [shostak](0.47 s) valx_copya............................proved - complete [shostak](0.60 s) setx_copya_is_copya_setx..............proved - complete [shostak](0.56 s) seth_copya_is_copya_seth..............proved - complete [shostak](0.55 s) copya_seta_is_seta_copya..............proved - complete [shostak](1.10 s) nomem_copya_seta......................proved - complete [shostak](0.79 s) nomem_seta_copya......................proved - complete [shostak](0.90 s) copyalloc_any.........................proved - complete [shostak](1.51 s) mem_seta_copya........................proved - complete [shostak](1.02 s) mem_copya_seta........................proved - complete [shostak](0.12 s) copya_idem............................proved - complete [shostak](0.55 s) copya_setremh.........................proved - complete [shostak](1.75 s) subset_copya_idem.....................proved - complete [shostak](0.99 s) copya_copya_idem......................proved - complete [shostak](0.85 s) copya_copy............................proved - complete [shostak](0.76 s) nomem_valof_copyaq....................proved - complete [shostak](0.58 s) valof_copyaq..........................proved - complete [shostak](0.45 s) restrict_allocadreqv..................proved - complete [shostak](0.48 s) seth_copya_allocadreqv................proved - complete [shostak](0.36 s) allocadreqv_make_allocsub.............proved - complete [shostak](1.08 s) allocsub_subset_copya_eq_right........proved - complete [shostak](0.53 s) allocsub_copya_eq_right...............proved - complete [shostak](0.54 s) allocsub_copya_eq_right2..............proved - complete [shostak](1.88 s) allocsub_copya_eq.....................proved - complete [shostak](1.06 s) allocsub_copya_allocsub...............proved - complete [shostak](0.03 s) allocsub_copya_revert_lesser..........proved - complete [shostak](1.11 s) allocsub_copya_subset_allocsub........proved - complete [shostak](0.57 s) allocsub_copya_subset_allocsub_inv....proved - complete [shostak](0.48 s) allocsub_copya_donut_diffdiff.........proved - complete [shostak](1.99 s) allocsub_copya_donut_diffdiff2........proved - complete [shostak](1.57 s) allocsub_copya_setdiffh...............proved - complete [shostak](1.25 s) allocsub_copya_setdiffh2..............proved - complete [shostak](1.12 s) allocsub_valeqv_eq....................proved - complete [shostak](1.63 s) allocsub_mv_alloc.....................proved - complete [shostak](0.97 s) allocsub_commut_setempty_copya........proved - complete [shostak](1.06 s) allocsub_copya_setdiffh_left..........proved - complete [shostak](1.68 s) sub_allocsub_copya_donut_diffdiff.....proved - complete [shostak](2.39 s) allocsub3_transit.....................proved - complete [shostak](1.12 s) copyalloc_delx_any....................proved - complete [shostak](0.61 s) copyalloc_delx........................proved - complete [shostak](0.70 s) delx_copya_is_copya_delx..............proved - complete [shostak](0.60 s) addx_allocsub_copya_allocsub2.........proved - complete [shostak](1.57 s) asub_addx_asub_copya..................proved - complete [shostak](2.57 s) asub_addx_delx........................proved - complete [shostak](2.61 s) asub_addx_delx_left...................proved - complete [shostak](1.56 s) asub_addx_asub_self...................proved - complete [shostak](1.70 s) asub_extend_copyalloc.................proved - complete [shostak](0.76 s) asub_diff_singleton_eq................proved - complete [shostak](0.72 s) subset_addrmatch_asub_copya...........proved - complete [shostak](1.71 s) seta_const_TCC1.......................proved - complete [shostak](0.05 s) seta_const_TCC2.......................proved - complete [shostak](0.17 s) seta_const_TCC3.......................proved - complete [shostak](0.30 s) valh_setac............................proved - complete [shostak](0.51 s) seth_setac............................proved - complete [shostak](0.54 s) valvar_setac..........................proved - complete [shostak](0.57 s) setvar_setac_TCC1.....................proved - complete [shostak](0.09 s) setvar_setac..........................proved - complete [shostak](0.74 s) delvar_setac..........................proved - complete [shostak](0.59 s) nonmem_vala_setac.....................proved - complete [shostak](0.62 s) mem_vala_setac........................proved - complete [shostak](0.67 s) nonmem_seta_setac_TCC1................proved - complete [shostak](0.13 s) nonmem_seta_setac.....................proved - complete [shostak](0.77 s) setac_any_TCC1........................proved - complete [shostak](0.13 s) setac_any.............................proved - complete [shostak](1.21 s) mem_seta_setac_TCC1...................proved - complete [shostak](0.14 s) mem_seta_setac........................proved - complete [shostak](1.05 s) copya_setac_stable....................proved - complete [shostak](0.75 s) Theory totals: 166 formulas, 166 attempted, 166 succeeded (95.30 s) Proof summary for theory list_plus null_is_null?.........................proved - complete [shostak](0.03 s) cons?_eta.............................proved - complete [shostak](0.06 s) length_cdr............................proved - complete [shostak](0.07 s) map_id_is_id..........................proved - complete [shostak](0.11 s) null_map_null.........................proved - complete [shostak](0.04 s) null_null_map.........................proved - complete [shostak](0.04 s) car_map_f_is_f_car_TCC1...............proved - complete [shostak](0.04 s) car_map_f_is_f_car_TCC2...............proved - complete [shostak](0.05 s) car_map_f_is_f_car....................proved - complete [shostak](0.05 s) cdr_map_map_cdr.......................proved - complete [shostak](0.24 s) reverse_null..........................proved - complete [shostak](0.03 s) append_null_l.........................proved - complete [shostak](0.03 s) append_null_null......................proved - complete [shostak](0.08 s) append_cons...........................proved - complete [shostak](0.09 s) member_append.........................proved - complete [shostak](0.12 s) member_reverse........................proved - complete [shostak](0.46 s) map_append............................proved - complete [shostak](0.16 s) map_reverse...........................proved - complete [shostak](0.24 s) cons_as_reversed_append...............proved - complete [shostak](0.37 s) car_snoc_r_TCC1.......................proved - complete [shostak](0.05 s) car_snoc_r............................proved - complete [shostak](0.07 s) cdr_snoc_r............................proved - complete [shostak](0.09 s) member_snoc_r.........................proved - complete [shostak](0.13 s) append_snoc_r_cons....................proved - complete [shostak](0.15 s) reverse_cons_as_snoc_r................proved - complete [shostak](0.20 s) map_snoc_r............................proved - complete [shostak](0.27 s) filter_subset.........................proved - complete [shostak](0.17 s) member_list2set.......................proved - complete [shostak](0.12 s) distinct?_TCC1........................proved - complete [shostak](0.22 s) add_distinct..........................proved - complete [shostak](0.09 s) distinct_snoc_r.......................proved - complete [shostak](0.32 s) append_cons_distinct..................proved - complete [shostak](0.39 s) snoc_r_distinct.......................proved - complete [shostak](0.35 s) reverse_distinct......................proved - complete [shostak](0.13 s) Theory totals: 34 formulas, 34 attempted, 34 succeeded (5.06 s) Proof summary for theory absexp del_valeqv............................proved - complete [shostak](0.30 s) del_valeqv_loc........................proved - complete [shostak](0.22 s) allocaddr_equivalent_TCC1.............proved - complete [shostak](0.03 s) allocaddr_equivalent_TCC2.............proved - complete [shostak](0.33 s) setx_allocadreqv......................proved - complete [shostak](1.00 s) nonalloc_independent_TCC1.............proved - complete [shostak](0.02 s) inf_nonalloc_finite...................proved - complete [shostak](0.39 s) nonalloc_closed_binary................proved - complete [shostak](0.21 s) nonalloc_closed_unary.................proved - complete [shostak](0.18 s) pure_closed_binary....................proved - complete [shostak](0.36 s) pure_closed_unary.....................proved - complete [shostak](0.04 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (3.08 s) Proof summary for theory valeqvdet Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s) Proof summary for theory valeqv val_equivalent_TCC1...................proved - complete [shostak](0.23 s) setx_valeqv...........................proved - complete [shostak](0.36 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.59 s) Proof summary for theory states val_of_TCC1...........................proved - complete [shostak](0.15 s) dels_TCC1.............................proved - complete [shostak](0.28 s) st_del_change_TCC1....................proved - complete [shostak](0.11 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.54 s) Proof summary for theory valtyp typ_TCC1..............................proved - complete [shostak](0.04 s) allocAddr_typ.........................proved - complete [shostak](0.15 s) fullsetValue_typ......................proved - complete [shostak](0.02 s) typ_of_TCC1...........................proved - complete [shostak](0.03 s) typof_adr_typ.........................proved - complete [shostak](0.03 s) typof_var_typ.........................proved - complete [shostak](0.03 s) typof_allocated_any...................proved - complete [shostak](0.04 s) typof_uloc_any........................proved - complete [shostak](0.05 s) typof_adr_any.........................proved - complete [shostak](0.05 s) typof_var_any.........................proved - complete [shostak](0.04 s) Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.48 s) Proof summary for theory values LocAddr_TCC1..........................proved - complete [shostak](0.05 s) const_notmem_locaddr..................proved - complete [shostak](0.07 s) disj_const_loc........................proved - complete [shostak](0.04 s) loc_subsumedby_locaddr................proved - complete [shostak](0.04 s) const_notmem_loc......................proved - complete [shostak](0.08 s) userLocation_TCC1.....................proved - complete [shostak](0.06 s) allocated_isnot_userloc...............proved - complete [shostak](0.02 s) var_neq_addr..........................proved - complete [shostak](0.06 s) addr_neq_var..........................proved - complete [shostak](0.05 s) variable_userloc......................proved - complete [shostak](0.02 s) var_never_const.......................proved - complete [shostak](0.05 s) address_userloc.......................proved - complete [shostak](0.03 s) adr_never_const.......................proved - complete [shostak](0.05 s) address_of_value......................proved - complete [shostak](0.04 s) from_addrset_TCC1.....................proved - complete [shostak](0.04 s) id_finadr.............................proved - complete [shostak](0.07 s) id_allocadr...........................proved - complete [shostak](0.06 s) finadr_elem_is_addr...................proved - complete [shostak](0.04 s) value_infinite........................proved - complete [shostak](0.26 s) pick_new_value........................proved - complete [shostak](0.16 s) pick_new_value1.......................proved - complete [shostak](0.05 s) pick_nonallocated_address.............proved - complete [shostak](0.21 s) pick_new_variable.....................proved - complete [shostak](0.19 s) pick_newvar1..........................proved - complete [shostak](0.06 s) pick_newvar2..........................proved - complete [shostak](0.09 s) pick_newvar1_fincompl.................proved - complete [shostak](0.09 s) Theory totals: 26 formulas, 26 attempted, 26 succeeded (1.98 s) Proof summary for theory sets_plus difference_order......................proved - complete [shostak](0.13 s) disjoint_commutative..................proved - complete [shostak](0.05 s) subset_diff_disjoint..................proved - complete [shostak](0.12 s) subset_diff_disjoint2.................proved - complete [shostak](0.13 s) diff_decreasing.......................proved - complete [shostak](0.08 s) subset_intersection_difference........proved - complete [shostak](0.12 s) intersection_preserves_subset.........proved - complete [shostak](0.08 s) nonmember_remove......................proved - complete [shostak](0.04 s) remove_empty..........................proved - complete [shostak](0.07 s) unique_then_singleton.................proved - complete [shostak](0.11 s) member_singleton......................proved - complete [shostak](0.08 s) empty_remove_sigleton.................proved - complete [shostak](0.09 s) subset_remove_remove..................proved - complete [shostak](0.08 s) propersubset_memdiff_subset_remove....proved - complete [shostak](0.07 s) relcompl_twice........................proved - complete [shostak](0.11 s) add_add...............................proved - complete [shostak](0.10 s) remove_remove.........................proved - complete [shostak](0.08 s) add_add_commut........................proved - complete [shostak](0.09 s) add_remove_commut.....................proved - complete [shostak](0.14 s) remove_remove_commut..................proved - complete [shostak](0.09 s) remove_preserves_subset...............proved - complete [shostak](0.08 s) choose_difference_TCC1................proved - complete [shostak](0.07 s) choose_difference.....................proved - complete [shostak](0.09 s) difference_mono.......................proved - complete [shostak](0.09 s) difference_subset_inv.................proved - complete [shostak](0.05 s) subset_emptyset_emptyset..............proved - complete [shostak](0.06 s) porpersubset_difference...............proved - complete [shostak](0.05 s) member_member_diff....................proved - complete [shostak](0.07 s) singleton_difference_inv..............proved - complete [shostak](0.12 s) difference_remove.....................proved - complete [shostak](0.10 s) difference_remove_remove..............proved - complete [shostak](0.13 s) difference_remove_remove2.............proved - complete [shostak](0.14 s) member_difference_remove..............proved - complete [shostak](0.07 s) mem_diff_remove_member................proved - complete [shostak](0.06 s) remeq_nonmem..........................proved - complete [shostak](0.06 s) remove_difference_remove..............proved - complete [shostak](0.14 s) member_difference_remove_cancel.......proved - complete [shostak](0.12 s) subset_diffeq_eq......................proved - complete [shostak](0.19 s) subset_diffeq_eq2.....................proved - complete [shostak](0.18 s) subset_add_add........................proved - complete [shostak](0.04 s) subset_add_eq.........................proved - complete [shostak](0.10 s) difference_add........................proved - complete [shostak](0.11 s) difference_remove_singleton...........proved - complete [shostak](0.10 s) diff_diff_singleton...................proved - complete [shostak](0.34 s) member_diff_singleton_add.............proved - complete [shostak](0.13 s) member_diff_singleton_remove..........proved - complete [shostak](0.07 s) member_diff_add_member_diff...........proved - complete [shostak](0.08 s) member_diff_add_member................proved - complete [shostak](0.08 s) difference_add_commut.................proved - complete [shostak](0.12 s) subset2_memdiff2_memdiff..............proved - complete [shostak](0.08 s) subset_diff_diff_eq...................proved - complete [shostak](0.07 s) subset_subsetdiff_diffdiff_eq.........proved - complete [shostak](0.21 s) union_add_commut......................proved - complete [shostak](0.13 s) subset_union_monotonic................proved - complete [shostak](0.08 s) finite_union_finite_each..............proved - complete [shostak](0.10 s) mem2_dichodichotomy...................proved - complete [shostak](0.06 s) card_remove_lt........................proved - complete [shostak](0.14 s) finitediff_finset.....................proved - complete [shostak](0.04 s) Theory totals: 58 formulas, 58 attempted, 58 succeeded (5.81 s) Proof summary for theory relation_plus inverse_relcomp_is_id.................proved - complete [shostak](0.18 s) graph_distrib.........................proved - complete [shostak](0.09 s) graph_equivalence.....................proved - complete [shostak](0.08 s) graphf_is_functional..................proved - complete [shostak](0.03 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.38 s) Proof summary for theory fixed_points_plus mono_compose..........................proved - complete [shostak](0.24 s) setorder_luborder_TCC1................proved - complete [shostak](0.06 s) setorder_luborder_TCC2................proved - complete [shostak](0.03 s) setorder_luborder.....................proved - complete [shostak](0.16 s) lfp_TCC1..............................proved - complete [shostak](0.52 s) lfp_expand............................proved - complete [shostak](0.28 s) bottom_TCC1...........................proved - complete [shostak](0.04 s) bottom_is_least.......................proved - complete [shostak](0.11 s) iterate_TCC1..........................proved - complete [shostak](0.13 s) iterate_TCC2..........................proved - complete [shostak](0.10 s) iterate_TCC3..........................proved - complete [shostak](0.21 s) iterate_TCC4..........................proved - complete [shostak](0.07 s) iterate_TCC5..........................proved - complete [shostak](0.46 s) iter_zero.............................proved - complete [shostak](0.04 s) iter_succ.............................proved - complete [shostak](0.19 s) iter_ord_succ.........................proved - complete [shostak](0.74 s) iter_succ_inner.......................proved - complete [shostak](0.66 s) iternat_iterord.......................proved - complete [shostak](0.68 s) iternat_succ..........................proved - complete [shostak](0.37 s) continuous?_TCC1......................proved - complete [shostak](0.04 s) continuous?_TCC2......................proved - complete [shostak](0.05 s) admissible?_TCC1......................proved - complete [shostak](0.03 s) iter_succ_increasing..................proved - complete [shostak](1.03 s) iter_succ_increasing_nat..............proved - complete [shostak](0.38 s) iter_monotonic........................proved - complete [shostak](0.73 s) iter_monotonic_nat....................proved - complete [shostak](0.20 s) Theory totals: 26 formulas, 26 attempted, 26 succeeded (7.55 s) Proof summary for theory ordinals_plus zero?_zero............................proved - complete [shostak](0.06 s) zero?_iff_zero........................proved - complete [shostak](0.03 s) zero_minord...........................proved - complete [shostak](0.16 s) ordstruct_exclusive...................proved - complete [shostak](0.05 s) zero_as_ordinal.......................proved - complete [shostak](0.03 s) one_TCC1..............................proved - complete [shostak](0.04 s) size_exp_lt_TCC1......................proved - complete [shostak](0.04 s) size_exp_lt...........................proved - complete [shostak](0.36 s) size_rest_lt..........................proved - complete [shostak](0.35 s) succ_pre_TCC1.........................proved - complete [shostak](0.43 s) succ_zero_is_one......................proved - complete [shostak](0.02 s) one_is_nonzero........................proved - complete [shostak](0.02 s) succ_monotonic........................proved - complete [shostak](0.09 s) zero_nosucc...........................proved - complete [shostak](0.17 s) zero_least_ordinal....................proved - complete [shostak](0.05 s) lt_one_is_zero........................proved - complete [shostak](0.24 s) exp_ordinal_TCC1......................proved - complete [shostak](0.04 s) exp_ordinal...........................proved - complete [shostak](0.03 s) rest_ordinal..........................proved - complete [shostak](0.03 s) succ_TCC1.............................proved - complete [shostak](0.72 s) lt_succ_dichotomous...................proved - complete [shostak](1.32 s) expsucc_nonzero_ord_TCC1..............proved - complete [shostak](0.03 s) expsucc_nonzero_ord...................proved - complete [shostak](0.18 s) coefsucc_nonzero_ord_zero?............proved - complete [shostak](0.29 s) coefsucc_nonzero_ord_nonzero?.........proved - complete [shostak](0.36 s) zero_is_limit_ordinal.................proved - complete [shostak](0.46 s) succ_is_succ_ordinal..................proved - complete [shostak](0.04 s) succ_ord_TCC1.........................proved - complete [shostak](0.03 s) lim_ord_TCC1..........................proved - complete [shostak](0.03 s) succ_injective........................proved - complete [shostak](1.52 s) succ_bijective........................proved - complete [shostak](0.05 s) pred_succ_id..........................proved - complete [shostak](0.18 s) succ_pred_id..........................proved - complete [shostak](0.04 s) pred_lt...............................proved - complete [shostak](0.21 s) nat_ord_TCC1..........................proved - complete [shostak](0.05 s) nat_ord_TCC2..........................proved - complete [shostak](0.03 s) nat_ord_zero..........................proved - complete [shostak](0.02 s) nat_ord_one...........................proved - complete [shostak](0.03 s) nat_ord_succ..........................proved - complete [shostak](0.51 s) nat_ord_order.........................proved - complete [shostak](0.24 s) nat_succ_ord..........................proved - complete [shostak](0.14 s) succ_chain_TCC1.......................proved - complete [shostak](0.05 s) succ_chain_TCC2.......................proved - complete [shostak](0.04 s) succ_chain_reflexive..................proved - complete [shostak](0.03 s) succ_chain_succ.......................proved - complete [shostak](0.04 s) succ_chain_order......................proved - complete [shostak](0.46 s) nat_ord_succ_chain....................proved - complete [shostak](0.68 s) succ_chain_wf.........................proved - complete [shostak](0.40 s) Theory totals: 48 formulas, 48 attempted, 48 succeeded (10.42 s) Proof summary for theory example conjunctive_inf?_TCC1.................proved - complete [shostak](0.17 s) disjunctive_inf?_TCC1.................proved - complete [shostak](0.10 s) univ_disjunctive_abort................proved - complete [shostak](0.72 s) Free_disjunctive_inf..................proved - complete [shostak](0.86 s) while_lemma_1a_TCC1...................proved - complete [shostak](0.28 s) while_lemma_1a........................proved - complete [shostak](2.42 s) while_lemma_code_motion_TCC1..........proved - complete [shostak](0.80 s) while_lemma_code_motion...............proved - complete [shostak](5.09 s) WS_TCC1...............................proved - complete [shostak](0.16 s) WS_TCC2...............................proved - complete [shostak](0.10 s) WT_TCC1...............................proved - complete [shostak](0.11 s) list_append_refine_recycle............proved - complete [shostak](5.56 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (16.37 s) Grand Totals: 915 proofs, 915 attempted, 915 succeeded (845.15 s)