YES 3 decompositions #0 ----------- 4: hd(:(x,y)) -> x #1 ----------- 6: d(:(x,y)) -> :(x,:(x,d(y))) #2 ----------- 1: nats() -> :(0(),inc(nats())) 2: inc(:(x,y)) -> :(s(x),inc(y)) 3: inc(tl(nats())) -> tl(inc(nats())) 5: tl(:(x,y)) -> y @Mutually Orthogonal --- R 4: hd(:(x,y)) -> x --- S 4: hd(:(x,y)) -> x @Mutually Orthogonal --- R 6: d(:(x,y)) -> :(x,:(x,d(y))) --- S 6: d(:(x,y)) -> :(x,:(x,d(y))) @Rule Labeling --- R 1: nats() -> :(0(),inc(nats())) 2: inc(:(x,y)) -> :(s(x),inc(y)) 3: inc(tl(nats())) -> tl(inc(nats())) 5: tl(:(x,y)) -> y --- S 1: nats() -> :(0(),inc(nats())) 2: inc(:(x,y)) -> :(s(x),inc(y)) 3: inc(tl(nats())) -> tl(inc(nats())) 5: tl(:(x,y)) -> y