YES Problem: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) Proof: DP Processor: DPs: foo#(0(x1)) -> p#(s(x1)) foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> p#(s(s(p(s(x1))))) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar#(0(x1)) -> p#(s(s(s(x1)))) bar#(s(x1)) -> p#(s(s(x1))) bar#(s(x1)) -> p#(p(s(s(x1)))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p#(p(s(x1))) -> p#(x1) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) TDG Processor: DPs: foo#(0(x1)) -> p#(s(x1)) foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> p#(s(s(p(s(x1))))) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar#(0(x1)) -> p#(s(s(s(x1)))) bar#(s(x1)) -> p#(s(s(x1))) bar#(s(x1)) -> p#(p(s(s(x1)))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p#(p(s(x1))) -> p#(x1) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> p#(s(s(x1))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(x1))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(x1)) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(0(x1)) -> p#(s(x1)) bar#(0(x1)) -> p#(s(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(p(s(s(x1)))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(s(x1))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(0(x1)) -> p#(s(s(s(x1)))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(s(p(s(x1))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(x1))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(s(x1)) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) foo#(0(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) EDG Processor: DPs: foo#(0(x1)) -> p#(s(x1)) foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> p#(s(s(p(s(x1))))) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar#(0(x1)) -> p#(s(s(s(x1)))) bar#(s(x1)) -> p#(s(s(x1))) bar#(s(x1)) -> p#(p(s(s(x1)))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p#(p(s(x1))) -> p#(x1) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(x1)) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(x1))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(0(x1)) -> p#(s(s(s(x1)))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(s(x1))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(p(s(s(x1)))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(s(x1)) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(x1))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) CDG Processor: DPs: foo#(0(x1)) -> p#(s(x1)) foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> p#(s(s(p(s(x1))))) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar#(0(x1)) -> p#(s(s(s(x1)))) bar#(s(x1)) -> p#(s(s(x1))) bar#(s(x1)) -> p#(p(s(s(x1)))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p#(p(s(x1))) -> p#(x1) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> p#(p(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(bar(p(p(s(s(p(s(x1))))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(s(p(s(x1))))) bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) -> foo#(s(x1)) -> p#(s(x1)) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(p(s(s(foo(s(p(p(s(s(x1)))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(s(foo(s(p(p(s(s(x1))))))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(p(s(s(x1)))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(s(x1)) -> p#(s(s(x1))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) -> bar#(0(x1)) -> p#(s(s(s(x1)))) foo#(s(x1)) -> p#(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(s(s(s(p(s(x1)))))) foo#(s(x1)) -> foo#(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))) -> foo#(0(x1)) -> p#(s(x1)) foo#(0(x1)) -> p#(p(p(s(s(s(p(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) foo#(0(x1)) -> p#(p(s(s(s(p(s(x1))))))) -> p#(p(s(x1))) -> p#(x1) SCC Processor: #sccs: 1 #rules: 2 #arcs: 33/676 DPs: bar#(s(x1)) -> foo#(s(p(p(s(s(x1)))))) foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [bar#](x0) = -5x0 + 0, [foo#](x0) = -10x0 + 0, [bar](x0) = 12, [p](x0) = -5x0 + 0, [s](x0) = 5x0 + 11, [foo](x0) = 6, [0](x0) = 0 orientation: bar#(s(x1)) = x1 + 6 >= -5x1 + 1 = foo#(s(p(p(s(s(x1)))))) foo#(s(x1)) = -5x1 + 1 >= -5x1 + 1 = bar#(p(p(s(s(p(s(x1))))))) foo(0(x1)) = 6 >= 0 = 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) = 6 >= 6 = p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) = 12 >= 0 = 0(p(s(s(s(x1))))) bar(s(x1)) = 12 >= 6 = p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) = -5x1 + 1 >= -5x1 + 0 = p(x1) p(s(x1)) = x1 + 6 >= x1 = x1 p(0(x1)) = 0 >= 0 = 0(s(s(s(s(x1))))) problem: DPs: foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) EDG Processor: DPs: foo#(s(x1)) -> bar#(p(p(s(s(p(s(x1))))))) TRS: foo(0(x1)) -> 0(s(p(p(p(s(s(s(p(s(x1)))))))))) foo(s(x1)) -> p(s(p(p(p(s(s(p(s(s(p(s(foo(p(p(s(s(p(s(bar(p(p(s(s(p(s(x1)))))))))))))))))))))))))) bar(0(x1)) -> 0(p(s(s(s(x1))))) bar(s(x1)) -> p(s(p(p(s(s(foo(s(p(p(s(s(x1)))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: Qed