MAYBE 232.62/58.94 MAYBE 232.62/58.94 232.62/58.94 Problem: 232.62/58.94 top(free(x)) -> top(check(new(x))) 232.62/58.94 new(free(x)) -> free(new(x)) 232.62/58.94 old(free(x)) -> free(old(x)) 232.62/58.94 new(serve()) -> free(serve()) 232.62/58.94 old(serve()) -> free(serve()) 232.62/58.94 check(free(x)) -> free(check(x)) 232.62/58.94 check(new(x)) -> new(check(x)) 232.62/58.94 check(old(x)) -> old(check(x)) 232.62/58.94 check(old(x)) -> old(x) 232.62/58.94 232.62/58.94 Proof: 232.62/58.94 Open 232.62/58.94 EOF