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: 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#(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)) mark#(h(X1,X2)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X1) mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) 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(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) 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#(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)) mark#(h(X1,X2)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X1) mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) 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(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) graph: a__z#(e(),X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) a__z#(e(),X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X1) a__z#(e(),X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X2) a__z#(e(),X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X3) a__z#(e(),X) -> mark#(X) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) a__z#(e(),X) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X1) a__z#(e(),X) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X2) 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__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#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) -> a__g#(d(),X,X) -> a__A#() mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(h(X1,X2)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(h(X1,X2)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(f(X)) -> a__f#(mark(X)) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(f(X)) -> mark#(X) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(z(X1,X2)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(k()) -> a__k#() mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(d()) -> a__d#() mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(c()) -> a__c#() mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(b()) -> a__b#() mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(a()) -> a__a#() mark#(g(X1,X2,X3)) -> mark#(X3) -> mark#(A()) -> a__A#() mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(h(X1,X2)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(h(X1,X2)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> a__f#(mark(X)) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(z(X1,X2)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(k()) -> a__k#() mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(d()) -> a__d#() mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(c()) -> a__c#() mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(b()) -> a__b#() mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(a()) -> a__a#() mark#(g(X1,X2,X3)) -> mark#(X2) -> mark#(A()) -> a__A#() mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(h(X1,X2)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(h(X1,X2)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> a__f#(mark(X)) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(z(X1,X2)) -> mark#(X1) mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(k()) -> a__k#() mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(d()) -> a__d#() mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(c()) -> a__c#() mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(b()) -> a__b#() mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(a()) -> a__a#() mark#(g(X1,X2,X3)) -> mark#(X1) -> mark#(A()) -> a__A#() mark#(h(X1,X2)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(h(X1,X2)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(h(X1,X2)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X2) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(h(X1,X2)) -> mark#(X2) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(h(X1,X2)) -> mark#(X2) -> mark#(h(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> mark#(X2) -> mark#(h(X1,X2)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X2) -> mark#(f(X)) -> a__f#(mark(X)) mark#(h(X1,X2)) -> mark#(X2) -> mark#(f(X)) -> mark#(X) mark#(h(X1,X2)) -> mark#(X2) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(h(X1,X2)) -> mark#(X2) -> mark#(z(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> mark#(X2) -> mark#(k()) -> a__k#() mark#(h(X1,X2)) -> mark#(X2) -> mark#(d()) -> a__d#() mark#(h(X1,X2)) -> mark#(X2) -> mark#(c()) -> a__c#() mark#(h(X1,X2)) -> mark#(X2) -> mark#(b()) -> a__b#() mark#(h(X1,X2)) -> mark#(X2) -> mark#(a()) -> a__a#() mark#(h(X1,X2)) -> mark#(X2) -> mark#(A()) -> a__A#() mark#(h(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(h(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(h(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(h(X1,X2)) -> mark#(X1) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(h(X1,X2)) -> mark#(X1) -> mark#(h(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> mark#(X1) -> mark#(h(X1,X2)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> a__f#(mark(X)) mark#(h(X1,X2)) -> mark#(X1) -> mark#(f(X)) -> mark#(X) mark#(h(X1,X2)) -> mark#(X1) -> mark#(z(X1,X2)) -> a__z#(mark(X1),X2) mark#(h(X1,X2)) -> mark#(X1) -> mark#(z(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> mark#(X1) -> mark#(k()) -> a__k#() mark#(h(X1,X2)) -> mark#(X1) -> mark#(d()) -> a__d#() mark#(h(X1,X2)) -> mark#(X1) -> mark#(c()) -> a__c#() mark#(h(X1,X2)) -> mark#(X1) -> mark#(b()) -> a__b#() mark#(h(X1,X2)) -> mark#(X1) -> mark#(a()) -> a__a#() mark#(h(X1,X2)) -> mark#(X1) -> mark#(A()) -> a__A#() mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) -> a__h#(X,X) -> a__g#(mark(X),mark(X),a__f(a__k())) mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) -> a__h#(X,X) -> mark#(X) mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) -> a__h#(X,X) -> a__f#(a__k()) mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) -> a__h#(X,X) -> a__k#() mark#(f(X)) -> mark#(X) -> mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(f(X)) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(f(X)) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(f(X)) -> mark#(X) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(f(X)) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X1) mark#(f(X)) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X2) 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)) -> 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#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) mark#(z(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X1) mark#(z(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X2) mark#(z(X1,X2)) -> mark#(X1) -> mark#(g(X1,X2,X3)) -> mark#(X3) mark#(z(X1,X2)) -> mark#(X1) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) mark#(z(X1,X2)) -> mark#(X1) -> mark#(h(X1,X2)) -> mark#(X1) mark#(z(X1,X2)) -> mark#(X1) -> mark#(h(X1,X2)) -> mark#(X2) 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#(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#() mark#(A()) -> a__A#() -> a__A#() -> a__h#(a__f(a__a()),a__f(a__b())) mark#(A()) -> a__A#() -> a__A#() -> a__f#(a__a()) mark#(A()) -> a__A#() -> a__A#() -> a__a#() mark#(A()) -> a__A#() -> a__A#() -> a__f#(a__b()) mark#(A()) -> a__A#() -> a__A#() -> a__b#() 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#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) a__h#(X,X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X1) a__h#(X,X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X2) a__h#(X,X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X3) a__h#(X,X) -> mark#(X) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) a__h#(X,X) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X1) a__h#(X,X) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X2) 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) -> 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#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) a__f#(X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X1) a__f#(X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X2) a__f#(X) -> mark#(X) -> mark#(g(X1,X2,X3)) -> mark#(X3) a__f#(X) -> mark#(X) -> mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) a__f#(X) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X1) a__f#(X) -> mark#(X) -> mark#(h(X1,X2)) -> mark#(X2) 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__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: 1 #rules: 22 #arcs: 208/1156 DPs: a__z#(e(),X) -> mark#(X) mark#(A()) -> a__A#() a__A#() -> a__f#(a__b()) a__f#(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) -> a__z#(mark(X),X) mark#(h(X1,X2)) -> mark#(X2) mark#(h(X1,X2)) -> mark#(X1) mark#(h(X1,X2)) -> a__h#(mark(X1),mark(X2)) a__h#(X,X) -> a__f#(a__k()) a__h#(X,X) -> mark#(X) mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> mark#(X2) mark#(g(X1,X2,X3)) -> mark#(X1) mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) a__g#(d(),X,X) -> 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__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(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) Arctic Interpretation Processor: dimension: 1 interpretation: [a__z#](x0, x1) = x0 + x1 + 0, [a__g#](x0, x1, x2) = x0 + x1 + x2 + 0, [mark#](x0) = x0, [a__h#](x0, x1) = x0 + x1 + 0, [a__f#](x0) = x0 + 0, [a__A#] = 0, [g](x0, x1, x2) = 4x0 + 4x1 + x2 + 4, [h](x0, x1) = 4x0 + 4x1 + 4, [f](x0) = x0 + 0, [z](x0, x1) = x0 + x1 + 0, [k] = 0, [c] = 0, [b] = 0, [a] = 0, [A] = 4, [a__z](x0, x1) = x0 + x1 + 0, [d] = 0, [a__g](x0, x1, x2) = 4x0 + 4x1 + x2 + 4, [mark](x0) = x0 + 0, [a__h](x0, x1) = 4x0 + 4x1 + 4, [a__f](x0) = x0 + 0, [a__A] = 4, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 0, [a__b] = 0, [a__c] = 0, [a__a] = 0 orientation: a__z#(e(),X) = X + 0 >= X = mark#(X) mark#(A()) = 4 >= 0 = a__A#() a__A#() = 0 >= 0 = a__f#(a__b()) a__f#(X) = X + 0 >= 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)) = X + 0 >= X = mark#(X) mark#(f(X)) = X + 0 >= X + 0 = a__f#(mark(X)) a__f#(X) = X + 0 >= X + 0 = a__z#(mark(X),X) mark#(h(X1,X2)) = 4X1 + 4X2 + 4 >= X2 = mark#(X2) mark#(h(X1,X2)) = 4X1 + 4X2 + 4 >= X1 = mark#(X1) mark#(h(X1,X2)) = 4X1 + 4X2 + 4 >= X1 + X2 + 0 = a__h#(mark(X1),mark(X2)) a__h#(X,X) = X + 0 >= 0 = a__f#(a__k()) a__h#(X,X) = X + 0 >= X = mark#(X) mark#(g(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= X3 = mark#(X3) mark#(g(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= X2 = mark#(X2) mark#(g(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= X1 = mark#(X1) mark#(g(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= X1 + X2 + X3 + 0 = a__g#(mark(X1),mark(X2),mark(X3)) a__g#(d(),X,X) = X + 0 >= 0 = a__A#() a__A#() = 0 >= 0 = a__f#(a__a()) a__A#() = 0 >= 0 = a__h#(a__f(a__a()),a__f(a__b())) a__h#(X,X) = X + 0 >= X + 0 = a__g#(mark(X),mark(X),a__f(a__k())) 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() = 4 >= 4 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = 4X + 4 >= 4X + 4 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 4X + 4 >= 4 = a__A() a__f(X) = X + 0 >= X + 0 = a__z(mark(X),X) a__z(e(),X) = X + 0 >= X + 0 = mark(X) mark(A()) = 4 >= 4 = 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)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__z(mark(X1),X2) mark(f(X)) = X + 0 >= X + 0 = a__f(mark(X)) mark(h(X1,X2)) = 4X1 + 4X2 + 4 >= 4X1 + 4X2 + 4 = a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) = 4X1 + 4X2 + X3 + 4 >= 4X1 + 4X2 + X3 + 4 = 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() = 4 >= 4 = 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 + X2 + 0 >= X1 + X2 + 0 = z(X1,X2) a__f(X) = X + 0 >= X + 0 = f(X) a__h(X1,X2) = 4X1 + 4X2 + 4 >= 4X1 + 4X2 + 4 = h(X1,X2) a__g(X1,X2,X3) = 4X1 + 4X2 + X3 + 4 >= 4X1 + 4X2 + X3 + 4 = g(X1,X2,X3) problem: DPs: a__z#(e(),X) -> mark#(X) a__A#() -> a__f#(a__b()) a__f#(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) -> a__z#(mark(X),X) a__h#(X,X) -> a__f#(a__k()) a__h#(X,X) -> mark#(X) mark#(g(X1,X2,X3)) -> mark#(X3) mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) a__g#(d(),X,X) -> 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__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(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) Arctic Interpretation Processor: dimension: 1 interpretation: [a__z#](x0, x1) = x1, [a__g#](x0, x1, x2) = x0 + x2 + 0, [mark#](x0) = x0, [a__h#](x0, x1) = x0 + x1 + 0, [a__f#](x0) = x0, [a__A#] = 0, [g](x0, x1, x2) = 7x0 + 7x1 + 7x2 + 0, [h](x0, x1) = 7x0 + 7, [f](x0) = x0, [z](x0, x1) = x0 + x1, [k] = 0, [c] = 0, [b] = 0, [a] = 0, [A] = 7, [a__z](x0, x1) = x0 + x1, [d] = 0, [a__g](x0, x1, x2) = 7x0 + 7x1 + 7x2 + 0, [mark](x0) = x0, [a__h](x0, x1) = 7x0 + 7, [a__f](x0) = x0, [a__A] = 7, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 0, [a__b] = 0, [a__c] = 0, [a__a] = 0 orientation: a__z#(e(),X) = X >= X = mark#(X) a__A#() = 0 >= 0 = a__f#(a__b()) a__f#(X) = X >= X = mark#(X) mark#(z(X1,X2)) = X1 + X2 >= X1 = mark#(X1) mark#(z(X1,X2)) = X1 + X2 >= X2 = a__z#(mark(X1),X2) mark#(f(X)) = X >= X = mark#(X) mark#(f(X)) = X >= X = a__f#(mark(X)) a__f#(X) = X >= X = a__z#(mark(X),X) a__h#(X,X) = X + 0 >= 0 = a__f#(a__k()) a__h#(X,X) = X + 0 >= X = mark#(X) mark#(g(X1,X2,X3)) = 7X1 + 7X2 + 7X3 + 0 >= X3 = mark#(X3) mark#(g(X1,X2,X3)) = 7X1 + 7X2 + 7X3 + 0 >= X1 + X3 + 0 = a__g#(mark(X1),mark(X2),mark(X3)) a__g#(d(),X,X) = X + 0 >= 0 = a__A#() a__A#() = 0 >= 0 = a__f#(a__a()) a__A#() = 0 >= 0 = a__h#(a__f(a__a()),a__f(a__b())) a__h#(X,X) = X + 0 >= X + 0 = a__g#(mark(X),mark(X),a__f(a__k())) 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() = 7 >= 7 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = 7X + 7 >= 7X + 7 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 7X + 7 >= 7 = a__A() a__f(X) = X >= X = a__z(mark(X),X) a__z(e(),X) = X + 0 >= X = mark(X) mark(A()) = 7 >= 7 = 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)) = X1 + X2 >= X1 + X2 = a__z(mark(X1),X2) mark(f(X)) = X >= X = a__f(mark(X)) mark(h(X1,X2)) = 7X1 + 7 >= 7X1 + 7 = a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) = 7X1 + 7X2 + 7X3 + 0 >= 7X1 + 7X2 + 7X3 + 0 = 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() = 7 >= 7 = 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 + X2 >= X1 + X2 = z(X1,X2) a__f(X) = X >= X = f(X) a__h(X1,X2) = 7X1 + 7 >= 7X1 + 7 = h(X1,X2) a__g(X1,X2,X3) = 7X1 + 7X2 + 7X3 + 0 >= 7X1 + 7X2 + 7X3 + 0 = g(X1,X2,X3) problem: DPs: a__z#(e(),X) -> mark#(X) a__A#() -> a__f#(a__b()) a__f#(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) -> a__z#(mark(X),X) a__h#(X,X) -> a__f#(a__k()) a__h#(X,X) -> mark#(X) mark#(g(X1,X2,X3)) -> a__g#(mark(X1),mark(X2),mark(X3)) a__g#(d(),X,X) -> 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__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(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) Arctic Interpretation Processor: dimension: 1 interpretation: [a__z#](x0, x1) = x0 + x1 + 0, [a__g#](x0, x1, x2) = x0 + x1 + x2, [mark#](x0) = x0, [a__h#](x0, x1) = x0 + x1 + 0, [a__f#](x0) = x0 + 0, [a__A#] = 0, [g](x0, x1, x2) = 2x0 + 2x1 + 1x2 + 0, [h](x0, x1) = 2x0 + 2x1 + 1, [f](x0) = x0 + 0, [z](x0, x1) = x0 + x1 + 0, [k] = 0, [c] = 0, [b] = 0, [a] = 0, [A] = 2, [a__z](x0, x1) = x0 + x1 + 0, [d] = 0, [a__g](x0, x1, x2) = 2x0 + 2x1 + 1x2 + 0, [mark](x0) = x0, [a__h](x0, x1) = 2x0 + 2x1 + 1, [a__f](x0) = x0 + 0, [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__z#(e(),X) = X + 0 >= X = mark#(X) a__A#() = 0 >= 0 = a__f#(a__b()) a__f#(X) = X + 0 >= 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)) = X + 0 >= X = mark#(X) mark#(f(X)) = X + 0 >= X + 0 = a__f#(mark(X)) a__f#(X) = X + 0 >= X + 0 = a__z#(mark(X),X) a__h#(X,X) = X + 0 >= 0 = a__f#(a__k()) a__h#(X,X) = X + 0 >= X = mark#(X) mark#(g(X1,X2,X3)) = 2X1 + 2X2 + 1X3 + 0 >= X1 + X2 + X3 = a__g#(mark(X1),mark(X2),mark(X3)) a__g#(d(),X,X) = X + 0 >= 0 = a__A#() a__A#() = 0 >= 0 = a__f#(a__a()) a__A#() = 0 >= 0 = a__h#(a__f(a__a()),a__f(a__b())) a__h#(X,X) = X + 0 >= X + 0 = a__g#(mark(X),mark(X),a__f(a__k())) 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) = 2X + 1 >= 2X + 1 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 2X + 2 >= 2 = a__A() a__f(X) = X + 0 >= X + 0 = a__z(mark(X),X) a__z(e(),X) = X + 0 >= X = mark(X) mark(A()) = 2 >= 2 = 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)) = X1 + X2 + 0 >= X1 + X2 + 0 = a__z(mark(X1),X2) mark(f(X)) = X + 0 >= X + 0 = a__f(mark(X)) mark(h(X1,X2)) = 2X1 + 2X2 + 1 >= 2X1 + 2X2 + 1 = a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) = 2X1 + 2X2 + 1X3 + 0 >= 2X1 + 2X2 + 1X3 + 0 = 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() = 2 >= 2 = 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 + X2 + 0 >= X1 + X2 + 0 = z(X1,X2) a__f(X) = X + 0 >= X + 0 = f(X) a__h(X1,X2) = 2X1 + 2X2 + 1 >= 2X1 + 2X2 + 1 = h(X1,X2) a__g(X1,X2,X3) = 2X1 + 2X2 + 1X3 + 0 >= 2X1 + 2X2 + 1X3 + 0 = g(X1,X2,X3) problem: DPs: a__z#(e(),X) -> mark#(X) a__A#() -> a__f#(a__b()) a__f#(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) -> a__z#(mark(X),X) a__h#(X,X) -> a__f#(a__k()) a__h#(X,X) -> mark#(X) a__g#(d(),X,X) -> 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__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(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) SCC Processor: #sccs: 2 #rules: 10 #arcs: 144/196 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(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) 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(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) Matrix Interpretation Processor: dim=1 interpretation: [a__z#](x0, x1) = x0 + 2x1, [mark#](x0) = 2x0 + 1, [a__f#](x0) = 4x0 + 1, [g](x0, x1, x2) = 0, [h](x0, x1) = 0, [f](x0) = 4x0, [z](x0, x1) = x0 + x1, [k] = 0, [c] = 1, [b] = 2, [a] = 2, [A] = 0, [a__z](x0, x1) = x0 + 2x1, [d] = 0, [a__g](x0, x1, x2) = 0, [mark](x0) = 2x0, [a__h](x0, x1) = 0, [a__f](x0) = 4x0, [a__A] = 0, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 1, [a__b] = 3, [a__c] = 2, [a__a] = 2 orientation: a__z#(e(),X) = 2X + 1 >= 2X + 1 = mark#(X) mark#(z(X1,X2)) = 2X1 + 2X2 + 1 >= 2X1 + 1 = mark#(X1) mark#(z(X1,X2)) = 2X1 + 2X2 + 1 >= 2X1 + 2X2 = a__z#(mark(X1),X2) mark#(f(X)) = 8X + 1 >= 2X + 1 = mark#(X) mark#(f(X)) = 8X + 1 >= 8X + 1 = a__f#(mark(X)) a__f#(X) = 4X + 1 >= 2X + 1 = mark#(X) a__f#(X) = 4X + 1 >= 4X = a__z#(mark(X),X) a__a() = 2 >= 2 = a__c() a__b() = 3 >= 2 = a__c() a__c() = 2 >= 1 = e() a__k() = 0 >= 0 = l() a__d() = 0 >= 0 = m() a__a() = 2 >= 0 = a__d() a__b() = 3 >= 0 = a__d() a__c() = 2 >= 0 = l() a__k() = 0 >= 0 = m() a__A() = 0 >= 0 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = 0 >= 0 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = 0 >= 0 = a__A() a__f(X) = 4X >= 4X = a__z(mark(X),X) a__z(e(),X) = 2X + 1 >= 2X = mark(X) mark(A()) = 0 >= 0 = a__A() mark(a()) = 4 >= 2 = a__a() mark(b()) = 4 >= 3 = a__b() mark(c()) = 2 >= 2 = 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)) = 0 >= 0 = a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) = 0 >= 0 = a__g(mark(X1),mark(X2),mark(X3)) mark(e()) = 2 >= 1 = e() mark(l()) = 0 >= 0 = l() mark(m()) = 0 >= 0 = m() a__A() = 0 >= 0 = A() a__a() = 2 >= 2 = a() a__b() = 3 >= 2 = b() a__c() = 2 >= 1 = 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) = 0 >= 0 = h(X1,X2) a__g(X1,X2,X3) = 0 >= 0 = g(X1,X2,X3) problem: DPs: a__z#(e(),X) -> mark#(X) mark#(z(X1,X2)) -> mark#(X1) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) a__f#(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(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) SCC Processor: #sccs: 1 #rules: 4 #arcs: 20/25 DPs: mark#(z(X1,X2)) -> mark#(X1) mark#(f(X)) -> mark#(X) mark#(f(X)) -> a__f#(mark(X)) a__f#(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(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) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__f#](x0) = 4x0 + 0, [g](x0, x1, x2) = x2 + 4, [h](x0, x1) = x1 + 4, [f](x0) = 4x0 + 0, [z](x0, x1) = x0 + 1x1 + 0, [k] = 0, [c] = 0, [b] = 0, [a] = 3, [A] = 4, [a__z](x0, x1) = x0 + 1x1 + 0, [d] = 0, [a__g](x0, x1, x2) = x2 + 4, [mark](x0) = x0, [a__h](x0, x1) = x1 + 4, [a__f](x0) = 4x0 + 0, [a__A] = 4, [m] = 0, [a__d] = 0, [l] = 0, [a__k] = 0, [e] = 0, [a__b] = 0, [a__c] = 0, [a__a] = 3 orientation: mark#(z(X1,X2)) = X1 + 1X2 + 0 >= X1 = mark#(X1) mark#(f(X)) = 4X + 0 >= X = mark#(X) mark#(f(X)) = 4X + 0 >= 4X + 0 = a__f#(mark(X)) a__f#(X) = 4X + 0 >= X = mark#(X) a__a() = 3 >= 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() = 3 >= 0 = a__d() a__b() = 0 >= 0 = a__d() a__c() = 0 >= 0 = l() a__k() = 0 >= 0 = m() a__A() = 4 >= 4 = a__h(a__f(a__a()),a__f(a__b())) a__h(X,X) = X + 4 >= 4 = a__g(mark(X),mark(X),a__f(a__k())) a__g(d(),X,X) = X + 4 >= 4 = a__A() a__f(X) = 4X + 0 >= 1X + 0 = a__z(mark(X),X) a__z(e(),X) = 1X + 0 >= X = mark(X) mark(A()) = 4 >= 4 = a__A() mark(a()) = 3 >= 3 = 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)) = X1 + 1X2 + 0 >= X1 + 1X2 + 0 = a__z(mark(X1),X2) mark(f(X)) = 4X + 0 >= 4X + 0 = a__f(mark(X)) mark(h(X1,X2)) = X2 + 4 >= X2 + 4 = a__h(mark(X1),mark(X2)) mark(g(X1,X2,X3)) = X3 + 4 >= X3 + 4 = 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() = 4 >= 4 = A() a__a() = 3 >= 3 = 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 + 1X2 + 0 >= X1 + 1X2 + 0 = z(X1,X2) a__f(X) = 4X + 0 >= 4X + 0 = f(X) a__h(X1,X2) = X2 + 4 >= X2 + 4 = h(X1,X2) a__g(X1,X2,X3) = X3 + 4 >= X3 + 4 = g(X1,X2,X3) problem: DPs: mark#(z(X1,X2)) -> mark#(X1) 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(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) SCC Processor: #sccs: 1 #rules: 1 #arcs: 10/4 DPs: mark#(z(X1,X2)) -> mark#(X1) 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(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) Subterm Criterion Processor: simple projection: pi(mark#) = 0 problem: DPs: 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(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) Qed