YES Problem: log(s(x1)) -> s(log(half(s(x1)))) half(0(x1)) -> 0(s(s(half(x1)))) half(s(0(x1))) -> 0(x1) half(s(s(x1))) -> s(half(p(s(s(x1))))) half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) p(s(s(s(x1)))) -> s(p(s(s(x1)))) s(s(p(s(x1)))) -> s(s(x1)) 0(x1) -> x1 Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [p](x0) = x0, [0](x0) = 4x0, [half](x0) = x0, [log](x0) = x0, [s](x0) = x0 orientation: log(s(x1)) = x1 >= x1 = s(log(half(s(x1)))) half(0(x1)) = 4x1 >= 4x1 = 0(s(s(half(x1)))) half(s(0(x1))) = 4x1 >= 4x1 = 0(x1) half(s(s(x1))) = x1 >= x1 = s(half(p(s(s(x1))))) half(half(s(s(s(s(x1)))))) = x1 >= x1 = s(s(half(half(x1)))) p(s(s(s(x1)))) = x1 >= x1 = s(p(s(s(x1)))) s(s(p(s(x1)))) = x1 >= x1 = s(s(x1)) 0(x1) = 4x1 >= x1 = x1 problem: log(s(x1)) -> s(log(half(s(x1)))) half(0(x1)) -> 0(s(s(half(x1)))) half(s(0(x1))) -> 0(x1) half(s(s(x1))) -> s(half(p(s(s(x1))))) half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) p(s(s(s(x1)))) -> s(p(s(s(x1)))) s(s(p(s(x1)))) -> s(s(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 2 ] [p](x0) = [-& 0 ]x0, [1 2] [0](x0) = [0 3]x0, [0 2] [half](x0) = [0 0]x0, [2 2 ] [log](x0) = [-& 2 ]x0, [0 0 ] [s](x0) = [-& -&]x0 orientation: [2 2 ] [2 2 ] log(s(x1)) = [-& -&]x1 >= [-& -&]x1 = s(log(half(s(x1)))) [2 5] [1 3] half(0(x1)) = [1 3]x1 >= [0 2]x1 = 0(s(s(half(x1)))) [1 3] [1 2] half(s(0(x1))) = [1 3]x1 >= [0 3]x1 = 0(x1) [0 0] [0 0 ] half(s(s(x1))) = [0 0]x1 >= [-& -&]x1 = s(half(p(s(s(x1))))) [2 2] [2 2 ] half(half(s(s(s(s(x1)))))) = [0 0]x1 >= [-& -&]x1 = s(s(half(half(x1)))) [0 0 ] [0 0 ] p(s(s(s(x1)))) = [-& -&]x1 >= [-& -&]x1 = s(p(s(s(x1)))) [0 0 ] [0 0 ] s(s(p(s(x1)))) = [-& -&]x1 >= [-& -&]x1 = s(s(x1)) problem: log(s(x1)) -> s(log(half(s(x1)))) half(s(0(x1))) -> 0(x1) half(s(s(x1))) -> s(half(p(s(s(x1))))) half(half(s(s(s(s(x1)))))) -> s(s(half(half(x1)))) p(s(s(s(x1)))) -> s(p(s(s(x1)))) s(s(p(s(x1)))) -> s(s(x1)) String Reversal Processor: s(log(x1)) -> s(half(log(s(x1)))) 0(s(half(x1))) -> 0(x1) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [p](x0) = [1 0 0]x0 [0 0 0] , [1 1 0] [1] [0](x0) = [0 0 0]x0 + [1] [1 1 0] [1], [1 0 0] [half](x0) = [0 0 0]x0 [0 1 0] , [1 0 0] [1] [log](x0) = [0 0 0]x0 + [0] [0 0 0] [0], [1 0 0] [0] [s](x0) = [0 0 1]x0 + [1] [0 0 0] [0] orientation: [1 0 0] [1] [1 0 0] [1] s(log(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(half(log(s(x1)))) [0 0 0] [0] [0 0 0] [0] [1 1 0] [2] [1 1 0] [1] 0(s(half(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = 0(x1) [1 1 0] [2] [1 1 0] [1] [1 0 0] [0] [1 0 0] [0] s(s(half(x1))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(s(p(half(s(x1))))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [0] [1 0 0] s(s(s(s(half(half(x1)))))) = [0 0 0]x1 + [1] >= [0 0 0]x1 = half(half(s(s(x1)))) [0 0 0] [0] [0 0 0] [1 0 0] [0] [1 0 0] [0] s(s(s(p(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(s(p(s(x1)))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [0] [1 0 0] [0] s(p(s(s(x1)))) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = s(s(x1)) [0 0 0] [0] [0 0 0] [0] problem: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) DP Processor: DPs: s#(log(x1)) -> s#(x1) s#(log(x1)) -> s#(half(log(s(x1)))) s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(p(x1)))) -> s#(x1) s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) EDG Processor: DPs: s#(log(x1)) -> s#(x1) s#(log(x1)) -> s#(half(log(s(x1)))) s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(p(x1)))) -> s#(x1) s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) graph: s#(log(x1)) -> s#(x1) -> s#(log(x1)) -> s#(x1) s#(log(x1)) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1)))) s#(log(x1)) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(log(x1)) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(log(x1)) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(log(x1)) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(log(x1)) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(log(x1)) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(log(x1)) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(log(x1)) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(half(x1))) -> s#(x1) -> s#(log(x1)) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1)))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(half(x1))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(half(x1))) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) -> s#(log(x1)) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(half(x1))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(log(x1)) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(log(x1)) -> s#(half(log(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(half(x1))) -> s#(p(half(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(half(x1))) -> s#(s(p(half(s(x1))))) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(p(s(x1))) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) SCC Processor: #sccs: 1 #rules: 6 #arcs: 56/100 DPs: s#(log(x1)) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(half(x1))) -> s#(x1) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) Arctic Interpretation Processor: dimension: 1 usable rules: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) interpretation: [s#](x0) = x0 + 0, [p](x0) = x0 + 0, [half](x0) = x0 + 5, [log](x0) = 1x0 + 6, [s](x0) = x0 + 0 orientation: s#(log(x1)) = 1x1 + 6 >= x1 + 0 = s#(x1) s#(s(s(p(x1)))) = x1 + 0 >= x1 + 0 = s#(s(p(s(x1)))) s#(s(s(p(x1)))) = x1 + 0 >= x1 + 0 = s#(x1) s#(s(s(s(half(half(x1)))))) = x1 + 5 >= x1 + 0 = s#(s(x1)) s#(s(s(s(half(half(x1)))))) = x1 + 5 >= x1 + 0 = s#(x1) s#(s(half(x1))) = x1 + 5 >= x1 + 0 = s#(x1) s(log(x1)) = 1x1 + 6 >= 1x1 + 6 = s(half(log(s(x1)))) s(s(half(x1))) = x1 + 5 >= x1 + 5 = s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) = x1 + 5 >= x1 + 5 = half(half(s(s(x1)))) s(s(s(p(x1)))) = x1 + 0 >= x1 + 0 = s(s(p(s(x1)))) s(p(s(s(x1)))) = x1 + 0 >= x1 + 0 = s(s(x1)) problem: DPs: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(half(x1))) -> s#(x1) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) Restore Modifier: DPs: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(half(x1))) -> s#(x1) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) EDG Processor: DPs: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(half(x1))) -> s#(x1) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) graph: s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(half(x1))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(half(x1))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(half(x1))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(half(x1))) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(p(x1)))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) -> s#(s(half(x1))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(p(x1)))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(s(x1)) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(s(s(half(half(x1)))))) -> s#(x1) s#(s(s(s(half(half(x1)))))) -> s#(x1) -> s#(s(half(x1))) -> s#(x1) Arctic Interpretation Processor: dimension: 1 usable rules: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) interpretation: [s#](x0) = 2x0 + 0, [p](x0) = -1x0 + 0, [half](x0) = x0 + 1, [log](x0) = 1, [s](x0) = 1x0 + 0 orientation: s#(s(s(p(x1)))) = 3x1 + 4 >= 3x1 + 3 = s#(s(p(s(x1)))) s#(s(s(p(x1)))) = 3x1 + 4 >= 2x1 + 0 = s#(x1) s#(s(s(s(half(half(x1)))))) = 5x1 + 6 >= 3x1 + 2 = s#(s(x1)) s#(s(s(s(half(half(x1)))))) = 5x1 + 6 >= 2x1 + 0 = s#(x1) s#(s(half(x1))) = 3x1 + 4 >= 2x1 + 0 = s#(x1) s(log(x1)) = 2 >= 2 = s(half(log(s(x1)))) s(s(half(x1))) = 2x1 + 3 >= 2x1 + 2 = s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) = 4x1 + 5 >= 2x1 + 1 = half(half(s(s(x1)))) s(s(s(p(x1)))) = 2x1 + 3 >= 2x1 + 2 = s(s(p(s(x1)))) s(p(s(s(x1)))) = 2x1 + 1 >= 2x1 + 1 = s(s(x1)) problem: DPs: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) Restore Modifier: DPs: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) EDG Processor: DPs: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) graph: s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) -> s#(s(s(p(x1)))) -> s#(s(p(s(x1)))) Matrix Interpretation Processor: dim=3 interpretation: [s#](x0) = [0 0 1]x0 + [1], [0 0 1] [p](x0) = [1 0 0]x0 [0 1 0] , [0] [half](x0) = [0] [0], [0 0 0] [log](x0) = [1 1 1]x0 [0 0 0] , [0 1 0] [1] [s](x0) = [0 0 0]x0 + [0] [1 0 1] [0] orientation: s#(s(s(p(x1)))) = [1 1 1]x1 + [2] >= [1 0 1]x1 + [1] = s#(s(p(s(x1)))) [1 1 1] [1] [1] s(log(x1)) = [0 0 0]x1 + [0] >= [0] = s(half(log(s(x1)))) [0 0 0] [0] [0] [1] [1] s(s(half(x1))) = [0] >= [0] = s(s(p(half(s(x1))))) [1] [1] [1] [0] s(s(s(s(half(half(x1)))))) = [0] >= [0] = half(half(s(s(x1)))) [3] [0] [0 0 0] [1] [0 0 0] [1] s(s(s(p(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = s(s(p(s(x1)))) [1 1 1] [2] [1 1 1] [2] [0 0 0] [2] [0 0 0] [1] s(p(s(s(x1)))) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = s(s(x1)) [1 1 1] [1] [1 1 1] [1] problem: DPs: TRS: s(log(x1)) -> s(half(log(s(x1)))) s(s(half(x1))) -> s(s(p(half(s(x1))))) s(s(s(s(half(half(x1)))))) -> half(half(s(s(x1)))) s(s(s(p(x1)))) -> s(s(p(s(x1)))) s(p(s(s(x1)))) -> s(s(x1)) Qed