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)
↳ QTRS
↳ DependencyPairsProof
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)
MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A1 → A__A
MARK(k) → A__K
A__A1 → A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__A1 → A__B
A__A → A__C
A__A → A__D
MARK(A) → A__A1
A__H(X, X) → A__K
A__A1 → A__F(a__b)
A__A1 → A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__B → A__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__B → A__D
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
MARK(g(X1, X2, X3)) → MARK(X2)
MARK(b) → A__B
A__A1 → A__A
MARK(k) → A__K
A__A1 → A__H(a__f(a__a), a__f(a__b))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__A1 → A__B
A__A → A__C
A__A → A__D
MARK(A) → A__A1
A__H(X, X) → A__K
A__A1 → A__F(a__b)
A__A1 → A__F(a__a)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__B → A__C
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
MARK(a) → A__A
MARK(c) → A__C
MARK(f(X)) → A__F(mark(X))
MARK(d) → A__D
A__B → A__D
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
A__F(X) → A__Z(mark(X), X)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
A__A1 → A__H(a__f(a__a), a__f(a__b))
A__H(X, X) → A__G(mark(X), mark(X), a__f(a__k))
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
A__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
MARK(A) → A__A1
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
A__A1 → A__F(a__b)
A__A1 → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(g(X1, X2, X3)) → MARK(X2)
MARK(g(X1, X2, X3)) → MARK(X1)
MARK(h(X1, X2)) → A__H(mark(X1), mark(X2))
MARK(h(X1, X2)) → MARK(X1)
MARK(g(X1, X2, X3)) → A__G(mark(X1), mark(X2), mark(X3))
MARK(A) → A__A1
MARK(g(X1, X2, X3)) → MARK(X3)
MARK(h(X1, X2)) → MARK(X2)
Used ordering: Polynomial interpretation [25,35]:
A__F(X) → A__Z(mark(X), X)
A__A1 → 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__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__A1 → A__F(a__b)
A__A1 → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
The value of delta used in the strict ordering is 1.
POL(a__b) = 0
POL(z(x1, x2)) = x_1 + (3)x_2
POL(a__h(x1, x2)) = 1 + (2)x_1 + (2)x_2
POL(A__F(x1)) = x_1
POL(mark(x1)) = x_1
POL(a__k) = 0
POL(a__c) = 0
POL(f(x1)) = (4)x_1
POL(g(x1, x2, x3)) = 1 + x_1 + x_2 + x_3
POL(b) = 0
POL(a__a) = 0
POL(c) = 0
POL(a) = 0
POL(e) = 0
POL(k) = 0
POL(A__A1) = 0
POL(d) = 0
POL(A) = 1
POL(a__d) = 0
POL(a__A) = 1
POL(a__z(x1, x2)) = x_1 + (3)x_2
POL(m) = 0
POL(A__Z(x1, x2)) = x_2
POL(MARK(x1)) = x_1
POL(l) = 0
POL(a__g(x1, x2, x3)) = 1 + x_1 + x_2 + x_3
POL(a__f(x1)) = (4)x_1
POL(h(x1, x2)) = 1 + (2)x_1 + (2)x_2
POL(A__H(x1, x2)) = (2)x_1
POL(A__G(x1, x2, x3)) = 0
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)
a__b → b
a__c → c
a__d → d
a__k → k
a__a → a__c
a__k → l
a__d → m
a__b → a__c
a__c → e
a__c → l
a__k → m
a__a → a__d
a__b → a__d
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__g(d, X, X) → a__A
mark(b) → a__b
mark(a) → a__a
mark(A) → a__A
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(k) → a__k
mark(d) → a__d
mark(c) → a__c
mark(e) → e
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
a__a → a
a__A → A
mark(m) → m
mark(l) → l
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
A__F(X) → A__Z(mark(X), X)
A__A1 → 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__H(X, X) → MARK(X)
A__F(X) → MARK(X)
A__G(d, X, X) → A__A1
A__H(X, X) → A__F(a__k)
A__Z(e, X) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__A1 → A__F(a__b)
A__A1 → A__F(a__a)
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
A__F(X) → A__Z(mark(X), X)
MARK(f(X)) → A__F(mark(X))
A__F(X) → MARK(X)
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)
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)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
MARK(f(X)) → A__F(mark(X))
MARK(z(X1, X2)) → MARK(X1)
MARK(f(X)) → MARK(X)
MARK(z(X1, X2)) → A__Z(mark(X1), X2)
A__Z(e, X) → MARK(X)
Used ordering: Polynomial interpretation [25,35]:
A__F(X) → A__Z(mark(X), X)
A__F(X) → MARK(X)
The value of delta used in the strict ordering is 4.
POL(a__b) = 4
POL(z(x1, x2)) = 4 + (2)x_1 + x_2
POL(a__h(x1, x2)) = 0
POL(A__F(x1)) = (3)x_1
POL(mark(x1)) = x_1
POL(a__k) = 4
POL(a__c) = 4
POL(f(x1)) = 4 + (4)x_1
POL(g(x1, x2, x3)) = 0
POL(b) = 4
POL(a__a) = 4
POL(c) = 4
POL(a) = 4
POL(e) = 4
POL(k) = 4
POL(d) = 1
POL(A) = 0
POL(a__d) = 1
POL(a__A) = 0
POL(a__z(x1, x2)) = 4 + (2)x_1 + x_2
POL(MARK(x1)) = x_1
POL(A__Z(x1, x2)) = (2)x_1 + x_2
POL(m) = 0
POL(l) = 1
POL(a__f(x1)) = 4 + (4)x_1
POL(a__g(x1, x2, x3)) = 0
POL(h(x1, x2)) = 0
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)
a__b → b
a__c → c
a__d → d
a__k → k
a__a → a__c
a__k → l
a__d → m
a__b → a__c
a__c → e
a__c → l
a__k → m
a__a → a__d
a__b → a__d
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__g(d, X, X) → a__A
mark(b) → a__b
mark(a) → a__a
mark(A) → a__A
a__f(X) → a__z(mark(X), X)
mark(z(X1, X2)) → a__z(mark(X1), X2)
mark(f(X)) → a__f(mark(X))
a__z(e, X) → mark(X)
mark(k) → a__k
mark(d) → a__d
mark(c) → a__c
mark(e) → e
mark(g(X1, X2, X3)) → a__g(mark(X1), mark(X2), mark(X3))
mark(h(X1, X2)) → a__h(mark(X1), mark(X2))
a__a → a
a__A → A
mark(m) → m
mark(l) → l
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
A__F(X) → A__Z(mark(X), X)
A__F(X) → MARK(X)
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)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
A__A1 → 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__A1
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)