YES Problem: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) Proof: DP Processor: DPs: c#(c(c(b(x)))) -> c#(x) c#(c(c(b(x)))) -> b#(c(x)) c#(c(c(b(x)))) -> a#(1(),b(c(x))) b#(c(b(c(x)))) -> a#(1(),x) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) a#(0(),x) -> c#(x) a#(0(),x) -> c#(c(x)) a#(1(),x) -> b#(x) a#(1(),x) -> c#(b(x)) TRS: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) TDG Processor: DPs: c#(c(c(b(x)))) -> c#(x) c#(c(c(b(x)))) -> b#(c(x)) c#(c(c(b(x)))) -> a#(1(),b(c(x))) b#(c(b(c(x)))) -> a#(1(),x) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) a#(0(),x) -> c#(x) a#(0(),x) -> c#(c(x)) a#(1(),x) -> b#(x) a#(1(),x) -> c#(b(x)) TRS: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) graph: a#(0(),x) -> c#(c(x)) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) a#(0(),x) -> c#(c(x)) -> c#(c(c(b(x)))) -> b#(c(x)) a#(0(),x) -> c#(c(x)) -> c#(c(c(b(x)))) -> c#(x) a#(0(),x) -> c#(x) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) a#(0(),x) -> c#(x) -> c#(c(c(b(x)))) -> b#(c(x)) a#(0(),x) -> c#(x) -> c#(c(c(b(x)))) -> c#(x) a#(1(),x) -> b#(x) -> b#(c(b(c(x)))) -> a#(0(),a(1(),x)) a#(1(),x) -> b#(x) -> b#(c(b(c(x)))) -> a#(1(),x) a#(1(),x) -> c#(b(x)) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) a#(1(),x) -> c#(b(x)) -> c#(c(c(b(x)))) -> b#(c(x)) a#(1(),x) -> c#(b(x)) -> c#(c(c(b(x)))) -> c#(x) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) -> a#(1(),x) -> c#(b(x)) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) -> a#(1(),x) -> b#(x) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) -> a#(0(),x) -> c#(c(x)) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) -> a#(0(),x) -> c#(x) b#(c(b(c(x)))) -> a#(1(),x) -> a#(1(),x) -> c#(b(x)) b#(c(b(c(x)))) -> a#(1(),x) -> a#(1(),x) -> b#(x) b#(c(b(c(x)))) -> a#(1(),x) -> a#(0(),x) -> c#(c(x)) b#(c(b(c(x)))) -> a#(1(),x) -> a#(0(),x) -> c#(x) c#(c(c(b(x)))) -> a#(1(),b(c(x))) -> a#(1(),x) -> c#(b(x)) c#(c(c(b(x)))) -> a#(1(),b(c(x))) -> a#(1(),x) -> b#(x) c#(c(c(b(x)))) -> a#(1(),b(c(x))) -> a#(0(),x) -> c#(c(x)) c#(c(c(b(x)))) -> a#(1(),b(c(x))) -> a#(0(),x) -> c#(x) c#(c(c(b(x)))) -> b#(c(x)) -> b#(c(b(c(x)))) -> a#(0(),a(1(),x)) c#(c(c(b(x)))) -> b#(c(x)) -> b#(c(b(c(x)))) -> a#(1(),x) c#(c(c(b(x)))) -> c#(x) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) c#(c(c(b(x)))) -> c#(x) -> c#(c(c(b(x)))) -> b#(c(x)) c#(c(c(b(x)))) -> c#(x) -> c#(c(c(b(x)))) -> c#(x) EDG Processor: DPs: c#(c(c(b(x)))) -> c#(x) c#(c(c(b(x)))) -> b#(c(x)) c#(c(c(b(x)))) -> a#(1(),b(c(x))) b#(c(b(c(x)))) -> a#(1(),x) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) a#(0(),x) -> c#(x) a#(0(),x) -> c#(c(x)) a#(1(),x) -> b#(x) a#(1(),x) -> c#(b(x)) TRS: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) graph: a#(0(),x) -> c#(c(x)) -> c#(c(c(b(x)))) -> c#(x) a#(0(),x) -> c#(c(x)) -> c#(c(c(b(x)))) -> b#(c(x)) a#(0(),x) -> c#(c(x)) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) a#(0(),x) -> c#(x) -> c#(c(c(b(x)))) -> c#(x) a#(0(),x) -> c#(x) -> c#(c(c(b(x)))) -> b#(c(x)) a#(0(),x) -> c#(x) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) a#(1(),x) -> b#(x) -> b#(c(b(c(x)))) -> a#(1(),x) a#(1(),x) -> b#(x) -> b#(c(b(c(x)))) -> a#(0(),a(1(),x)) a#(1(),x) -> c#(b(x)) -> c#(c(c(b(x)))) -> c#(x) a#(1(),x) -> c#(b(x)) -> c#(c(c(b(x)))) -> b#(c(x)) a#(1(),x) -> c#(b(x)) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) -> a#(0(),x) -> c#(x) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) -> a#(0(),x) -> c#(c(x)) b#(c(b(c(x)))) -> a#(1(),x) -> a#(1(),x) -> b#(x) b#(c(b(c(x)))) -> a#(1(),x) -> a#(1(),x) -> c#(b(x)) c#(c(c(b(x)))) -> a#(1(),b(c(x))) -> a#(1(),x) -> b#(x) c#(c(c(b(x)))) -> a#(1(),b(c(x))) -> a#(1(),x) -> c#(b(x)) c#(c(c(b(x)))) -> b#(c(x)) -> b#(c(b(c(x)))) -> a#(1(),x) c#(c(c(b(x)))) -> b#(c(x)) -> b#(c(b(c(x)))) -> a#(0(),a(1(),x)) c#(c(c(b(x)))) -> c#(x) -> c#(c(c(b(x)))) -> c#(x) c#(c(c(b(x)))) -> c#(x) -> c#(c(c(b(x)))) -> b#(c(x)) c#(c(c(b(x)))) -> c#(x) -> c#(c(c(b(x)))) -> a#(1(),b(c(x))) Arctic Interpretation Processor: dimension: 1 interpretation: [a#](x0, x1) = 1x1, [b#](x0) = x0, [c#](x0) = x0, [0] = 3, [a](x0, x1) = 2x1, [1] = 4, [c](x0) = 1x0, [b](x0) = 1x0 orientation: c#(c(c(b(x)))) = 3x >= x = c#(x) c#(c(c(b(x)))) = 3x >= 1x = b#(c(x)) c#(c(c(b(x)))) = 3x >= 3x = a#(1(),b(c(x))) b#(c(b(c(x)))) = 3x >= 1x = a#(1(),x) b#(c(b(c(x)))) = 3x >= 3x = a#(0(),a(1(),x)) a#(0(),x) = 1x >= x = c#(x) a#(0(),x) = 1x >= 1x = c#(c(x)) a#(1(),x) = 1x >= x = b#(x) a#(1(),x) = 1x >= 1x = c#(b(x)) c(c(c(b(x)))) = 4x >= 4x = a(1(),b(c(x))) b(c(b(c(x)))) = 4x >= 4x = a(0(),a(1(),x)) a(0(),x) = 2x >= 2x = c(c(x)) a(1(),x) = 2x >= 2x = c(b(x)) problem: DPs: c#(c(c(b(x)))) -> a#(1(),b(c(x))) b#(c(b(c(x)))) -> a#(0(),a(1(),x)) a#(0(),x) -> c#(c(x)) a#(1(),x) -> c#(b(x)) TRS: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) SCC Processor: #sccs: 1 #rules: 2 #arcs: 22/16 DPs: c#(c(c(b(x)))) -> a#(1(),b(c(x))) a#(1(),x) -> c#(b(x)) TRS: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) Matrix Interpretation Processor: dim=3 interpretation: [a#](x0, x1) = [1 0 0]x0 + [0 1 1]x1, [c#](x0) = [0 0 1]x0, [0] [0] = [1] [0], [0 1 0] [0 1 1] [0] [a](x0, x1) = [0 0 0]x0 + [0 0 1]x1 + [0] [0 1 0] [1 1 1] [1], [1] [1] = [0] [0], [0 0 1] [0] [c](x0) = [1 0 0]x0 + [0] [0 1 1] [1], [0 0 1] [b](x0) = [1 0 0]x0 [0 1 1] orientation: c#(c(c(b(x)))) = [1 1 2]x + [2] >= [1 1 2]x + [2] = a#(1(),b(c(x))) a#(1(),x) = [0 1 1]x + [1] >= [0 1 1]x = c#(b(x)) [1 1 2] [2] [1 1 2] [1] c(c(c(b(x)))) = [1 1 1]x + [1] >= [1 1 1]x + [1] = a(1(),b(c(x))) [1 2 3] [3] [1 2 3] [3] [1 1 2] [2] [1 1 2] [2] b(c(b(c(x)))) = [1 1 1]x + [1] >= [1 1 1]x + [1] = a(0(),a(1(),x)) [1 2 3] [3] [1 2 3] [3] [0 1 1] [1] [0 1 1] [1] a(0(),x) = [0 0 1]x + [0] >= [0 0 1]x + [0] = c(c(x)) [1 1 1] [2] [1 1 1] [2] [0 1 1] [0] [0 1 1] [0] a(1(),x) = [0 0 1]x + [0] >= [0 0 1]x + [0] = c(b(x)) [1 1 1] [1] [1 1 1] [1] problem: DPs: c#(c(c(b(x)))) -> a#(1(),b(c(x))) TRS: c(c(c(b(x)))) -> a(1(),b(c(x))) b(c(b(c(x)))) -> a(0(),a(1(),x)) a(0(),x) -> c(c(x)) a(1(),x) -> c(b(x)) SCC Processor: #sccs: 0 #rules: 0 #arcs: 2/1