MAYBE Problem: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(A()) -> a__A() mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(h(X1,X2)) -> a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) -> a__g(mark(X1),mark(X2),mark(X3)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__A() -> A() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) a__g(X1,X2,X3) -> g(X1,X2,X3) Proof: Matrix Interpretation Processor: dim=1 interpretation: [g](x0, x1, x2) = 2x0 + 3x1 + 4x2 + 1, [h](x0, x1) = 6x0 + 4x1 + 1, [f](x0) = 4x0, [z](x0, x1) = x0 + x1, [k] = 0, [c] = 0, [b] = 0, [a] = 0, [A] = 1, [a__z](x0, x1) = x0 + 2x1, [d] = 0, [a__g](x0, x1, x2) = 2x0 + 3x1 + 4x2 + 1, [mark](x0) = 2x0, [a__h](x0, x1) = 6x0 + 4x1 + 1, [a__f](x0) = 4x0, [a__A] = 1, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 0, [a__b] = 0, [a__c] = 0, [a__a] = 0 orientation: a__a() = 0 >= 0 = a__c() a__b() = 0 >= 0 = a__c() a__c() = 0 >= 0 = e() a__k() = 0 >= 0 = l() a__d() = 0 >= 0 = m() a__a() = 0 >= 0 = a__d() a__b() = 0 >= 0 = a__d() a__c() = 0 >= 0 = l() a__k() = 0 >= 0 = m() a__A() = 1 >= 1 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = 10X + 1 >= 10X + 1 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 7X + 1 >= 1 = a__A() a__f(X) = 4X >= 4X = a__z(mark(X),X) a__z(e(),X) = 2X >= 2X = mark(X) mark(A()) = 2 >= 1 = a__A() mark(a()) = 0 >= 0 = a__a() mark(b()) = 0 >= 0 = a__b() mark(c()) = 0 >= 0 = a__c() mark(d()) = 0 >= 0 = a__d() mark(k()) = 0 >= 0 = a__k() mark(z(X1,X2)) = 2X1 + 2X2 >= 2X1 + 2X2 = a__z(mark(X1),X2) mark(f(X)) = 8X >= 8X = a__f(mark(X)) mark(h(X1,X2)) = 12X1 + 8X2 + 2 >= 12X1 + 8X2 + 1 = a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) = 4X1 + 6X2 + 8X3 + 2 >= 4X1 + 6X2 + 8X3 + 1 = a__g(mark(X1),mark(X2),mark(X3)) mark(e()) = 0 >= 0 = e() mark(l()) = 0 >= 0 = l() mark(m()) = 0 >= 0 = m() a__A() = 1 >= 1 = A() a__a() = 0 >= 0 = a() a__b() = 0 >= 0 = b() a__c() = 0 >= 0 = c() a__d() = 0 >= 0 = d() a__k() = 0 >= 0 = k() a__z(X1,X2) = X1 + 2X2 >= X1 + X2 = z(X1,X2) a__f(X) = 4X >= 4X = f(X) a__h(X1,X2) = 6X1 + 4X2 + 1 >= 6X1 + 4X2 + 1 = h(X1,X2) a__g(X1,X2,X3) = 2X1 + 3X2 + 4X3 + 1 >= 2X1 + 3X2 + 4X3 + 1 = g(X1,X2,X3) problem: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__A() -> A() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) a__g(X1,X2,X3) -> g(X1,X2,X3) Matrix Interpretation Processor: dim=1 interpretation: [g](x0, x1, x2) = x0 + x1 + 2x2 + 1, [h](x0, x1) = 2x0 + 2x1 + 1, [f](x0) = 6x0, [z](x0, x1) = 4x0 + 2x1, [k] = 0, [c] = 0, [b] = 0, [a] = 0, [A] = 0, [a__z](x0, x1) = 4x0 + 2x1, [d] = 0, [a__g](x0, x1, x2) = 2x0 + 2x1 + 4x2 + 1, [mark](x0) = x0, [a__h](x0, x1) = 5x0 + 2x1 + 1, [a__f](x0) = 6x0, [a__A] = 1, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 0, [a__b] = 0, [a__c] = 0, [a__a] = 0 orientation: a__a() = 0 >= 0 = a__c() a__b() = 0 >= 0 = a__c() a__c() = 0 >= 0 = e() a__k() = 0 >= 0 = l() a__d() = 0 >= 0 = m() a__a() = 0 >= 0 = a__d() a__b() = 0 >= 0 = a__d() a__c() = 0 >= 0 = l() a__k() = 0 >= 0 = m() a__A() = 1 >= 1 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = 7X + 1 >= 4X + 1 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 6X + 1 >= 1 = a__A() a__f(X) = 6X >= 6X = a__z(mark(X),X) a__z(e(),X) = 2X >= X = mark(X) mark(a()) = 0 >= 0 = a__a() mark(b()) = 0 >= 0 = a__b() mark(c()) = 0 >= 0 = a__c() mark(d()) = 0 >= 0 = a__d() mark(k()) = 0 >= 0 = a__k() mark(z(X1,X2)) = 4X1 + 2X2 >= 4X1 + 2X2 = a__z(mark(X1),X2) mark(f(X)) = 6X >= 6X = a__f(mark(X)) mark(e()) = 0 >= 0 = e() mark(l()) = 0 >= 0 = l() mark(m()) = 0 >= 0 = m() a__A() = 1 >= 0 = A() a__a() = 0 >= 0 = a() a__b() = 0 >= 0 = b() a__c() = 0 >= 0 = c() a__d() = 0 >= 0 = d() a__k() = 0 >= 0 = k() a__z(X1,X2) = 4X1 + 2X2 >= 4X1 + 2X2 = z(X1,X2) a__f(X) = 6X >= 6X = f(X) a__h(X1,X2) = 5X1 + 2X2 + 1 >= 2X1 + 2X2 + 1 = h(X1,X2) a__g(X1,X2,X3) = 2X1 + 2X2 + 4X3 + 1 >= X1 + X2 + 2X3 + 1 = g(X1,X2,X3) problem: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) a__g(X1,X2,X3) -> g(X1,X2,X3) Matrix Interpretation Processor: dim=1 interpretation: [g](x0, x1, x2) = x0 + x1 + x2, [h](x0, x1) = 2x0 + x1 + 2, [f](x0) = 4x0, [z](x0, x1) = 3x0 + x1, [k] = 0, [c] = 0, [b] = 0, [a] = 0, [a__z](x0, x1) = 3x0 + x1, [d] = 0, [a__g](x0, x1, x2) = x0 + 2x1 + 4x2 + 2, [mark](x0) = x0, [a__h](x0, x1) = 2x0 + x1 + 2, [a__f](x0) = 4x0, [a__A] = 2, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 0, [a__b] = 0, [a__c] = 0, [a__a] = 0 orientation: a__a() = 0 >= 0 = a__c() a__b() = 0 >= 0 = a__c() a__c() = 0 >= 0 = e() a__k() = 0 >= 0 = l() a__d() = 0 >= 0 = m() a__a() = 0 >= 0 = a__d() a__b() = 0 >= 0 = a__d() a__c() = 0 >= 0 = l() a__k() = 0 >= 0 = m() a__A() = 2 >= 2 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = 3X + 2 >= 3X + 2 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 6X + 2 >= 2 = a__A() a__f(X) = 4X >= 4X = a__z(mark(X),X) a__z(e(),X) = X >= X = mark(X) mark(a()) = 0 >= 0 = a__a() mark(b()) = 0 >= 0 = a__b() mark(c()) = 0 >= 0 = a__c() mark(d()) = 0 >= 0 = a__d() mark(k()) = 0 >= 0 = a__k() mark(z(X1,X2)) = 3X1 + X2 >= 3X1 + X2 = a__z(mark(X1),X2) mark(f(X)) = 4X >= 4X = a__f(mark(X)) mark(e()) = 0 >= 0 = e() mark(l()) = 0 >= 0 = l() mark(m()) = 0 >= 0 = m() a__a() = 0 >= 0 = a() a__b() = 0 >= 0 = b() a__c() = 0 >= 0 = c() a__d() = 0 >= 0 = d() a__k() = 0 >= 0 = k() a__z(X1,X2) = 3X1 + X2 >= 3X1 + X2 = z(X1,X2) a__f(X) = 4X >= 4X = f(X) a__h(X1,X2) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = h(X1,X2) a__g(X1,X2,X3) = X1 + 2X2 + 4X3 + 2 >= X1 + X2 + X3 = g(X1,X2,X3) problem: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) DP Processor: DPs: a__a#() -> a__c#() a__b#() -> a__c#() a__a#() -> a__d#() a__b#() -> a__d#() a__A#() -> a__b#() a__A#() -> a__f#(a__b()) a__A#() -> a__a#() a__A#() -> a__f#(a__a()) a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) a__h#(X,X) -> a__k#() a__h#(X,X) -> a__f#(a__k()) a__h#(X,X) -> mark#(X) a__h#(X,X) -> a__g#(mark(X),mark(X),a__f(a__k())) a__g#(d(),X,X) -> a__A#() a__f#(X) -> mark#(X) a__f#(X) -> a__z#(mark(X),X) a__z#(e(),X) -> mark#(X) mark#(a()) -> a__a#() mark#(b()) -> a__b#() mark#(c()) -> a__c#() mark#(d()) -> a__d#() mark#(k()) -> a__k#() mark#(z(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) TDG Processor: DPs: a__a#() -> a__c#() a__b#() -> a__c#() a__a#() -> a__d#() a__b#() -> a__d#() a__A#() -> a__b#() a__A#() -> a__f#(a__b()) a__A#() -> a__a#() a__A#() -> a__f#(a__a()) a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) a__h#(X,X) -> a__k#() a__h#(X,X) -> a__f#(a__k()) a__h#(X,X) -> mark#(X) a__h#(X,X) -> a__g#(mark(X),mark(X),a__f(a__k())) a__g#(d(),X,X) -> a__A#() a__f#(X) -> mark#(X) a__f#(X) -> a__z#(mark(X),X) a__z#(e(),X) -> mark#(X) mark#(a()) -> a__a#() mark#(b()) -> a__b#() mark#(c()) -> a__c#() mark#(d()) -> a__d#() mark#(k()) -> a__k#() mark#(z(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) graph: a__z#(e(),X) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__z#(e(),X) -> mark#(X) -> mark#(f(X)) -> mark#(X) a__z#(e(),X) -> mark#(X) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) a__z#(e(),X) -> mark#(X) -> mark#(z(X1,X2)) -> mark#(X1) a__z#(e(),X) -> mark#(X) -> mark#(k()) -> a__k#() a__z#(e(),X) -> mark#(X) -> mark#(d()) -> a__d#() a__z#(e(),X) -> mark#(X) -> mark#(c()) -> a__c#() a__z#(e(),X) -> mark#(X) -> mark#(b()) -> a__b#() a__z#(e(),X) -> mark#(X) -> mark#(a()) -> a__a#() a__g#(d(),X,X) -> a__A#() -> a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) a__g#(d(),X,X) -> a__A#() -> a__A#() -> a__f#(a__a()) a__g#(d(),X,X) -> a__A#() -> a__A#() -> a__a#() a__g#(d(),X,X) -> a__A#() -> a__A#() -> a__f#(a__b()) a__g#(d(),X,X) -> a__A#() -> a__A#() -> a__b#() mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) mark#(f(X)) -> mark#(X) -> mark#(f(X)) -> mark#(X) mark#(f(X)) -> mark#(X) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(f(X)) -> mark#(X) -> mark#(z(X1,X2)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(k()) -> a__k#() mark#(f(X)) -> mark#(X) -> mark#(d()) -> a__d#() mark#(f(X)) -> mark#(X) -> mark#(c()) -> a__c#() mark#(f(X)) -> mark#(X) -> mark#(b()) -> a__b#() mark#(f(X)) -> mark#(X) -> mark#(a()) -> a__a#() mark#(f(X)) -> a__f#(mark(X)) -> a__f#(X) -> a__z#(mark(X),X) mark#(f(X)) -> a__f#(mark(X)) -> a__f#(X) -> mark#(X) mark#(z(X1,X2)) -> a__z#(mark(X1),X2) -> a__z#(e(),X) -> mark#(X) mark#(z(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> a__f#(mark(X)) mark#(z(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(z(X1,X2)) -> mark#(X1) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(z(X1,X2)) -> mark#(X1) -> mark#(z(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> mark#(X1) -> mark#(k()) -> a__k#() mark#(z(X1,X2)) -> mark#(X1) -> mark#(d()) -> a__d#() mark#(z(X1,X2)) -> mark#(X1) -> mark#(c()) -> a__c#() mark#(z(X1,X2)) -> mark#(X1) -> mark#(b()) -> a__b#() mark#(z(X1,X2)) -> mark#(X1) -> mark#(a()) -> a__a#() mark#(b()) -> a__b#() -> a__b#() -> a__d#() mark#(b()) -> a__b#() -> a__b#() -> a__c#() mark#(a()) -> a__a#() -> a__a#() -> a__d#() mark#(a()) -> a__a#() -> a__a#() -> a__c#() a__h#(X,X) -> a__g#(mark(X),mark(X),a__f(a__k())) -> a__g#(d(),X,X) -> a__A#() a__h#(X,X) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__h#(X,X) -> mark#(X) -> mark#(f(X)) -> mark#(X) a__h#(X,X) -> mark#(X) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) a__h#(X,X) -> mark#(X) -> mark#(z(X1,X2)) -> mark#(X1) a__h#(X,X) -> mark#(X) -> mark#(k()) -> a__k#() a__h#(X,X) -> mark#(X) -> mark#(d()) -> a__d#() a__h#(X,X) -> mark#(X) -> mark#(c()) -> a__c#() a__h#(X,X) -> mark#(X) -> mark#(b()) -> a__b#() a__h#(X,X) -> mark#(X) -> mark#(a()) -> a__a#() a__h#(X,X) -> a__f#(a__k()) -> a__f#(X) -> a__z#(mark(X),X) a__h#(X,X) -> a__f#(a__k()) -> a__f#(X) -> mark#(X) a__f#(X) -> a__z#(mark(X),X) -> a__z#(e(),X) -> mark#(X) a__f#(X) -> mark#(X) -> mark#(f(X)) -> a__f#(mark(X)) a__f#(X) -> mark#(X) -> mark#(f(X)) -> mark#(X) a__f#(X) -> mark#(X) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) a__f#(X) -> mark#(X) -> mark#(z(X1,X2)) -> mark#(X1) a__f#(X) -> mark#(X) -> mark#(k()) -> a__k#() a__f#(X) -> mark#(X) -> mark#(d()) -> a__d#() a__f#(X) -> mark#(X) -> mark#(c()) -> a__c#() a__f#(X) -> mark#(X) -> mark#(b()) -> a__b#() a__f#(X) -> mark#(X) -> mark#(a()) -> a__a#() a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) -> a__h#(X,X) -> a__g#(mark(X),mark(X),a__f(a__k())) a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) -> a__h#(X,X) -> mark#(X) a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) -> a__h#(X,X) -> a__f#(a__k()) a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) -> a__h#(X,X) -> a__k#() a__A#() -> a__f#(a__b()) -> a__f#(X) -> a__z#(mark(X),X) a__A#() -> a__f#(a__b()) -> a__f#(X) -> mark#(X) a__A#() -> a__f#(a__a()) -> a__f#(X) -> a__z#(mark(X),X) a__A#() -> a__f#(a__a()) -> a__f#(X) -> mark#(X) a__A#() -> a__b#() -> a__b#() -> a__d#() a__A#() -> a__b#() -> a__b#() -> a__c#() a__A#() -> a__a#() -> a__a#() -> a__d#() a__A#() -> a__a#() -> a__a#() -> a__c#() SCC Processor: #sccs: 2 #rules: 10 #arcs: 73/676 DPs: a__g#(d(),X,X) -> a__A#() a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) a__h#(X,X) -> a__g#(mark(X),mark(X),a__f(a__k())) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) Open DPs: a__z#(e(),X) -> mark#(X) mark#(z(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) a__f#(X) -> mark#(X) a__f#(X) -> a__z#(mark(X),X) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) Arctic Interpretation Processor: dimension: 1 interpretation: [a__z#](x0, x1) = x0 + x1 + 0, [mark#](x0) = x0, [a__f#](x0) = x0 + 0, [h](x0, x1) = 1, [f](x0) = 3x0 + 3, [z](x0, x1) = x0 + x1 + 0, [k] = 0, [c] = 4, [b] = 4, [a] = 4, [a__z](x0, x1) = x0 + x1 + 0, [d] = 4, [a__g](x0, x1, x2) = x1 + 4x2 + 7, [mark](x0) = x0 + 0, [a__h](x0, x1) = x1 + 7, [a__f](x0) = 3x0 + 3, [a__A] = 7, [m] = 0, [a__d] = 4, [l] = 0, [a__k] = 0, [e] = 4, [a__b] = 4, [a__c] = 4, [a__a] = 4 orientation: a__z#(e(),X) = X + 4 >= X = mark#(X) mark#(z(X1,X2)) = X1 + X2 + 0 >= X1 = mark#(X1) mark#(z(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__z#(mark(X1),X2) mark#(f(X)) = 3X + 3 >= X = mark#(X) mark#(f(X)) = 3X + 3 >= X + 0 = a__f#(mark(X)) a__f#(X) = X + 0 >= X = mark#(X) a__f#(X) = X + 0 >= X + 0 = a__z#(mark(X),X) a__a() = 4 >= 4 = a__c() a__b() = 4 >= 4 = a__c() a__c() = 4 >= 4 = e() a__k() = 0 >= 0 = l() a__d() = 4 >= 0 = m() a__a() = 4 >= 4 = a__d() a__b() = 4 >= 4 = a__d() a__c() = 4 >= 0 = l() a__k() = 0 >= 0 = m() a__A() = 7 >= 7 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = X + 7 >= X + 7 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 4X + 7 >= 7 = a__A() a__f(X) = 3X + 3 >= X + 0 = a__z(mark(X),X) a__z(e(),X) = X + 4 >= X + 0 = mark(X) mark(a()) = 4 >= 4 = a__a() mark(b()) = 4 >= 4 = a__b() mark(c()) = 4 >= 4 = a__c() mark(d()) = 4 >= 4 = a__d() mark(k()) = 0 >= 0 = a__k() mark(z(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__z(mark(X1),X2) mark(f(X)) = 3X + 3 >= 3X + 3 = a__f(mark(X)) mark(e()) = 4 >= 4 = e() mark(l()) = 0 >= 0 = l() mark(m()) = 0 >= 0 = m() a__a() = 4 >= 4 = a() a__b() = 4 >= 4 = b() a__c() = 4 >= 4 = c() a__d() = 4 >= 4 = d() a__k() = 0 >= 0 = k() a__z(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = z(X1,X2) a__f(X) = 3X + 3 >= 3X + 3 = f(X) a__h(X1,X2) = X2 + 7 >= 1 = h(X1,X2) problem: DPs: a__z#(e(),X) -> mark#(X) mark#(z(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> a__z#(mark(X1),X2) a__f#(X) -> mark#(X) a__f#(X) -> a__z#(mark(X),X) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) SCC Processor: #sccs: 1 #rules: 3 #arcs: 20/25 DPs: a__z#(e(),X) -> mark#(X) mark#(z(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> a__z#(mark(X1),X2) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) Subterm Criterion Processor: simple projection: pi(mark#) = 0 pi(a__z#) = 1 problem: DPs: a__z#(e(),X) -> mark#(X) TRS: a__a() -> a__c() a__b() -> a__c() a__c() -> e() a__k() -> l() a__d() -> m() a__a() -> a__d() a__b() -> a__d() a__c() -> l() a__k() -> m() a__A() -> a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) -> a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) -> a__A() a__f(X) -> a__z(mark(X),X) a__z(e(),X) -> mark(X) mark(a()) -> a__a() mark(b()) -> a__b() mark(c()) -> a__c() mark(d()) -> a__d() mark(k()) -> a__k() mark(z(X1,X2)) -> a__z(mark(X1),X2) mark(f(X)) -> a__f(mark(X)) mark(e()) -> e() mark(l()) -> l() mark(m()) -> m() a__a() -> a() a__b() -> b() a__c() -> c() a__d() -> d() a__k() -> k() a__z(X1,X2) -> z(X1,X2) a__f(X) -> f(X) a__h(X1,X2) -> h(X1,X2) SCC Processor: #sccs: 0 #rules: 0 #arcs: 5/1