(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(x, y, w, w, a) → g1(x, x, y, w)
f(x, y, w, a, a) → g1(y, x, x, w)
f(x, y, a, a, w) → g2(x, y, y, w)
f(x, y, a, w, w) → g2(y, y, x, w)
g1(x, x, y, a) → h(x, y)
g1(y, x, x, a) → h(x, y)
g2(x, y, y, a) → h(x, y)
g2(y, y, x, a) → h(x, y)
h(x, x) → x
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, z1, z2, z2, a) → g1(z0, z0, z1, z2)
f(z0, z1, z2, a, a) → g1(z1, z0, z0, z2)
f(z0, z1, a, a, z2) → g2(z0, z1, z1, z2)
f(z0, z1, a, z2, z2) → g2(z1, z1, z0, z2)
g1(z0, z0, z1, a) → h(z0, z1)
g1(z0, z1, z1, a) → h(z1, z0)
g2(z0, z1, z1, a) → h(z0, z1)
g2(z0, z0, z1, a) → h(z1, z0)
h(z0, z0) → z0
Tuples:
F(z0, z1, z2, z2, a) → c(G1(z0, z0, z1, z2))
F(z0, z1, z2, a, a) → c1(G1(z1, z0, z0, z2))
F(z0, z1, a, a, z2) → c2(G2(z0, z1, z1, z2))
F(z0, z1, a, z2, z2) → c3(G2(z1, z1, z0, z2))
G1(z0, z0, z1, a) → c4(H(z0, z1))
G1(z0, z1, z1, a) → c5(H(z1, z0))
G2(z0, z1, z1, a) → c6(H(z0, z1))
G2(z0, z0, z1, a) → c7(H(z1, z0))
S tuples:
F(z0, z1, z2, z2, a) → c(G1(z0, z0, z1, z2))
F(z0, z1, z2, a, a) → c1(G1(z1, z0, z0, z2))
F(z0, z1, a, a, z2) → c2(G2(z0, z1, z1, z2))
F(z0, z1, a, z2, z2) → c3(G2(z1, z1, z0, z2))
G1(z0, z0, z1, a) → c4(H(z0, z1))
G1(z0, z1, z1, a) → c5(H(z1, z0))
G2(z0, z1, z1, a) → c6(H(z0, z1))
G2(z0, z0, z1, a) → c7(H(z1, z0))
K tuples:none
Defined Rule Symbols:
f, g1, g2, h
Defined Pair Symbols:
F, G1, G2
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 8 trailing nodes:
F(z0, z1, a, a, z2) → c2(G2(z0, z1, z1, z2))
F(z0, z1, a, z2, z2) → c3(G2(z1, z1, z0, z2))
G2(z0, z1, z1, a) → c6(H(z0, z1))
F(z0, z1, z2, z2, a) → c(G1(z0, z0, z1, z2))
G1(z0, z1, z1, a) → c5(H(z1, z0))
F(z0, z1, z2, a, a) → c1(G1(z1, z0, z0, z2))
G1(z0, z0, z1, a) → c4(H(z0, z1))
G2(z0, z0, z1, a) → c7(H(z1, z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0, z1, z2, z2, a) → g1(z0, z0, z1, z2)
f(z0, z1, z2, a, a) → g1(z1, z0, z0, z2)
f(z0, z1, a, a, z2) → g2(z0, z1, z1, z2)
f(z0, z1, a, z2, z2) → g2(z1, z1, z0, z2)
g1(z0, z0, z1, a) → h(z0, z1)
g1(z0, z1, z1, a) → h(z1, z0)
g2(z0, z1, z1, a) → h(z0, z1)
g2(z0, z0, z1, a) → h(z1, z0)
h(z0, z0) → z0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
f, g1, g2, h
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))