| Obligations |
| lmem_dec |
| inter_com |
| inter_add_l |
| inter_not_add_l |
| diff_add_l |
| diff_not_add_l |
| subset_add_r |
| union_add_l |
| union_add_r |
| union_com |
| union_var_l |
| union_var_r |
| set_of_elt |
| elt_set_of |
| subset_set_of |
| elts_cons |
| elts_app |
| list_simpl_r |
| snoc_app |
| precedes_mem |
| head_precedes |
| precedes_tail |
| tail_not_precedes |
| split_list_precedes |
| precedes_refl |
| precedes_append_left |
| precedes_append_left_iff |
| precedes_append_right |
| precedes_append_right_iff |
| simplelist_tl |
| simplelist_split |
| simplelist_app_disjoint |
| simplelist_length |
| precedes_antisym |
| precedes_trans |
| reachable_refl |
| reachable_trans |
| xpath_xedge |
| same_scc_refl |
| same_scc_sym |
| same_scc_trans |
| subscc_add |
| scc_max |
| subscc_after_last_gray |
| wf_color_postcond_split |
| wf_color_sccs |
| wf_color_3_cases |
| num_lmem |
| num_rank_strict |
| simplelist_x_prec_strict_y' |
| 51. VC for split |
| 52. VC for popuntil |
| 53. VC for popuntil_lstack |
| 54. VC for add_stack_incr |
| 55. VC for add_black |
| 56. VC for set_infty |
| 57. VC for dfs1 |
| 58. VC for dfs |
| 59. VC for gabow |