YES Problem: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Proof: DP Processor: DPs: a#(x1) -> g#(d(x1)) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(d(c(x1))) b#(b(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) b#(b(x1)) -> a#(g(g(x1))) c#(d(x1)) -> g#(x1) c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) g#(g(g(x1))) -> b#(b(x1)) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) TDG Processor: DPs: a#(x1) -> g#(d(x1)) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(d(c(x1))) b#(b(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) b#(b(x1)) -> a#(g(g(x1))) c#(d(x1)) -> g#(x1) c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) g#(g(g(x1))) -> b#(b(x1)) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) graph: c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> a#(g(g(x1))) -> a#(x1) -> g#(d(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(g(g(x1))) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> a#(g(g(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(x1) a#(x1) -> g#(d(x1)) -> g#(g(g(x1))) -> b#(b(x1)) a#(x1) -> g#(d(x1)) -> g#(g(g(x1))) -> b#(x1) EDG Processor: DPs: a#(x1) -> g#(d(x1)) b#(b(b(x1))) -> c#(x1) b#(b(b(x1))) -> c#(d(c(x1))) b#(b(x1)) -> g#(x1) b#(b(x1)) -> g#(g(x1)) b#(b(x1)) -> a#(g(g(x1))) c#(d(x1)) -> g#(x1) c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) g#(g(g(x1))) -> b#(b(x1)) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) graph: c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) c#(d(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) c#(d(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(d(c(x1))) -> c#(d(x1)) -> g#(g(x1)) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(x1) -> c#(d(x1)) -> g#(g(x1)) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(g(x1)) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(x1) -> g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> a#(g(g(x1))) -> a#(x1) -> g#(d(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(x1) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(b(x1)) -> b#(b(x1)) -> a#(g(g(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(b(x1))) -> c#(d(c(x1))) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(x1) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) -> b#(b(x1)) -> a#(g(g(x1))) SCC Processor: #sccs: 1 #rules: 8 #arcs: 23/100 DPs: c#(d(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(b(x1)) b#(b(x1)) -> g#(g(x1)) g#(g(g(x1))) -> b#(x1) b#(b(x1)) -> g#(x1) b#(b(b(x1))) -> c#(d(c(x1))) c#(d(x1)) -> g#(x1) b#(b(b(x1))) -> c#(x1) TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Matrix Interpretation Processor: dim=1 interpretation: [c#](x0) = 4x0 + 17, [b#](x0) = 4x0 + 4, [g#](x0) = 4x0, [c](x0) = x0 + 8, [b](x0) = x0 + 6, [g](x0) = x0 + 4, [d](x0) = x0, [a](x0) = x0 + 4 orientation: c#(d(x1)) = 4x1 + 17 >= 4x1 + 16 = g#(g(x1)) g#(g(g(x1))) = 4x1 + 32 >= 4x1 + 28 = b#(b(x1)) b#(b(x1)) = 4x1 + 28 >= 4x1 + 16 = g#(g(x1)) g#(g(g(x1))) = 4x1 + 32 >= 4x1 + 4 = b#(x1) b#(b(x1)) = 4x1 + 28 >= 4x1 = g#(x1) b#(b(b(x1))) = 4x1 + 52 >= 4x1 + 49 = c#(d(c(x1))) c#(d(x1)) = 4x1 + 17 >= 4x1 = g#(x1) b#(b(b(x1))) = 4x1 + 52 >= 4x1 + 17 = c#(x1) a(x1) = x1 + 4 >= x1 + 4 = g(d(x1)) b(b(b(x1))) = x1 + 18 >= x1 + 16 = c(d(c(x1))) b(b(x1)) = x1 + 12 >= x1 + 12 = a(g(g(x1))) c(d(x1)) = x1 + 8 >= x1 + 8 = g(g(x1)) g(g(g(x1))) = x1 + 12 >= x1 + 12 = b(b(x1)) problem: DPs: TRS: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Qed