119.77/60.10 MAYBE 119.77/60.10 119.77/60.10 Problem: 119.77/60.10 max(x,0()) -> x 119.77/60.10 max(0(),y) -> y 119.77/60.10 max(s(x),s(y)) -> s(max(x,y)) 119.77/60.10 max(x,y) -> max(y,x) 119.77/60.10 max(x,x) -> x 119.77/60.10 119.77/60.10 Proof: 119.77/60.10 Open 119.77/60.11 EOF