YES Problem: thrice(0(x1)) -> p(s(p(p(p(s(s(s(0(p(s(p(s(x1))))))))))))) thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))))))) half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1)))))))))))) half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(0(x1)) -> p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1)))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) 0(x1) -> x1 Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [half](x0) = x0, [sixtimes](x0) = 14x0, [p](x0) = x0, [s](x0) = x0, [thrice](x0) = 14x0, [0](x0) = 7x0 orientation: thrice(0(x1)) = 21x1 >= 7x1 = p(s(p(p(p(s(s(s(0(p(s(p(s(x1))))))))))))) thrice(s(x1)) = 14x1 >= 14x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))))))) half(0(x1)) = 7x1 >= 7x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1)))))))))))) half(s(x1)) = x1 >= x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) = x1 >= x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(0(x1)) = 21x1 >= 7x1 = p(s(p(s(0(s(s(s(s(s(p(s(p(s(x1)))))))))))))) sixtimes(s(x1)) = 14x1 >= 14x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = 7x1 >= 7x1 = 0(s(s(s(s(x1))))) 0(x1) = 7x1 >= x1 = x1 problem: thrice(s(x1)) -> p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))))))) half(0(x1)) -> p(p(s(s(p(s(0(p(s(s(s(s(x1)))))))))))) half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(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: [half](x0) = 1x0, [sixtimes](x0) = 3x0, [p](x0) = x0, [s](x0) = x0, [thrice](x0) = 8x0, [0](x0) = x0 orientation: thrice(s(x1)) = 8x1 >= 4x1 = p(p(s(s(half(p(p(s(s(p(s(sixtimes(p(s(p(p(s(s(x1)))))))))))))))))) half(0(x1)) = 1x1 >= x1 = p(p(s(s(p(s(0(p(s(s(s(s(x1)))))))))))) half(s(x1)) = 1x1 >= 1x1 = p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) = 1x1 >= 1x1 = p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) = 3x1 >= 3x1 = p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = x1 >= x1 = 0(s(s(s(s(x1))))) problem: half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) DP Processor: DPs: half#(s(x1)) -> p#(s(x1)) half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(s(x1))) -> p#(s(x1)) half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(x1)))) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(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: half#(s(x1)) -> p#(s(x1)) half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(s(x1))) -> p#(s(x1)) half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(x1)))) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(s(s(x1)))) sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(s(s(s(x1)))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(s(s(p(s(x1))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(x1)) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(x1)) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(s(s(p(s(x1))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(s(x1)) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(x1)) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(x1)) EDG Processor: DPs: half#(s(x1)) -> p#(s(x1)) half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(s(x1))) -> p#(s(x1)) half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(x1)))) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(s(s(x1)))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) -> sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(x1) p#(p(s(x1))) -> p#(x1) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(x1)) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(x1)) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(x1)) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(x1)) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) -> half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) CDG Processor: DPs: half#(s(x1)) -> p#(s(x1)) half#(s(x1)) -> p#(s(s(p(s(x1))))) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) half#(s(x1)) -> half#(p(p(s(s(p(s(x1))))))) half#(s(x1)) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(x1)) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) half#(s(x1)) -> p#(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half#(s(s(x1))) -> p#(s(x1)) half#(s(s(x1))) -> p#(s(s(p(s(x1))))) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) half#(s(s(x1))) -> half#(p(p(s(s(p(s(x1))))))) half#(s(s(x1))) -> p#(s(s(half(p(p(s(s(p(s(x1)))))))))) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) half#(s(s(x1))) -> p#(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))) half#(s(s(x1))) -> p#(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(x1)))) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) sixtimes#(s(x1)) -> p#(s(p(p(p(s(s(s(x1)))))))) sixtimes#(s(x1)) -> sixtimes#(p(s(p(p(p(s(s(s(x1))))))))) sixtimes#(s(x1)) -> p#(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))) sixtimes#(s(x1)) -> p#(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) sixtimes#(s(x1)) -> p#(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))))))))))) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p#(p(s(x1))) -> p#(x1) TRS: half(s(x1)) -> p(s(p(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))))) half(s(s(x1))) -> p(s(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1)))))))))))))))) sixtimes(s(x1)) -> p(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(x1))))) graph: sixtimes#(s(x1)) -> p#(p(p(s(s(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1)))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(s(s(s(s(s(s(p(p(s(p(s(s(s(sixtimes(p(s(p(p(p(s(s(s(x1))))))))))))))))))))))))) -> p#(p(s(x1))) -> p#(x1) sixtimes#(s(x1)) -> p#(p(s(s(s(x1))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(s(x1))) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(half(p(p(s(s(p(s(x1))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(p(p(s(s(half(p(p(s(s(p(s(x1))))))))))))))) -> p#(p(s(x1))) -> p#(x1) half#(s(x1)) -> p#(p(s(s(p(s(x1)))))) -> p#(p(s(x1))) -> p#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 9/784