YES Problem: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) Proof: DP Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> d#(x1) b#(b(x1)) -> c#(d(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> f#(x1) c#(c(x1)) -> d#(f(x1)) d#(d(x1)) -> f#(x1) d#(d(x1)) -> f#(f(x1)) d#(d(x1)) -> f#(f(f(x1))) d#(x1) -> b#(x1) f#(f(x1)) -> a#(x1) f#(f(x1)) -> g#(a(x1)) g#(g(x1)) -> a#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) TDG Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> d#(x1) b#(b(x1)) -> c#(d(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> f#(x1) c#(c(x1)) -> d#(f(x1)) d#(d(x1)) -> f#(x1) d#(d(x1)) -> f#(f(x1)) d#(d(x1)) -> f#(f(f(x1))) d#(x1) -> b#(x1) f#(f(x1)) -> a#(x1) f#(f(x1)) -> g#(a(x1)) g#(g(x1)) -> a#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: g#(g(x1)) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) g#(g(x1)) -> a#(x1) -> a#(a(x1)) -> c#(x1) f#(f(x1)) -> g#(a(x1)) -> g#(g(x1)) -> a#(x1) f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> c#(x1) d#(d(x1)) -> f#(f(f(x1))) -> f#(f(x1)) -> g#(a(x1)) d#(d(x1)) -> f#(f(f(x1))) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(f(x1)) -> f#(f(x1)) -> g#(a(x1)) d#(d(x1)) -> f#(f(x1)) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(x1) -> f#(f(x1)) -> g#(a(x1)) d#(d(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) d#(x1) -> b#(x1) -> b#(x1) -> a#(x1) d#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1)) d#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1) b#(b(x1)) -> d#(x1) -> d#(x1) -> b#(x1) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(f(f(x1))) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(f(x1)) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(f(x1)) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> f#(x1) b#(x1) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) -> a#(a(x1)) -> c#(x1) c#(c(x1)) -> f#(x1) -> f#(f(x1)) -> g#(a(x1)) c#(c(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) c#(c(x1)) -> d#(f(x1)) -> d#(x1) -> b#(x1) c#(c(x1)) -> d#(f(x1)) -> d#(d(x1)) -> f#(f(f(x1))) c#(c(x1)) -> d#(f(x1)) -> d#(d(x1)) -> f#(f(x1)) c#(c(x1)) -> d#(f(x1)) -> d#(d(x1)) -> f#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> d#(f(x1)) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> f#(x1) CDG Processor: DPs: a#(a(x1)) -> c#(x1) a#(a(x1)) -> b#(c(x1)) b#(b(x1)) -> d#(x1) b#(b(x1)) -> c#(d(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> f#(x1) c#(c(x1)) -> d#(f(x1)) d#(d(x1)) -> f#(x1) d#(d(x1)) -> f#(f(x1)) d#(d(x1)) -> f#(f(f(x1))) d#(x1) -> b#(x1) f#(f(x1)) -> a#(x1) f#(f(x1)) -> g#(a(x1)) g#(g(x1)) -> a#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: g#(g(x1)) -> a#(x1) -> a#(a(x1)) -> c#(x1) g#(g(x1)) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> c#(x1) f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) d#(d(x1)) -> f#(f(f(x1))) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(f(f(x1))) -> f#(f(x1)) -> g#(a(x1)) d#(d(x1)) -> f#(f(x1)) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(f(x1)) -> f#(f(x1)) -> g#(a(x1)) d#(d(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(x1) -> f#(f(x1)) -> g#(a(x1)) d#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1) d#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1)) d#(x1) -> b#(x1) -> b#(x1) -> a#(x1) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(f(x1)) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(f(f(x1))) b#(b(x1)) -> d#(x1) -> d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> f#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(f(x1)) b#(x1) -> a#(x1) -> a#(a(x1)) -> c#(x1) b#(x1) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) c#(c(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) c#(c(x1)) -> f#(x1) -> f#(f(x1)) -> g#(a(x1)) c#(c(x1)) -> d#(f(x1)) -> d#(x1) -> b#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(x1) -> a#(x1) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> f#(x1) a#(a(x1)) -> c#(x1) -> c#(c(x1)) -> d#(f(x1)) SCC Processor: #sccs: 1 #rules: 12 #arcs: 29/196 DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) a#(a(x1)) -> c#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) f#(f(x1)) -> a#(x1) b#(b(x1)) -> d#(x1) d#(d(x1)) -> f#(f(f(x1))) d#(d(x1)) -> f#(f(x1)) d#(d(x1)) -> f#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) Matrix Interpretation Processor: dim=4 interpretation: [f#](x0) = [0 0 1 0]x0 + [1], [d#](x0) = [0 0 1 0]x0 + [1], [b#](x0) = [0 0 1 0]x0 + [1], [c#](x0) = [0 0 1 1]x0, [a#](x0) = [0 0 1 0]x0 + [1], [0 1 0 0] [1] [0 0 0 1] [0] [g](x0) = [0 1 1 0]x0 + [0] [1 0 0 0] [0], [0 0 0 0] [1] [1 0 0 0] [0] [f](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [0], [0 0 0 1] [0] [0 0 0 1] [0] [d](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 0] [0] [b](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 0] [0] [c](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 0] [0] [a](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [1] orientation: a#(a(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = b#(c(x1)) b#(x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = a#(x1) a#(a(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 = c#(x1) c#(c(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = d#(f(x1)) d#(x1) = [0 0 1 0]x1 + [1] >= [0 0 1 0]x1 + [1] = b#(x1) b#(b(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = c#(d(x1)) c#(c(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [1] = f#(x1) f#(f(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [1] = a#(x1) b#(b(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [1] = d#(x1) d#(d(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = f#(f(f(x1))) d#(d(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = f#(f(x1)) d#(d(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 0]x1 + [1] = f#(x1) [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] a(a(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = b(c(x1)) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] b(b(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [1] = c(d(x1)) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] b(x1) = [0 0 1 1]x1 + [0] >= [0 0 1 1]x1 + [0] = a(x1) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] c(c(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [0] = d(f(x1)) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] d(d(x1)) = [0 0 1 1]x1 + [1] >= [0 0 1 1]x1 + [0] = f(f(f(x1))) [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 1] [0] [0 0 0 0] [0] [0 0 0 1] [0] [0 0 0 0] [0] d(x1) = [0 0 1 1]x1 + [0] >= [0 0 1 1]x1 + [0] = b(x1) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] f(f(x1)) = [0 0 1 1]x1 + [0] >= [0 0 1 1]x1 + [0] = g(a(x1)) [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 1] [1] [0 0 0 0] [0] [1 0 0 0] [0] [0 0 0 0] [0] g(g(x1)) = [0 1 1 1]x1 + [0] >= [0 0 1 1]x1 + [0] = a(x1) [0 1 0 0] [1] [0 0 0 0] [1] problem: DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) f#(f(x1)) -> a#(x1) b#(b(x1)) -> d#(x1) d#(d(x1)) -> f#(f(f(x1))) d#(d(x1)) -> f#(f(x1)) d#(d(x1)) -> f#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) EDG Processor: DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) f#(f(x1)) -> a#(x1) b#(b(x1)) -> d#(x1) d#(d(x1)) -> f#(f(f(x1))) d#(d(x1)) -> f#(f(x1)) d#(d(x1)) -> f#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) d#(d(x1)) -> f#(f(f(x1))) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(f(x1)) -> f#(f(x1)) -> a#(x1) d#(d(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) d#(x1) -> b#(x1) -> b#(x1) -> a#(x1) d#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1)) d#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1) b#(b(x1)) -> d#(x1) -> d#(x1) -> b#(x1) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(f(f(x1))) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(f(x1)) b#(b(x1)) -> d#(x1) -> d#(d(x1)) -> f#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(f(x1)) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> f#(x1) b#(x1) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) c#(c(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) c#(c(x1)) -> d#(f(x1)) -> d#(x1) -> b#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1) Matrix Interpretation Processor: dim=4 interpretation: [f#](x0) = [0], [d#](x0) = [0 1 1 0]x0, [b#](x0) = [0 0 1 0]x0, [c#](x0) = [1 0 0 0]x0, [a#](x0) = [0], [0 0 0 0] [1] [1 0 0 0] [0] [g](x0) = [0 0 0 1]x0 + [0] [0 1 0 0] [0], [0 0 0 0] [1] [0 0 0 0] [0] [f](x0) = [0 0 0 0]x0 + [0] [1 0 0 0] [0], [0 1 0 0] [0] [0 0 0 0] [1] [d](x0) = [0 1 1 0]x0 + [0] [0 1 0 0] [0], [0 0 0 0] [0] [0 0 0 0] [1] [b](x0) = [0 1 1 0]x0 + [0] [0 0 0 0] [0], [0] [1] [c](x0) = [0] [0], [0 0 0 0] [0] [0 0 0 0] [1] [a](x0) = [0 1 0 0]x0 + [0] [0 0 0 0] [0] orientation: a#(a(x1)) = [0] >= [0] = b#(c(x1)) b#(x1) = [0 0 1 0]x1 >= [0] = a#(x1) c#(c(x1)) = [0] >= [0] = d#(f(x1)) d#(x1) = [0 1 1 0]x1 >= [0 0 1 0]x1 = b#(x1) b#(b(x1)) = [0 1 1 0]x1 >= [0 1 0 0]x1 = c#(d(x1)) c#(c(x1)) = [0] >= [0] = f#(x1) f#(f(x1)) = [0] >= [0] = a#(x1) b#(b(x1)) = [0 1 1 0]x1 >= [0 1 1 0]x1 = d#(x1) d#(d(x1)) = [0 1 1 0]x1 + [1] >= [0] = f#(f(f(x1))) d#(d(x1)) = [0 1 1 0]x1 + [1] >= [0] = f#(f(x1)) d#(d(x1)) = [0 1 1 0]x1 + [1] >= [0] = f#(x1) [0] [0] [1] [1] a(a(x1)) = [1] >= [1] = b(c(x1)) [0] [0] [0 0 0 0] [0] [0] [0 0 0 0] [1] [1] b(b(x1)) = [0 1 1 0]x1 + [1] >= [0] = c(d(x1)) [0 0 0 0] [0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [1] b(x1) = [0 1 1 0]x1 + [0] >= [0 1 0 0]x1 + [0] = a(x1) [0 0 0 0] [0] [0 0 0 0] [0] [0] [0] [1] [1] c(c(x1)) = [0] >= [0] = d(f(x1)) [0] [0] [0 0 0 0] [1] [1] [0 0 0 0] [1] [0] d(d(x1)) = [0 1 1 0]x1 + [1] >= [0] = f(f(f(x1))) [0 0 0 0] [1] [1] [0 1 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [1] d(x1) = [0 1 1 0]x1 + [0] >= [0 1 1 0]x1 + [0] = b(x1) [0 1 0 0] [0] [0 0 0 0] [0] [1] [1] [0] [0] f(f(x1)) = [0] >= [0] = g(a(x1)) [1] [1] [0 0 0 0] [1] [0 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [1] g(g(x1)) = [0 1 0 0]x1 + [0] >= [0 1 0 0]x1 + [0] = a(x1) [1 0 0 0] [0] [0 0 0 0] [0] problem: DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) f#(f(x1)) -> a#(x1) b#(b(x1)) -> d#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) EDG Processor: DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) f#(f(x1)) -> a#(x1) b#(b(x1)) -> d#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: f#(f(x1)) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) d#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1) d#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1)) d#(x1) -> b#(x1) -> b#(x1) -> a#(x1) b#(b(x1)) -> d#(x1) -> d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> f#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(f(x1)) b#(x1) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) c#(c(x1)) -> f#(x1) -> f#(f(x1)) -> a#(x1) c#(c(x1)) -> d#(f(x1)) -> d#(x1) -> b#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(x1) -> a#(x1) Matrix Interpretation Processor: dim=4 interpretation: [f#](x0) = [1 0 0 0]x0, [d#](x0) = [0 0 1 1]x0, [b#](x0) = [0 0 1 0]x0, [c#](x0) = [1 0 0 0]x0, [a#](x0) = [0], [0 0 0 0] [1] [0 1 0 1] [0] [g](x0) = [0 1 0 0]x0 + [0] [1 0 0 0] [0], [0 0 0 0] [1] [1 0 0 0] [0] [f](x0) = [0 0 0 0]x0 + [0] [0 0 0 0] [0], [0 0 1 1] [0] [0 0 0 1] [0] [d](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [1], [0 0 1 0] [0] [0 0 0 0] [0] [b](x0) = [0 0 1 1]x0 + [0] [0 0 0 0] [1], [1 0 0 0] [0] [0 0 0 0] [0] [c](x0) = [0 0 0 0]x0 + [0] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 0] [0] [a](x0) = [0 0 0 1]x0 + [0] [0 0 0 0] [1] orientation: a#(a(x1)) = [0] >= [0] = b#(c(x1)) b#(x1) = [0 0 1 0]x1 >= [0] = a#(x1) c#(c(x1)) = [1 0 0 0]x1 >= [0] = d#(f(x1)) d#(x1) = [0 0 1 1]x1 >= [0 0 1 0]x1 = b#(x1) b#(b(x1)) = [0 0 1 1]x1 >= [0 0 1 1]x1 = c#(d(x1)) c#(c(x1)) = [1 0 0 0]x1 >= [1 0 0 0]x1 = f#(x1) f#(f(x1)) = [1] >= [0] = a#(x1) b#(b(x1)) = [0 0 1 1]x1 >= [0 0 1 1]x1 = d#(x1) [0] [0] [0] [0] a(a(x1)) = [1] >= [1] = b(c(x1)) [1] [1] [0 0 1 1] [0] [0 0 1 1] [0] [0 0 0 0] [0] [0 0 0 0] [0] b(b(x1)) = [0 0 1 1]x1 + [1] >= [0 0 0 0]x1 + [0] = c(d(x1)) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 1 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [0] b(x1) = [0 0 1 1]x1 + [0] >= [0 0 0 1]x1 + [0] = a(x1) [0 0 0 0] [1] [0 0 0 0] [1] [1 0 0 0] [0] [0] [0 0 0 0] [0] [0] c(c(x1)) = [0 0 0 0]x1 + [0] >= [0] = d(f(x1)) [0 0 0 0] [1] [1] [0 0 1 1] [1] [1] [0 0 0 0] [1] [1] d(d(x1)) = [0 0 1 1]x1 + [1] >= [0] = f(f(f(x1))) [0 0 0 0] [1] [0] [0 0 1 1] [0] [0 0 1 0] [0] [0 0 0 1] [0] [0 0 0 0] [0] d(x1) = [0 0 1 1]x1 + [0] >= [0 0 1 1]x1 + [0] = b(x1) [0 0 0 0] [1] [0 0 0 0] [1] [1] [1] [1] [1] f(f(x1)) = [0] >= [0] = g(a(x1)) [0] [0] [0 0 0 0] [1] [0 0 0 0] [0] [1 1 0 1] [0] [0 0 0 0] [0] g(g(x1)) = [0 1 0 1]x1 + [0] >= [0 0 0 1]x1 + [0] = a(x1) [0 0 0 0] [1] [0 0 0 0] [1] problem: DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) b#(b(x1)) -> d#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) EDG Processor: DPs: a#(a(x1)) -> b#(c(x1)) b#(x1) -> a#(x1) c#(c(x1)) -> d#(f(x1)) d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> f#(x1) b#(b(x1)) -> d#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: d#(x1) -> b#(x1) -> b#(x1) -> a#(x1) d#(x1) -> b#(x1) -> b#(b(x1)) -> c#(d(x1)) d#(x1) -> b#(x1) -> b#(b(x1)) -> d#(x1) b#(b(x1)) -> d#(x1) -> d#(x1) -> b#(x1) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> d#(f(x1)) b#(b(x1)) -> c#(d(x1)) -> c#(c(x1)) -> f#(x1) b#(x1) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) c#(c(x1)) -> d#(f(x1)) -> d#(x1) -> b#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> c#(d(x1)) a#(a(x1)) -> b#(c(x1)) -> b#(b(x1)) -> d#(x1) SCC Processor: #sccs: 1 #rules: 6 #arcs: 11/49 DPs: d#(x1) -> b#(x1) b#(b(x1)) -> d#(x1) b#(b(x1)) -> c#(d(x1)) c#(c(x1)) -> d#(f(x1)) b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) Matrix Interpretation Processor: dim=3 interpretation: [d#](x0) = [0 0 1]x0, [b#](x0) = [0 0 1]x0, [c#](x0) = [0], [a#](x0) = [0 0 1]x0, [0 0 1] [0] [g](x0) = [0 0 0]x0 + [1] [1 1 0] [0], [0 1 0] [0] [f](x0) = [0 0 1]x0 + [1] [0 0 0] [0], [0 0 1] [0] [d](x0) = [0 0 1]x0 + [0] [0 0 1] [1], [0 0 0] [0] [b](x0) = [0 0 0]x0 + [0] [0 0 1] [1], [0] [c](x0) = [0] [1], [0 0 0] [0] [a](x0) = [0 0 0]x0 + [0] [0 0 1] [1] orientation: d#(x1) = [0 0 1]x1 >= [0 0 1]x1 = b#(x1) b#(b(x1)) = [0 0 1]x1 + [1] >= [0 0 1]x1 = d#(x1) b#(b(x1)) = [0 0 1]x1 + [1] >= [0] = c#(d(x1)) c#(c(x1)) = [0] >= [0] = d#(f(x1)) b#(x1) = [0 0 1]x1 >= [0 0 1]x1 = a#(x1) a#(a(x1)) = [0 0 1]x1 + [1] >= [1] = b#(c(x1)) [0 0 0] [0] [0] a(a(x1)) = [0 0 0]x1 + [0] >= [0] = b(c(x1)) [0 0 1] [2] [2] [0 0 0] [0] [0] b(b(x1)) = [0 0 0]x1 + [0] >= [0] = c(d(x1)) [0 0 1] [2] [1] [0 0 0] [0] [0 0 0] [0] b(x1) = [0 0 0]x1 + [0] >= [0 0 0]x1 + [0] = a(x1) [0 0 1] [1] [0 0 1] [1] [0] [0] c(c(x1)) = [0] >= [0] = d(f(x1)) [1] [1] [0 0 1] [1] [1] d(d(x1)) = [0 0 1]x1 + [1] >= [1] = f(f(f(x1))) [0 0 1] [2] [0] [0 0 1] [0] [0 0 0] [0] d(x1) = [0 0 1]x1 + [0] >= [0 0 0]x1 + [0] = b(x1) [0 0 1] [1] [0 0 1] [1] [0 0 1] [1] [0 0 1] [1] f(f(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [1] = g(a(x1)) [0 0 0] [0] [0 0 0] [0] [1 1 0] [0] [0 0 0] [0] g(g(x1)) = [0 0 0]x1 + [1] >= [0 0 0]x1 + [0] = a(x1) [0 0 1] [1] [0 0 1] [1] problem: DPs: d#(x1) -> b#(x1) c#(c(x1)) -> d#(f(x1)) b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) EDG Processor: DPs: d#(x1) -> b#(x1) c#(c(x1)) -> d#(f(x1)) b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: d#(x1) -> b#(x1) -> b#(x1) -> a#(x1) b#(x1) -> a#(x1) -> a#(a(x1)) -> b#(c(x1)) c#(c(x1)) -> d#(f(x1)) -> d#(x1) -> b#(x1) a#(a(x1)) -> b#(c(x1)) -> b#(x1) -> a#(x1) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/16 DPs: b#(x1) -> a#(x1) a#(a(x1)) -> b#(c(x1)) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) Matrix Interpretation Processor: dim=4 interpretation: [b#](x0) = [0 1 1 0]x0, [a#](x0) = [0 1 1 0]x0, [0 0 0 0] [1] [0 1 0 1] [0] [g](x0) = [1 0 0 0]x0 + [0] [1 0 0 0] [0], [0 0 0 1] [1] [1 0 0 0] [0] [f](x0) = [0 0 0 0]x0 + [0] [0 0 0 0] [0], [0 0 1 0] [0] [0 0 0 1] [0] [d](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 1] [0] [b](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 0] [0] [c](x0) = [0 0 0 1]x0 + [0] [0 0 0 0] [1], [0 0 0 0] [0] [0 0 0 1] [0] [a](x0) = [0 0 0 0]x0 + [1] [0 0 0 0] [1] orientation: b#(x1) = [0 1 1 0]x1 >= [0 1 1 0]x1 = a#(x1) a#(a(x1)) = [0 0 0 1]x1 + [1] >= [0 0 0 1]x1 = b#(c(x1)) [0] [0] [1] [1] a(a(x1)) = [1] >= [1] = b(c(x1)) [1] [1] [0] [0] [1] [0] b(b(x1)) = [1] >= [1] = c(d(x1)) [1] [1] [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 1] [0] [0 0 0 1] [0] b(x1) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = a(x1) [0 0 0 0] [1] [0 0 0 0] [1] [0] [0] [0] [0] c(c(x1)) = [1] >= [1] = d(f(x1)) [1] [1] [1] [1] [1] [1] d(d(x1)) = [1] >= [0] = f(f(f(x1))) [1] [0] [0 0 1 0] [0] [0 0 0 0] [0] [0 0 0 1] [0] [0 0 0 1] [0] d(x1) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = b(x1) [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 0] [1] [0 0 0 1] [1] [0 0 0 1] [1] f(f(x1)) = [0 0 0 0]x1 + [0] >= [0 0 0 0]x1 + [0] = g(a(x1)) [0 0 0 0] [0] [0 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [0] [1 1 0 1] [0] [0 0 0 1] [0] g(g(x1)) = [0 0 0 0]x1 + [1] >= [0 0 0 0]x1 + [1] = a(x1) [0 0 0 0] [1] [0 0 0 0] [1] problem: DPs: b#(x1) -> a#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) EDG Processor: DPs: b#(x1) -> a#(x1) TRS: a(a(x1)) -> b(c(x1)) b(b(x1)) -> c(d(x1)) b(x1) -> a(x1) c(c(x1)) -> d(f(x1)) d(d(x1)) -> f(f(f(x1))) d(x1) -> b(x1) f(f(x1)) -> g(a(x1)) g(g(x1)) -> a(x1) graph: Qed