MAYBE 0.07/0.18 MAYBE 0.07/0.18 0.07/0.18 Problem: 0.07/0.18 t(N) -> cs(r(q(N)),nt(ns(N))) 0.07/0.18 q(0()) -> 0() 0.07/0.18 q(s(X)) -> s(p(q(X),d(X))) 0.07/0.18 d(0()) -> 0() 0.07/0.18 d(s(X)) -> s(s(d(X))) 0.07/0.18 p(0(),X) -> X 0.07/0.18 p(X,0()) -> X 0.07/0.18 p(s(X),s(Y)) -> s(s(p(X,Y))) 0.07/0.18 f(0(),X) -> nil() 0.07/0.18 f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) 0.07/0.18 t(X) -> nt(X) 0.07/0.18 s(X) -> ns(X) 0.07/0.18 f(X1,X2) -> nf(X1,X2) 0.07/0.18 a(nt(X)) -> t(a(X)) 0.07/0.18 a(ns(X)) -> s(a(X)) 0.07/0.18 a(nf(X1,X2)) -> f(a(X1),a(X2)) 0.07/0.18 a(X) -> X 0.07/0.18 0.07/0.18 Proof: 0.07/0.18 Open 0.07/0.19 EOF