[kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Warning: your preprocessor is not known to handle option `-dD'. If pre-processing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant.
[kernel] Parsing list_ptr.c (with preprocessing)
[kernel] Warning: trying to preprocess annotation with an unknown preprocessor.
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] Computing [100 goals...]
[wp] Computing [200 goals...]
[wp] Computing [300 goals...]
[wp] Computing [400 goals...]
[wp] Computing [500 goals...]
[wp] Computing [600 goals...]
[wp] Computing [700 goals...]
[wp] Computing [800 goals...]
[wp] Computing [900 goals...]
[wp] Computing [1000 goals...]
[wp] Computing [1100 goals...]
[wp] Computing [1200 goals...]
[wp] Computing [1300 goals...]
[wp] Computing [1400 goals...]
[wp] Computing [1500 goals...]
[wp] 1552 goals scheduled
[wp] [Qed] Goal typed_list_init_post_GhostSeparation : Valid
[wp] [Qed] Goal typed_list_init_post_ValidArray : Valid
[wp] [Qed] Goal typed_list_init_assign : Valid
[wp] [Qed] Goal typed_list_init_post_3 : Valid
[wp] [Qed] Goal typed_list_tail_complete_not_empty_empty : Valid
[wp] [Qed] Goal typed_list_head_empty_post : Valid
[wp] [Qed] Goal typed_list_head_assign : Valid
[wp] [Qed] Goal typed_list_tail_disjoint_not_empty_empty : Valid
[wp] [Qed] Goal typed_list_tail_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_list_tail_assert : Valid
[wp] [Qed] Goal typed_list_tail_loop_inv_4_established : Valid
[wp] [Qed] Goal typed_list_tail_assign_part2 : Valid
[wp] [Qed] Goal typed_list_tail_assign_part1 : Valid
[wp] [Qed] Goal typed_list_tail_loop_assign : Valid
[wp] [Qed] Goal typed_list_tail_loop_term_decrease : Valid
[wp] [Qed] Goal typed_list_tail_assign_part5 : Valid
[wp] [Qed] Goal typed_list_tail_assign_part4 : Valid
[wp] [Qed] Goal typed_list_tail_assign_part3 : Valid
[wp] [Qed] Goal typed_list_tail_not_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_tail_empty_post_part2 : Valid
[wp] [Qed] Goal typed_list_tail_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_tail_loop_term_positive : Valid
[wp] [Qed] Goal typed_list_tail_not_empty_post_3_part1 : Valid
[wp] [Qed] Goal typed_list_tail_not_empty_post_2_part1 : Valid
[wp] [Qed] Goal typed_list_pop_post_part1 : Valid
[wp] [Qed] Goal typed_list_pop_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_pop_post_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_pop_post_part2 : Valid
[wp] [Qed] Goal typed_list_pop_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_pop_assert : Valid
[wp] [Qed] Goal typed_list_pop_assert_4 : Valid
[wp] [Qed] Goal typed_list_pop_assert_3 : Valid
[wp] [Qed] Goal typed_list_pop_assert_2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_4_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Separation_part1 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Unique_part1 : Valid
[wp] [Qed] Goal typed_list_pop_empty_assign_part1 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_Separation_2_part1 : Valid
[wp] [Qed] Goal typed_list_pop_more_post_part1 : Valid
[wp] [Qed] Goal typed_list_pop_more_assign_part1 : Valid
[wp] [Qed] Goal typed_list_push_stmt_post_part2 : Valid
[wp] [Qed] Goal typed_list_pop_more_assign_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert : Valid
[wp] [Qed] Goal typed_list_push_stmt_post_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_4 : Valid
[wp] [Qed] Goal typed_list_push_assert_3 : Valid
[wp] [Qed] Goal typed_list_push_assert_2 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_push_disjoint_does_not_contain_item_contains_item : Valid
[wp] [Qed] Goal typed_list_push_complete_does_not_contain_item_contains_item : Valid
[wp] [Qed] Goal typed_list_push_stmt_assign : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_2_part1 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_5 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_2_part4 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_post_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_9 : Valid
[wp] [Qed] Goal typed_list_push_assert_8 : Valid
[wp] [Qed] Goal typed_list_push_assert_7 : Valid
[wp] [Qed] Goal typed_list_push_assert_6 : Valid
[wp] [Qed] Goal typed_list_push_assert_13 : Valid
[wp] [Qed] Goal typed_list_push_assert_12 : Valid
[wp] [Qed] Goal typed_list_push_assert_11 : Valid
[wp] [Qed] Goal typed_list_push_assert_10 : Valid
[wp] [Qed] Goal typed_list_push_assert_17 : Valid
[wp] [Qed] Goal typed_list_push_assert_16 : Valid
[wp] [Qed] Goal typed_list_push_assert_15 : Valid
[wp] [Qed] Goal typed_list_push_assert_14 : Valid
[wp] [Qed] Goal typed_list_push_assert_21 : Valid
[wp] [Qed] Goal typed_list_push_assert_20 : Valid
[wp] [Qed] Goal typed_list_push_assert_19 : Valid
[wp] [Qed] Goal typed_list_push_assert_18 : Valid
[wp] [Qed] Goal typed_list_push_assert_25 : Valid
[wp] [Qed] Goal typed_list_push_assert_24 : Valid
[wp] [Qed] Goal typed_list_push_assert_23 : Valid
[wp] [Qed] Goal typed_list_push_assert_22 : Valid
[wp] [Qed] Goal typed_list_push_assert_29 : Valid
[wp] [Qed] Goal typed_list_push_assert_28 : Valid
[wp] [Qed] Goal typed_list_push_assert_27 : Valid
[wp] [Qed] Goal typed_list_push_assert_26 : Valid
[wp] [Qed] Goal typed_list_push_assert_33 : Valid
[wp] [Qed] Goal typed_list_push_assert_32 : Valid
[wp] [Qed] Goal typed_list_push_assert_31 : Valid
[wp] [Qed] Goal typed_list_push_assert_30 : Valid
[wp] [Qed] Goal typed_list_push_assert_37 : Valid
[wp] [Qed] Goal typed_list_push_assert_36 : Valid
[wp] [Qed] Goal typed_list_push_assert_35 : Valid
[wp] [Qed] Goal typed_list_push_assert_34 : Valid
[wp] [Qed] Goal typed_list_push_assert_41 : Valid
[wp] [Qed] Goal typed_list_push_assert_40 : Valid
[wp] [Qed] Goal typed_list_push_assert_39 : Valid
[wp] [Qed] Goal typed_list_push_assert_38 : Valid
[wp] [Qed] Goal typed_list_push_assert_45 : Valid
[wp] [Qed] Goal typed_list_push_assert_44 : Valid
[wp] [Qed] Goal typed_list_push_assert_43 : Valid
[wp] [Qed] Goal typed_list_push_assert_42 : Valid
[wp] [Qed] Goal typed_list_push_assert_49 : Valid
[wp] [Qed] Goal typed_list_push_assert_48 : Valid
[wp] [Qed] Goal typed_list_push_assert_47 : Valid
[wp] [Qed] Goal typed_list_push_assert_46 : Valid
[wp] [Qed] Goal typed_list_push_assert_53 : Valid
[wp] [Qed] Goal typed_list_push_assert_52 : Valid
[wp] [Qed] Goal typed_list_push_assert_51 : Valid
[wp] [Qed] Goal typed_list_push_assert_50 : Valid
[wp] [Qed] Goal typed_list_push_assert_57 : Valid
[wp] [Qed] Goal typed_list_push_assert_56 : Valid
[wp] [Qed] Goal typed_list_push_assert_55 : Valid
[wp] [Qed] Goal typed_list_push_assert_54 : Valid
[wp] [Qed] Goal typed_list_push_assert_61 : Valid
[wp] [Qed] Goal typed_list_push_assert_60 : Valid
[wp] [Qed] Goal typed_list_push_assert_59 : Valid
[wp] [Qed] Goal typed_list_push_assert_58 : Valid
[wp] [Qed] Goal typed_list_push_assert_65 : Valid
[wp] [Qed] Goal typed_list_push_assert_64 : Valid
[wp] [Qed] Goal typed_list_push_assert_63 : Valid
[wp] [Qed] Goal typed_list_push_assert_62 : Valid
[wp] [Qed] Goal typed_list_push_assert_69 : Valid
[wp] [Qed] Goal typed_list_push_assert_68 : Valid
[wp] [Qed] Goal typed_list_push_assert_67 : Valid
[wp] [Qed] Goal typed_list_push_assert_66 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part02 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part01 : Valid
[wp] [Qed] Goal typed_list_push_assert_71 : Valid
[wp] [Qed] Goal typed_list_push_assert_70 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part06 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part05 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part04 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part03 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part10 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part09 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part08 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part07 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part14 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part13 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part12 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part11 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part03 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part02 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part01 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part06 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part05 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part04 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part10 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part09 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part08 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part07 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part14 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part13 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part12 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part11 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part18 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part17 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part16 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part21 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part20 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part19 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part25 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part24 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part23 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part22 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_bounds_weak_pre_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_bounds_weak_pre_part1 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part27 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part26 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_bounds_weak_pre_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_bounds_weak_pre_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_up_unexisting_item_pre_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_up_unexisting_item_pre_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_up_unexisting_item_pre_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_up_unexisting_item_pre_2_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_up_unexisting_item_pre_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_up_unexisting_item_pre_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_3_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_2_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part8 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part6 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part5 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Linked_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Linked_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Linked_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_ValidArray_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_ValidArray_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_ValidArray_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Linked_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part03 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part02 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part01 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_ValidArray_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part07 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part06 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part05 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part04 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part11 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part10 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part09 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part08 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_2_part12 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_3_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_3_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Item_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Item_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_3_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_3_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_4_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_4_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_length_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_list_length_loop_assign : Valid
[wp] [Qed] Goal typed_list_length_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_list_length_assign_part2 : Valid
[wp] [Qed] Goal typed_list_length_assign_part1 : Valid
[wp] [Qed] Goal typed_list_length_loop_term_positive : Valid
[wp] [Qed] Goal typed_list_length_loop_term_decrease : Valid
[wp] [Qed] Goal typed_list_length_assign_part3 : Valid
[wp] [Qed] Goal typed_list_chop_post_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_chop_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_chop_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_chop_post_GhostSeparation_3_part1 : Valid
[wp] [Qed] Goal typed_list_chop_assert : Valid
[wp] [Qed] Goal typed_list_chop_assert_3 : Valid
[wp] [Qed] Goal typed_list_chop_assert_2 : Valid
[wp] [Qed] Goal typed_list_chop_assert_4 : Valid
[wp] [Qed] Goal typed_list_chop_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_list_chop_assert_5 : Valid
[wp] [Qed] Goal typed_list_chop_assert_8 : Valid
[wp] [Qed] Goal typed_list_chop_assert_7 : Valid
[wp] [Qed] Goal typed_list_chop_assert_6 : Valid
[wp] [Qed] Goal typed_list_chop_assert_12 : Valid
[wp] [Qed] Goal typed_list_chop_assert_11 : Valid
[wp] [Qed] Goal typed_list_chop_assert_10 : Valid
[wp] [Qed] Goal typed_list_chop_assert_9 : Valid
[wp] [Qed] Goal typed_list_chop_assert_16 : Valid
[wp] [Qed] Goal typed_list_chop_assert_15 : Valid
[wp] [Qed] Goal typed_list_chop_assert_14 : Valid
[wp] [Qed] Goal typed_list_chop_assert_13 : Valid
[wp] [Qed] Goal typed_list_chop_assert_20 : Valid
[wp] [Qed] Goal typed_list_chop_assert_19 : Valid
[wp] [Qed] Goal typed_list_chop_assert_18 : Valid
[wp] [Qed] Goal typed_list_chop_assert_17 : Valid
[wp] [Qed] Goal typed_list_chop_loop_assign : Valid
[wp] [Qed] Goal typed_list_chop_assert_23 : Valid
[wp] [Qed] Goal typed_list_chop_assert_22 : Valid
[wp] [Qed] Goal typed_list_chop_assert_21 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part4 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part3 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part2 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part1 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part03 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part02 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part01 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part5 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part07 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part06 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part05 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part04 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part11 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part09 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part08 : Valid
[wp] [Qed] Goal typed_list_chop_loop_term_decrease : Valid
[wp] [Qed] Goal typed_list_chop_call_linked_n_before_last_pre_ValidArray : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_2_part1 : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_part3 : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_part3 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_2_part1 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_chop_more_post_4_part1 : Valid
[wp] [Qed] Goal typed_list_add_disjoint_does_not_contain_item_contains_item : Valid
[wp] [Qed] Goal typed_list_add_complete_does_not_contain_item_contains_item : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part7 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part5 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_part8 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_assert_2 : Valid
[wp] [Qed] Goal typed_list_add_assert : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part8 : Valid
[wp] [Qed] Goal typed_list_add_assert_5 : Valid
[wp] [Qed] Goal typed_list_add_assert_4 : Valid
[wp] [Qed] Goal typed_list_add_assert_3 : Valid
[wp] [Qed] Goal typed_list_add_assert_9 : Valid
[wp] [Qed] Goal typed_list_add_assert_8 : Valid
[wp] [Qed] Goal typed_list_add_assert_7 : Valid
[wp] [Qed] Goal typed_list_add_assert_6 : Valid
[wp] [Qed] Goal typed_list_add_assert_13 : Valid
[wp] [Qed] Goal typed_list_add_assert_12 : Valid
[wp] [Qed] Goal typed_list_add_assert_11 : Valid
[wp] [Qed] Goal typed_list_add_assert_10 : Valid
[wp] [Qed] Goal typed_list_add_assert_17 : Valid
[wp] [Qed] Goal typed_list_add_assert_16 : Valid
[wp] [Qed] Goal typed_list_add_assert_15 : Valid
[wp] [Qed] Goal typed_list_add_assert_14 : Valid
[wp] [Qed] Goal typed_list_add_assert_21 : Valid
[wp] [Qed] Goal typed_list_add_assert_20 : Valid
[wp] [Qed] Goal typed_list_add_assert_19 : Valid
[wp] [Qed] Goal typed_list_add_assert_18 : Valid
[wp] [Qed] Goal typed_list_add_assert_25 : Valid
[wp] [Qed] Goal typed_list_add_assert_24 : Valid
[wp] [Qed] Goal typed_list_add_assert_23 : Valid
[wp] [Qed] Goal typed_list_add_assert_22 : Valid
[wp] [Qed] Goal typed_list_add_assert_29 : Valid
[wp] [Qed] Goal typed_list_add_assert_28 : Valid
[wp] [Qed] Goal typed_list_add_assert_27 : Valid
[wp] [Qed] Goal typed_list_add_assert_26 : Valid
[wp] [Qed] Goal typed_list_add_assert_33 : Valid
[wp] [Qed] Goal typed_list_add_assert_32 : Valid
[wp] [Qed] Goal typed_list_add_assert_31 : Valid
[wp] [Qed] Goal typed_list_add_assert_30 : Valid
[wp] [Qed] Goal typed_list_add_assert_37 : Valid
[wp] [Qed] Goal typed_list_add_assert_36 : Valid
[wp] [Qed] Goal typed_list_add_assert_35 : Valid
[wp] [Qed] Goal typed_list_add_assert_34 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part03 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part02 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part01 : Valid
[wp] [Qed] Goal typed_list_add_assert_38 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part07 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part06 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part05 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part04 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part11 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part10 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part09 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part08 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part15 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part14 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part13 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part12 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part19 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part18 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part17 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part16 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part23 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part22 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part21 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part20 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part27 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part26 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part25 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part29 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part28 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part02 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part01 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part31 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part06 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part05 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part04 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part03 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part10 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part09 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part08 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part07 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part14 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part13 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part12 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part11 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part18 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part17 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part16 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part15 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part22 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part21 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part20 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part19 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part26 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part25 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part23 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part29 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part28 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part31 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part30 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part35 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part34 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part33 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part39 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part37 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part36 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_bounds_weak_pre_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_bounds_weak_pre_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_bounds_weak_pre_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_up_unexisting_item_pre_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_bounds_weak_pre_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_up_unexisting_item_pre_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_up_unexisting_item_pre_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_up_unexisting_item_pre_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_up_unexisting_item_pre_2_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_up_unexisting_item_pre_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_2_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_3_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part5 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Linked_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part8 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part6 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Linked_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Linked_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Linked_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_ValidArray_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_ValidArray_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_ValidArray_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_ValidArray_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part04 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part03 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part02 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part01 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part08 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part07 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part06 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part05 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part12 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part11 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part10 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_2_part09 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_3_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Item_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Item_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_3_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_ValidArray_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_ValidArray_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_ValidArray_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_ValidArray_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part01 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part04 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part03 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part07 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part06 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part05 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part10 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part09 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part08 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part02 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part12 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part05 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part04 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part08 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part07 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part06 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part11 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part09 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_ValidArray_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_ValidArray_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_ValidArray_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_ValidArray_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part5 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_1_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part6 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_1_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_1_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_1_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_item_value_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_item_value_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_item_value_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_item_value_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_4_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_4_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_4_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_4_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Item_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Item_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part8 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part8 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part2 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part4 : Valid
[wp] [Qed] Goal typed_list_remove_disjoint_does_not_contain_item_contains_item : Valid
[wp] [Qed] Goal typed_list_remove_complete_does_not_contain_item_contains_item : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part1 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_part5 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part4 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part1 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part4 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part3 : Valid
[wp] [Qed] Goal typed_list_remove_assert : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part6 : Valid
[wp] [Qed] Goal typed_list_remove_assert_5 : Valid
[wp] [Qed] Goal typed_list_remove_assert_4 : Valid
[wp] [Qed] Goal typed_list_remove_assert_3 : Valid
[wp] [Qed] Goal typed_list_remove_assert_2 : Valid
[wp] [Qed] Goal typed_list_remove_assert_9 : Valid
[wp] [Qed] Goal typed_list_remove_assert_8 : Valid
[wp] [Qed] Goal typed_list_remove_assert_7 : Valid
[wp] [Qed] Goal typed_list_remove_assert_6 : Valid
[wp] [Qed] Goal typed_list_remove_assert_13 : Valid
[wp] [Qed] Goal typed_list_remove_assert_12 : Valid
[wp] [Qed] Goal typed_list_remove_assert_11 : Valid
[wp] [Qed] Goal typed_list_remove_assert_10 : Valid
[wp] [Qed] Goal typed_list_remove_assert_17 : Valid
[wp] [Qed] Goal typed_list_remove_assert_16 : Valid
[wp] [Qed] Goal typed_list_remove_assert_15 : Valid
[wp] [Qed] Goal typed_list_remove_assert_14 : Valid
[wp] [Qed] Goal typed_list_remove_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_18 : Valid
[wp] [Qed] Goal typed_list_remove_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_list_remove_loop_inv_7_established : Valid
[wp] [Qed] Goal typed_list_remove_assert_20 : Valid
[wp] [Qed] Goal typed_list_remove_assert_19 : Valid
[wp] [Qed] Goal typed_list_remove_assert_24 : Valid
[wp] [Qed] Goal typed_list_remove_assert_23 : Valid
[wp] [Qed] Goal typed_list_remove_assert_22 : Valid
[wp] [Qed] Goal typed_list_remove_assert_21 : Valid
[wp] [Qed] Goal typed_list_remove_assert_28 : Valid
[wp] [Qed] Goal typed_list_remove_assert_27 : Valid
[wp] [Qed] Goal typed_list_remove_assert_26 : Valid
[wp] [Qed] Goal typed_list_remove_assert_25 : Valid
[wp] [Qed] Goal typed_list_remove_assert_32 : Valid
[wp] [Qed] Goal typed_list_remove_assert_31 : Valid
[wp] [Qed] Goal typed_list_remove_assert_30 : Valid
[wp] [Qed] Goal typed_list_remove_assert_29 : Valid
[wp] [Qed] Goal typed_list_remove_assert_36 : Valid
[wp] [Qed] Goal typed_list_remove_assert_35 : Valid
[wp] [Qed] Goal typed_list_remove_assert_34 : Valid
[wp] [Qed] Goal typed_list_remove_assert_33 : Valid
[wp] [Qed] Goal typed_list_remove_assert_40 : Valid
[wp] [Qed] Goal typed_list_remove_assert_39 : Valid
[wp] [Qed] Goal typed_list_remove_assert_38 : Valid
[wp] [Qed] Goal typed_list_remove_assert_37 : Valid
[wp] [Qed] Goal typed_list_remove_assert_44 : Valid
[wp] [Qed] Goal typed_list_remove_assert_43 : Valid
[wp] [Qed] Goal typed_list_remove_assert_42 : Valid
[wp] [Qed] Goal typed_list_remove_assert_41 : Valid
[wp] [Qed] Goal typed_list_remove_assert_48 : Valid
[wp] [Qed] Goal typed_list_remove_assert_47 : Valid
[wp] [Qed] Goal typed_list_remove_assert_46 : Valid
[wp] [Qed] Goal typed_list_remove_assert_45 : Valid
[wp] [Qed] Goal typed_list_remove_assert_52 : Valid
[wp] [Qed] Goal typed_list_remove_assert_51 : Valid
[wp] [Qed] Goal typed_list_remove_assert_50 : Valid
[wp] [Qed] Goal typed_list_remove_assert_49 : Valid
[wp] [Qed] Goal typed_list_remove_assert_56 : Valid
[wp] [Qed] Goal typed_list_remove_assert_55 : Valid
[wp] [Qed] Goal typed_list_remove_assert_54 : Valid
[wp] [Qed] Goal typed_list_remove_assert_53 : Valid
[wp] [Qed] Goal typed_list_remove_assert_60 : Valid
[wp] [Qed] Goal typed_list_remove_assert_59 : Valid
[wp] [Qed] Goal typed_list_remove_assert_58 : Valid
[wp] [Qed] Goal typed_list_remove_assert_57 : Valid
[wp] [Qed] Goal typed_list_remove_loop_assign : Valid
[wp] [Qed] Goal typed_list_remove_assert_63 : Valid
[wp] [Qed] Goal typed_list_remove_assert_62 : Valid
[wp] [Qed] Goal typed_list_remove_assert_61 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part4 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part3 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part2 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part1 : Valid
[wp] [Qed] Goal typed_list_remove_loop_term_positive : Valid
[wp] [Qed] Goal typed_list_remove_loop_term_decrease : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Linked_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Linked_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_ItemNotIn_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_ItemNotIn_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_IttemSep_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_IttemSep_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unchanged_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unchanged_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Swiped_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Swiped_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part1 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part4 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_UnchangedSwipe_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part1 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_UnchangedSwipe_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part4 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_3_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_4_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_4_part6 : Valid
[wp] [Qed] Goal typed_list_copy_assert_2 : Valid
[wp] [Qed] Goal typed_list_copy_assert : Valid
[wp] [Qed] Goal typed_list_item_next_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_item_next_assign_part2 : Valid
[wp] [Qed] Goal typed_list_item_next_assign_part1 : Valid
[wp] [Qed] Goal typed_list_copy_assign : Valid
[wp] [Qed] Goal typed_list_item_next_not_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_item_next_empty_post_part2 : Valid
[wp] [Qed] Goal typed_linked_n_starting_from_null_empty_assign : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_assign_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_assign_part1 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_term_positive : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_bounds_assign : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_assign_part2 : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_assign_part1 : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_term_positive : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_assign_part2 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_assign_part1 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_before_last_assert : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_term_positive : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_inv_preserved_part1 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_assert_3 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_assert_2 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_assert_4 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_post : Valid
[wp] [Qed] Goal typed_linked_n_before_last_assign : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_preserved_part1 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_2_preserved : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_3 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_7 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_6 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_5 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_4 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assign_part1 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_9 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assert_8 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_assign_part2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_direct_assert : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_direct_assign : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_direct_assert_3 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_direct_assert_2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_right_assign : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_right_assert : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_right_direct_assert_2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_right_direct_assert : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_right_direct_assign : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_right_direct_assert_3 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assert_2 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assert : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_inv_preserved_part1 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assert_3 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_inv_2_preserved : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assert_5 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assert_4 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_term_positive : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assign_part2 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_assign_part1 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_right_assign : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_right_assert : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_assign : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_term_positive : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_assign_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_assign_part1 : Valid
[wp] [Qed] Goal typed_index_of_post_2_part1 : Valid
[wp] [Qed] Goal typed_index_of_post_2_part2 : Valid
[wp] [Qed] Goal typed_index_of_post_2_part6 : Valid
[wp] [Qed] Goal typed_index_of_post_2_part5 : Valid
[wp] [Qed] Goal typed_index_of_post_2_part4 : Valid
[wp] [Qed] Goal typed_index_of_post_2_part3 : Valid
[wp] [Qed] Goal typed_index_of_post_3_part3 : Valid
[wp] [Qed] Goal typed_index_of_post_3_part2 : Valid
[wp] [Qed] Goal typed_index_of_post_3_part1 : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_loop_assign : Valid
[wp] [Qed] Goal typed_index_of_assert : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_index_of_assign_part3 : Valid
[wp] [Qed] Goal typed_index_of_assign_part2 : Valid
[wp] [Qed] Goal typed_index_of_assign_part1 : Valid
[wp] [Qed] Goal typed_index_of_loop_term_positive : Valid
[wp] [Qed] Goal typed_index_of_loop_term_decrease : Valid
[wp] [Qed] Goal typed_index_of_assign_part4 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_term_decrease : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_assign : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_assign : Valid
[wp] [Qed] Goal typed_index_of_unexisting_item_assign : Valid
[wp] [Qed] Goal typed_index_of_unexisting_item_assert : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_term_positive : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_assign : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_assign : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_term_positive : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_term_decrease : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_term_decrease : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_assign : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_assign : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_assign_exit : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_post_part2 : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_post_part1 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_term_positive : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_call_index_of_pre_part1 : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_assign_normal_part2 : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_assign_normal_part1 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_post_part1 : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_call_index_of_pre_2 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_assign_exit_part1 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_assign_normal_part1 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_assign_exit_part2 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_call_index_of_pre_2 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_call_index_of_pre_part2 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_call_index_of_pre_part1 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_assign_normal_part2 : Valid
[wp] [Qed] Goal typed_array_pop_post : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_call_index_of_up_unexisting_i____3 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_call_index_of_up_unexisting_i___ : Valid
[wp] [Qed] Goal typed_array_pop_post_LinkedLeft : Valid
[wp] [Qed] Goal typed_array_pop_post_2 : Valid
[wp] [Qed] Goal typed_array_pop_post_GhostSeparation : Valid
[wp] [Qed] Goal typed_array_pop_assert_2 : Valid
[wp] [Qed] Goal typed_array_pop_assert : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_established : Valid
[wp] [Qed] Goal typed_array_pop_assert_3 : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_IInBounds_established_part1 : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_IInBounds_preserved_part2 : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_LeftLinked_established : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_IInBounds_established_part2 : Valid
[wp] [Qed] Goal typed_array_pop_assert_4 : Valid
[wp] [Qed] Goal typed_array_pop_assert_7 : Valid
[wp] [Qed] Goal typed_array_pop_assert_6 : Valid
[wp] [Qed] Goal typed_array_pop_assert_5 : Valid
[wp] [Qed] Goal typed_array_pop_assert_11 : Valid
[wp] [Qed] Goal typed_array_pop_assert_10 : Valid
[wp] [Qed] Goal typed_array_pop_assert_9 : Valid
[wp] [Qed] Goal typed_array_pop_assert_8 : Valid
[wp] [Qed] Goal typed_array_pop_assert_15 : Valid
[wp] [Qed] Goal typed_array_pop_assert_14 : Valid
[wp] [Qed] Goal typed_array_pop_assert_13 : Valid
[wp] [Qed] Goal typed_array_pop_assert_12 : Valid
[wp] [Qed] Goal typed_array_pop_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_array_pop_assert_17 : Valid
[wp] [Qed] Goal typed_array_pop_assert_16 : Valid
[wp] [Qed] Goal typed_array_pop_assign_part3 : Valid
[wp] [Qed] Goal typed_array_pop_assign_part2 : Valid
[wp] [Qed] Goal typed_array_pop_assign_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_array_push_post_GhostSeparation_part1 : Valid
[wp] [Qed] Goal typed_array_pop_loop_term_positive : Valid
[wp] [Qed] Goal typed_array_pop_loop_term_decrease : Valid
[wp] [Qed] Goal typed_array_push_post_GhostSeparation_3_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_GhostSeparation_2_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_Separation_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_Separation_2_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_part1 : Valid
[wp] [Qed] Goal typed_array_push_assert_2 : Valid
[wp] [Qed] Goal typed_array_push_assert : Valid
[wp] [Qed] Goal typed_array_push_assert_4 : Valid
[wp] [Qed] Goal typed_array_push_assert_3 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_2_preserved_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_established : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_3_preserved_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_2_preserved_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_3_preserved_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_GhostSeparation_established : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_IInBounds_preserved_part3 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_IInBounds_preserved_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_IInBounds_established_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_LeftLinked_established : Valid
[wp] [Qed] Goal typed_array_push_assert_7 : Valid
[wp] [Qed] Goal typed_array_push_assert_6 : Valid
[wp] [Qed] Goal typed_array_push_assert_5 : Valid
[wp] [Qed] Goal typed_array_push_assert_11 : Valid
[wp] [Qed] Goal typed_array_push_assert_10 : Valid
[wp] [Qed] Goal typed_array_push_assert_9 : Valid
[wp] [Qed] Goal typed_array_push_assert_8 : Valid
[wp] [Qed] Goal typed_array_push_assert_15 : Valid
[wp] [Qed] Goal typed_array_push_assert_14 : Valid
[wp] [Qed] Goal typed_array_push_assert_13 : Valid
[wp] [Qed] Goal typed_array_push_assert_12 : Valid
[wp] [Qed] Goal typed_array_push_assert_19 : Valid
[wp] [Qed] Goal typed_array_push_assert_18 : Valid
[wp] [Qed] Goal typed_array_push_assert_17 : Valid
[wp] [Qed] Goal typed_array_push_assert_16 : Valid
[wp] [Qed] Goal typed_array_push_assert_23 : Valid
[wp] [Qed] Goal typed_array_push_assert_22 : Valid
[wp] [Qed] Goal typed_array_push_assert_21 : Valid
[wp] [Qed] Goal typed_array_push_assert_20 : Valid
[wp] [Qed] Goal typed_array_push_assert_27 : Valid
[wp] [Qed] Goal typed_array_push_assert_26 : Valid
[wp] [Qed] Goal typed_array_push_assert_25 : Valid
[wp] [Qed] Goal typed_array_push_assert_24 : Valid
[wp] [Qed] Goal typed_array_push_assert_31 : Valid
[wp] [Qed] Goal typed_array_push_assert_30 : Valid
[wp] [Qed] Goal typed_array_push_assert_29 : Valid
[wp] [Qed] Goal typed_array_push_assert_28 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part3 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_array_push_assert_32 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part7 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part6 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part4 : Valid
[wp] [Qed] Goal typed_array_push_assign_part3 : Valid
[wp] [Qed] Goal typed_array_push_assign_part2 : Valid
[wp] [Qed] Goal typed_array_push_assign_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_term_decrease_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_term_decrease_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_term_positive_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_term_positive_part1 : Valid
[wp] [Qed] Goal typed_list_final_add_post_5 : Valid
[wp] [Qed] Goal typed_list_final_add_post_GhostSeparation : Valid
[wp] [Qed] Goal typed_list_final_add_assert : Valid
[wp] [Qed] Goal typed_list_final_add_assert_4 : Valid
[wp] [Qed] Goal typed_list_final_add_assert_3 : Valid
[wp] [Qed] Goal typed_list_final_add_assert_2 : Valid
[wp] [Qed] Goal typed_list_final_add_assert_8 : Valid
[wp] [Qed] Goal typed_list_final_add_assert_7 : Valid
[wp] [Qed] Goal typed_list_final_add_assert_6 : Valid
[wp] [Qed] Goal typed_list_final_add_assert_5 : Valid
[wp] [Qed] Goal typed_list_final_add_assign_part2 : Valid
[wp] [Qed] Goal typed_list_final_add_assign_part1 : Valid
[wp] 1552 goals generated
[wp] Running WP plugin...
[rte] annotating function list_init
[rte] annotating function list_head
[rte] annotating function list_tail
[rte] annotating function list_pop
[rte] annotating function list_push
[rte] annotating function list_length
[rte] annotating function list_chop
[rte] annotating function list_add
[rte] annotating function list_remove
[rte] annotating function list_copy
[rte] annotating function list_item_next
[rte] annotating function linked_n_starting_from_null_empty
[rte] annotating function linked_n_all_elements_valid
[rte] annotating function linked_n_first_valid
[rte] annotating function linked_n_bounds
[rte] annotating function linked_n_valid_range
[rte] annotating function linked_n_next_of_all_indexes
[rte] annotating function linked_n_before_last
[rte] annotating function linked_n_split_segment
[rte] annotating function linked_n_split_segment_direct
[rte] annotating function linked_n_split_segment_right
[rte] annotating function linked_n_split_segment_right_direct
[rte] annotating function linked_n_merge_segment
[rte] annotating function linked_n_merge_segment_right
[rte] annotating function linked_n_all_elements
[rte] annotating function index_of
[rte] annotating function index_of_not_in_subrange
[rte] annotating function index_of_unexisting_item
[rte] annotating function index_of_up_unexisting_item
[rte] annotating function index_of_inter_existing_item
[rte] annotating function index_of_bounds_weak
[rte] annotating function index_of_existing_item_weak
[rte] annotating function array_pop
[rte] annotating function array_push
[rte] annotating function list_final_add
[wp] Computing [1566 goals...]
[wp] Computing [1601 goals...]
[wp] Computing [1602 goals...]
[wp] Computing [1622 goals...]
[wp] Computing [1653 goals...]
[wp] Computing [1653 goals...]
[wp] Computing [1653 goals...]
[wp] Computing [1687 goals...]
[wp] Computing [1687 goals...]
[wp] Computing [1717 goals...]
[wp] Computing [1737 goals...]
[wp] Computing [1762 goals...]
[wp] 1165 goals scheduled
[wp] [Qed] Goal typed_list_init_assert_rte_mem_access : Valid
[wp] [Qed] Goal typed_list_tail_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_list_tail_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_list_tail_loop_inv_4_established : Valid
[wp] [Qed] Goal typed_list_tail_assert_rte_mem_access_4 : Valid
[wp] [Qed] Goal typed_list_tail_not_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_tail_not_empty_post_2_part1 : Valid
[wp] [Qed] Goal typed_list_tail_not_empty_post_3_part1 : Valid
[wp] [Qed] Goal typed_list_pop_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_pop_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_list_pop_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_list_pop_assert_rte_mem_access_5 : Valid
[wp] [Qed] Goal typed_list_pop_assert_rte_mem_access_7 : Valid
[wp] [Qed] Goal typed_list_pop_assert_rte_mem_access_6 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_post_4_part2 : Valid
[wp] [Qed] Goal typed_list_pop_empty_assign_part1 : Valid
[wp] [Qed] Goal typed_list_pop_more_post_part1 : Valid
[wp] [Qed] Goal typed_list_push_stmt_post_part2 : Valid
[wp] [Qed] Goal typed_list_push_stmt_post_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_4_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_5_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_4_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_6_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_5_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_7_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_6_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_8_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_7_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_9_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_8_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_9_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_10_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_signed_overflow_10_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_4_part1 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_4_part3 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_4_part2 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part01 : Valid
[wp] [Qed] Goal typed_list_push_assert_rte_mem_access_4_part4 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part03 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part02 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part05 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part04 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part07 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part06 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part09 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part08 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part11 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part10 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part13 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part12 : Valid
[wp] [Qed] Goal typed_list_push_assign_exit_part14 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part01 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part03 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part02 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part05 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part04 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part07 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part06 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part09 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part08 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part11 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part10 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part13 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part12 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part14 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part16 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part18 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part17 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part20 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part19 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part22 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part21 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part24 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part23 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part26 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part25 : Valid
[wp] [Qed] Goal typed_list_push_assign_normal_part27 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_3_part1 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_index_of_inter_existing_item_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part5 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part4 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part6 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_part8 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Item_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Item_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_push_call_list_remove_pre_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_4_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_4_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_push_contains_item_post_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_GhostSeparation_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_push_does_not_contain_item_post_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_length_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_list_length_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_list_chop_post_GhostSeparation_3_part1 : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_4 : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_5 : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_6 : Valid
[wp] [Qed] Goal typed_list_chop_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_9 : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_10 : Valid
[wp] [Qed] Goal typed_list_chop_assert_rte_mem_access_11 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part1 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part3 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part2 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part5 : Valid
[wp] [Qed] Goal typed_list_chop_assign_exit_part4 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part02 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part01 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part04 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part03 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part06 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part05 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part08 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part07 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part09 : Valid
[wp] [Qed] Goal typed_list_chop_assign_normal_part11 : Valid
[wp] [Qed] Goal typed_list_chop_loop_term_decrease : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_part1 : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_part3 : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_2_part1 : Valid
[wp] [Qed] Goal typed_list_chop_empty_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_part3 : Valid
[wp] [Qed] Goal typed_list_chop_one_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_chop_more_post_4_part1 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_post_GhostSeparation_2_part8 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_4_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_4_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_5_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_5_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_6_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_6_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_7_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_7_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_8_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_8_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_9_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_signed_overflow_9_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_part3 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_3_part1 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_4_part2 : Valid
[wp] [Qed] Goal typed_list_add_assert_rte_mem_access_4_part3 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part01 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part02 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part04 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part03 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part06 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part05 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part08 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part07 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part10 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part09 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part12 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part11 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part14 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part13 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part16 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part15 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part18 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part17 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part20 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part19 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part22 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part21 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part23 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part25 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part27 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part26 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part29 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part28 : Valid
[wp] [Qed] Goal typed_list_add_assign_exit_part31 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part01 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part03 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part02 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part05 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part04 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part07 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part06 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part09 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part08 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part11 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part10 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part13 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part12 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part15 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part14 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part17 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part16 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part19 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part18 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part21 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part20 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part23 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part22 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part25 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part26 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part28 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part29 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part31 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part30 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part33 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part34 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part36 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part35 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part37 : Valid
[wp] [Qed] Goal typed_list_add_assign_normal_part39 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_3_part1 : Valid
[wp] [Qed] Goal typed_list_add_call_index_of_inter_existing_item_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part6 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part5 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_part8 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Item_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Item_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_remove_pre_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_tail_pre_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part01 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part03 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part04 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part06 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part05 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part08 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part07 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part10 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part09 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_part12 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part02 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part04 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part05 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part07 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part06 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part09 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part08 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_2_part11 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part6 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_3_part5 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Linked_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_GhostSeparation_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Item_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Item_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Separation_2_part2 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_call_list_final_add_pre_Unique_part2 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_part8 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_3_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_4_part8 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_5_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_GhostSeparation_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Separation_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part4 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_add_contains_item_post_Unique_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part2 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_End_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part2 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_3_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_GhostSeparation_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Separation_2_part5 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part4 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_add_does_not_contain_item_post_Unique_part5 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part1 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part4 : Valid
[wp] [Qed] Goal typed_list_remove_post_GhostSeparation_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part1 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part3 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part4 : Valid
[wp] [Qed] Goal typed_list_remove_post_UnchangedItem_part6 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_5 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_6 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_8 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_7 : Valid
[wp] [Qed] Goal typed_list_remove_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_list_remove_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_list_remove_loop_inv_7_established : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_10 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_11 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_12_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_13_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_12_part2 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_14_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_14_part2 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_mem_access_15_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_2_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_3_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_4_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_5_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_4_part2 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_6_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_5_part2 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_7_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assert_rte_signed_overflow_8_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part1 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part2 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part4 : Valid
[wp] [Qed] Goal typed_list_remove_assign_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Linked_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Linked_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_ItemNotIn_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_ItemNotIn_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_IttemSep_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_IttemSep_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unchanged_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Unchanged_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Swiped_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_Swiped_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part1 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part4 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_PrevItem_part6 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_UnchangedSwipe_part3 : Valid
[wp] [Qed] Goal typed_list_remove_contains_item_post_UnchangedSwipe_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part1 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part4 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_3_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_3_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_GhostSeparation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_GhostSeparation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_2_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Separation_2_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Unique_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_Unique_part6 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_4_part3 : Valid
[wp] [Qed] Goal typed_list_remove_does_not_contain_item_post_4_part6 : Valid
[wp] [Qed] Goal typed_list_copy_assert_rte_mem_access_2 : Valid
[wp] [Qed] Goal typed_list_copy_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_list_item_next_not_empty_post_part1 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_valid_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_valid_range_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_next_of_all_indexes_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_inv_preserved_part1 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_before_last_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_preserved_part1 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_split_segment_loop_term_decrease : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_inv_preserved_part1 : Valid
[wp] [Qed] Goal typed_linked_n_merge_segment_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_linked_n_all_elements_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_not_in_subrange_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_index_of_up_unexisting_item_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_preserved_part2 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_established_part2 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_established_part1 : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_2_established : Valid
[wp] [Qed] Goal typed_index_of_inter_existing_item_loop_inv_3_established : Valid
[wp] [Qed] Goal typed_index_of_bounds_weak_call_index_of_pre_part1 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_post_part1 : Valid
[wp] [Qed] Goal typed_index_of_existing_item_weak_call_index_of_up_unexisting_i___ : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_established : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_IInBounds_preserved_part2 : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_IInBounds_established_part1 : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_IInBounds_established_part2 : Valid
[wp] [Qed] Goal typed_array_pop_loop_inv_LeftLinked_established : Valid
[wp] [Qed] Goal typed_array_pop_assert_rte_signed_overflow_5 : Valid
[wp] [Qed] Goal typed_array_pop_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_GhostSeparation_2_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_GhostSeparation_3_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_Separation_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_Separation_2_part1 : Valid
[wp] [Qed] Goal typed_array_push_post_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_established : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_GhostSeparation_established : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_IInBounds_preserved_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_IInBounds_preserved_part3 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_IInBounds_established_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_inv_LeftLinked_established : Valid
[wp] [Qed] Goal typed_array_push_assert_rte_signed_overflow_9 : Valid
[wp] [Qed] Goal typed_array_push_assert_rte_mem_access_3 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part3 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part2 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part4 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part6 : Valid
[wp] [Qed] Goal typed_array_push_assign_part1 : Valid
[wp] [Qed] Goal typed_array_push_loop_assign_part7 : Valid
[wp] [Qed] Goal typed_array_push_assign_part3 : Valid
[wp] [Qed] Goal typed_array_push_assign_part2 : Valid
[wp] 1780 goals generated
