MAYBE 0.18/0.20 MAYBE 0.18/0.20 0.18/0.20 Problem: 0.18/0.20 average(x,y) -> if(ge(x,y),x,y) 0.18/0.20 if(true(),x,y) -> averIter(y,x,y) 0.18/0.20 if(false(),x,y) -> averIter(x,y,x) 0.18/0.20 averIter(x,y,z) -> ifIter(ge(x,y),x,y,z) 0.18/0.20 ifIter(true(),x,y,z) -> z 0.18/0.20 ifIter(false(),x,y,z) -> averIter(plus(x,s(s(s(0())))),plus(y,s(0())),plus(z,s(0()))) 0.18/0.20 append(nil(),y) -> y 0.18/0.20 append(cons(n,x),y) -> cons(n,app(x,y)) 0.18/0.20 low(n,nil()) -> nil() 0.18/0.20 low(n,cons(m,x)) -> if_low(ge(m,n),n,cons(m,x)) 0.18/0.20 if_low(false(),n,cons(m,x)) -> cons(m,low(n,x)) 0.18/0.20 if_low(true(),n,cons(m,x)) -> low(n,x) 0.18/0.20 high(n,nil()) -> nil() 0.18/0.20 high(n,cons(m,x)) -> if_high(ge(m,n),n,cons(m,x)) 0.18/0.20 if_high(false(),n,cons(m,x)) -> high(n,x) 0.18/0.20 if_high(true(),n,cons(m,x)) -> cons(average(m,m),high(n,x)) 0.18/0.20 quicksort(x) -> ifquick(isempty(x),x) 0.18/0.20 ifquick(true(),x) -> nil() 0.18/0.20 ifquick(false(),x) -> 0.18/0.20 append(quicksort(low(head(x),tail(x))),cons(tail(x),quicksort(high(head(x),tail(x))))) 0.18/0.20 plus(0(),y) -> y 0.18/0.20 plus(s(x),y) -> s(plus(x,y)) 0.18/0.20 isempty(nil()) -> true() 0.18/0.20 isempty(cons(n,x)) -> false() 0.18/0.20 head(nil()) -> error() 0.18/0.20 head(cons(n,x)) -> n 0.18/0.20 tail(nil()) -> nil() 0.18/0.20 tail(cons(n,x)) -> x 0.18/0.20 ge(x,0()) -> true() 0.18/0.20 ge(0(),s(y)) -> false() 0.18/0.20 ge(s(x),s(y)) -> ge(x,y) 0.18/0.20 a() -> b() 0.18/0.20 a() -> c() 0.18/0.20 0.18/0.20 Proof: 0.18/0.20 Open 0.18/0.21 EOF