YES(O(1), O(n^2)) 75.66/32.46 YES(O(1), O(n^2)) 76.01/32.56 76.01/32.56 76.01/32.56 76.01/32.56 76.01/32.56 76.01/32.56 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 76.01/32.56 76.01/32.56 76.01/32.56
76.01/32.56 76.01/32.56 76.01/32.56
76.01/32.56
76.01/32.56

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(nil) → nil 76.01/32.56
f(.(nil, y)) → .(nil, f(y)) 76.01/32.56
f(.(.(x, y), z)) → f(.(x, .(y, z))) 76.01/32.56
g(nil) → nil 76.01/32.56
g(.(x, nil)) → .(g(x), nil) 76.01/32.56
g(.(x, .(y, z))) → g(.(.(x, y), z))

Rewrite Strategy: INNERMOST
76.01/32.56
76.01/32.56

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
76.01/32.56
76.01/32.56

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.56
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.56
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.56
g(nil) → nil 76.01/32.56
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.56
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.56
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.56
G(.(z0, nil)) → c4(G(z0)) 76.01/32.56
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.56
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.56
G(.(z0, nil)) → c4(G(z0)) 76.01/32.56
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:none
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.56
76.01/32.56

(3) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(nil, z0)) → c1(F(z0))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.56
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.56
G(.(z0, nil)) → c4(G(z0)) 76.01/32.56
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
The order we found is given by the following interpretation:
Polynomial interpretation : 76.01/32.56

POL(.(x1, x2)) = [1] + x1 + x2    76.01/32.56
POL(F(x1)) = [4]x1    76.01/32.56
POL(G(x1)) = 0    76.01/32.56
POL(c1(x1)) = x1    76.01/32.56
POL(c2(x1)) = x1    76.01/32.56
POL(c4(x1)) = x1    76.01/32.56
POL(c5(x1)) = x1    76.01/32.56
POL(nil) = 0   
76.01/32.56
76.01/32.56

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.56
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.56
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.56
g(nil) → nil 76.01/32.56
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.56
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.56
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.56
G(.(z0, nil)) → c4(G(z0)) 76.01/32.56
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.56
G(.(z0, nil)) → c4(G(z0)) 76.01/32.56
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

F(.(nil, z0)) → c1(F(z0))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.56
76.01/32.56

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(.(z0, nil)) → c4(G(z0))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.56
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.56
G(.(z0, nil)) → c4(G(z0)) 76.01/32.56
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
The order we found is given by the following interpretation:
Polynomial interpretation : 76.01/32.56

POL(.(x1, x2)) = x1 + x2    76.01/32.56
POL(F(x1)) = 0    76.01/32.56
POL(G(x1)) = [4]x1    76.01/32.56
POL(c1(x1)) = x1    76.01/32.56
POL(c2(x1)) = x1    76.01/32.56
POL(c4(x1)) = x1    76.01/32.56
POL(c5(x1)) = x1    76.01/32.56
POL(nil) = [4]   
76.01/32.56
76.01/32.56

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.57
F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.57
G(.(z0, nil)) → c4(G(z0)) 76.01/32.57
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.57
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

F(.(nil, z0)) → c1(F(z0)) 76.01/32.57
G(.(z0, nil)) → c4(G(z0))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.57
76.01/32.57

(7) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, z0)) → c1(F(z0)) by

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
76.01/32.57
76.01/32.57

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.57
G(.(z0, nil)) → c4(G(z0)) 76.01/32.57
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) 76.01/32.57
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
S tuples:

F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) 76.01/32.57
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2)))
K tuples:

G(.(z0, nil)) → c4(G(z0)) 76.01/32.57
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

76.01/32.57
76.01/32.57

(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(z0, z1), z2)) → c2(F(.(z0, .(z1, z2)))) by

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
76.01/32.57
76.01/32.57

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, nil)) → c4(G(z0)) 76.01/32.57
G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) 76.01/32.57
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
S tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) 76.01/32.57
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
K tuples:

G(.(z0, nil)) → c4(G(z0)) 76.01/32.57
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

76.01/32.57
76.01/32.57

(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, nil)) → c4(G(z0)) by

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
76.01/32.57
76.01/32.57

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) 76.01/32.57
F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
S tuples:

G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) 76.01/32.57
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2))))
K tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

76.01/32.57
76.01/32.57

(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(z1, z2))) → c5(G(.(.(z0, z1), z2))) by

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
76.01/32.57
76.01/32.57

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) 76.01/32.57
F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.57
76.01/32.57

(15) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, .(nil, y0))) → c1(F(.(nil, y0))) by

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
76.01/32.57
76.01/32.57

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.57
76.01/32.57

(17) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(nil, .(.(y0, y1), y2))) → c1(F(.(.(y0, y1), y2))) by

F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
76.01/32.57
76.01/32.57

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
S tuples:

F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) 76.01/32.57
F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil)))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

76.01/32.57
76.01/32.57

(19) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(.(y0, y1), z1), z2)) → c2(F(.(.(y0, y1), .(z1, z2)))) by

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
76.01/32.57
76.01/32.57

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
S tuples:

F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) 76.01/32.57
F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

76.01/32.57
76.01/32.57

(21) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(nil, nil), z2)) → c2(F(.(nil, .(nil, z2)))) by

F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.57
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
76.01/32.57
76.01/32.57

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.57
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.57
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
S tuples:

F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.57
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.57
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c2, c4, c5, c1

76.01/32.57
76.01/32.57

(23) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(.(.(nil, .(y0, y1)), z2)) → c2(F(.(nil, .(.(y0, y1), z2)))) by

F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.57
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.57
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
76.01/32.57
76.01/32.57

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.57
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.57
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.57
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.57
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.57
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.57
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.57
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.57
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.57
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.57
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) 76.01/32.57
G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

76.01/32.57
76.01/32.57

(25) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(.(y0, nil), nil)) → c4(G(.(y0, nil))) by

G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.57
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
76.01/32.57
76.01/32.57

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.57
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.57
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.57
g(nil) → nil 76.01/32.57
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.57
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.57
G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.57
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.57
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.57
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.57
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.57
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.57
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.57
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.57
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.57
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.57
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.57
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.57
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.57
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.57
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.58
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.58
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) 76.01/32.58
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c4, c5, c1, c2

76.01/32.58
76.01/32.58

(27) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(.(y0, .(y1, y2)), nil)) → c4(G(.(y0, .(y1, y2)))) by

G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
76.01/32.58
76.01/32.58

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.58
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.58
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.58
g(nil) → nil 76.01/32.58
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.58
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.58
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.58
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
S tuples:

G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) 76.01/32.58
G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.58
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

76.01/32.58
76.01/32.58

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(z1, .(y1, y2)))) → c5(G(.(.(z0, z1), .(y1, y2)))) by

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
76.01/32.58
76.01/32.58

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.58
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.58
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.58
g(nil) → nil 76.01/32.58
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.58
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.58
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
S tuples:

G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) 76.01/32.58
G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil))))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

76.01/32.58
76.01/32.58

(31) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(nil, nil))) → c5(G(.(.(z0, nil), nil))) by

G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
76.01/32.58
76.01/32.58

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.58
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.58
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.58
g(nil) → nil 76.01/32.58
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.58
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
S tuples:

G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

G, F

Compound Symbols:

c5, c1, c2, c4

76.01/32.58
76.01/32.58

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace G(.(z0, .(.(y1, y2), nil))) → c5(G(.(.(z0, .(y1, y2)), nil))) by

G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
76.01/32.58
76.01/32.58

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.58
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.58
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.58
g(nil) → nil 76.01/32.58
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.58
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.58
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.58
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.58
76.01/32.58

(35) CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.58
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]: 76.01/32.58
Non-tuple symbols:
76.01/32.58
M( f(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/00\
\00/
·x1

76.01/32.58
M( g(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/00\
\00/
·x1

76.01/32.58
M( .(x1, x2) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/10\
\00/
·x1+ 76.01/32.58 76.01/32.58
/11\
\00/
·x2

76.01/32.58
M( nil ) = 76.01/32.58 76.01/32.58
/0\
\4/

Tuple symbols:
76.01/32.58
M( c5(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/10\
\00/
·x1

76.01/32.58
M( f(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/00\
\00/
·x1

76.01/32.58
M( c1(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/10\
\00/
·x1

76.01/32.58
M( c2(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/10\
\00/
·x1

76.01/32.58
M( c4(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/10\
\00/
·x1

76.01/32.58
M( g(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/00\
\00/
·x1

76.01/32.58
M( G(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/00\
\00/
·x1

76.01/32.58
M( F(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/10\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
76.01/32.58
76.01/32.58

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.58
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.58
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.58
g(nil) → nil 76.01/32.58
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.58
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.58
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.58
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2)))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.58
76.01/32.58

(37) CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.58
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.58
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.58
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.58
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.58
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.58
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.58
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.58
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.58
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.58
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.58
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.58
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.58
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.58
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.58
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.58
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.58
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.58
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.58
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.58
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.58
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.58
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.58
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.58
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]: 76.01/32.58
Non-tuple symbols:
76.01/32.58
M( f(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.58 76.01/32.58
/00\
\00/
·x1

76.01/32.59
M( g(x1) ) = 76.01/32.58 76.01/32.58
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( .(x1, x2) ) = 76.01/32.59 76.01/32.59
/0\
\4/
+ 76.01/32.59 76.01/32.59
/14\
\00/
·x1+ 76.01/32.59 76.01/32.59
/10\
\01/
·x2

76.01/32.59
M( nil ) = 76.01/32.59 76.01/32.59
/0\
\2/

Tuple symbols:
76.01/32.59
M( c5(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( f(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( c1(x1) ) = 76.01/32.59 76.01/32.59
/0\
\2/
+ 76.01/32.59 76.01/32.59
/12\
\00/
·x1

76.01/32.59
M( c2(x1) ) = 76.01/32.59 76.01/32.59
/2\
\0/
+ 76.01/32.59 76.01/32.59
/12\
\00/
·x1

76.01/32.59
M( c4(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( g(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( G(x1) ) = 76.01/32.59 76.01/32.59
/0\
\4/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( F(x1) ) = 76.01/32.59 76.01/32.59
/0\
\4/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
76.01/32.59
76.01/32.59

(38) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.59
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.59
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.59
g(nil) → nil 76.01/32.59
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.59
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2))))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.59
76.01/32.59

(39) CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]: 76.01/32.59
Non-tuple symbols:
76.01/32.59
M( f(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( g(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( .(x1, x2) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/11\
\00/
·x1+ 76.01/32.59 76.01/32.59
/10\
\00/
·x2

76.01/32.59
M( nil ) = 76.01/32.59 76.01/32.59
/0\
\1/

Tuple symbols:
76.01/32.59
M( c5(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( f(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( c1(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( c2(x1) ) = 76.01/32.59 76.01/32.59
/0\
\2/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( c4(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( g(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( G(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( F(x1) ) = 76.01/32.59 76.01/32.59
/0\
\4/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
76.01/32.59
76.01/32.59

(40) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.59
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.59
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.59
g(nil) → nil 76.01/32.59
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.59
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.59
76.01/32.59

(41) CdtMatrixRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
We considered the (Usable) Rules:none
And the Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
The order we found is given by the following interpretation:
Matrix interpretation [MATRO]: 76.01/32.59
Non-tuple symbols:
76.01/32.59
M( f(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( g(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( .(x1, x2) ) = 76.01/32.59 76.01/32.59
/1\
\4/
+ 76.01/32.59 76.01/32.59
/10\
\01/
·x1+ 76.01/32.59 76.01/32.59
/14\
\00/
·x2

76.01/32.59
M( nil ) = 76.01/32.59 76.01/32.59
/2\
\0/

Tuple symbols:
76.01/32.59
M( c5(x1) ) = 76.01/32.59 76.01/32.59
/0\
\1/
+ 76.01/32.59 76.01/32.59
/11\
\00/
·x1

76.01/32.59
M( f(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( c1(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( c2(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( c4(x1) ) = 76.01/32.59 76.01/32.59
/3\
\1/
+ 76.01/32.59 76.01/32.59
/10\
\00/
·x1

76.01/32.59
M( g(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1

76.01/32.59
M( G(x1) ) = 76.01/32.59 76.01/32.59
/1\
\1/
+ 76.01/32.59 76.01/32.59
/13\
\00/
·x1

76.01/32.59
M( F(x1) ) = 76.01/32.59 76.01/32.59
/0\
\0/
+ 76.01/32.59 76.01/32.59
/00\
\00/
·x1


Matrix type:
We used a basic matrix type which is not further parametrizeable.


As matrix orders are CE-compatible, we used usable rules w.r.t. argument filtering in the order.
76.01/32.59
76.01/32.59

(42) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(nil) → nil 76.01/32.59
f(.(nil, z0)) → .(nil, f(z0)) 76.01/32.59
f(.(.(z0, z1), z2)) → f(.(z0, .(z1, z2))) 76.01/32.59
g(nil) → nil 76.01/32.59
g(.(z0, nil)) → .(g(z0), nil) 76.01/32.59
g(.(z0, .(z1, z2))) → g(.(.(z0, z1), z2))
Tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
S tuples:none
K tuples:

F(.(nil, .(nil, .(nil, y0)))) → c1(F(.(nil, .(nil, y0)))) 76.01/32.59
F(.(nil, .(nil, .(.(y0, y1), y2)))) → c1(F(.(nil, .(.(y0, y1), y2)))) 76.01/32.59
F(.(nil, .(.(.(y0, y1), z1), z2))) → c1(F(.(.(.(y0, y1), z1), z2))) 76.01/32.59
F(.(nil, .(.(nil, nil), z2))) → c1(F(.(.(nil, nil), z2))) 76.01/32.59
F(.(nil, .(.(nil, .(y0, y1)), z2))) → c1(F(.(.(nil, .(y0, y1)), z2))) 76.01/32.59
G(.(.(.(y0, nil), nil), nil)) → c4(G(.(.(y0, nil), nil))) 76.01/32.59
G(.(.(.(y0, .(y1, y2)), nil), nil)) → c4(G(.(.(y0, .(y1, y2)), nil))) 76.01/32.59
G(.(.(z0, .(z1, .(y2, y3))), nil)) → c4(G(.(z0, .(z1, .(y2, y3))))) 76.01/32.59
G(.(.(z0, .(nil, nil)), nil)) → c4(G(.(z0, .(nil, nil)))) 76.01/32.59
G(.(.(z0, .(.(y1, y2), nil)), nil)) → c4(G(.(z0, .(.(y1, y2), nil)))) 76.01/32.59
F(.(.(nil, nil), .(nil, y0))) → c2(F(.(nil, .(nil, .(nil, y0))))) 76.01/32.59
F(.(.(nil, nil), .(.(y0, y1), y2))) → c2(F(.(nil, .(nil, .(.(y0, y1), y2))))) 76.01/32.59
F(.(.(.(.(y0, y1), z1), z2), z3)) → c2(F(.(.(.(y0, y1), z1), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, nil), z2), z3)) → c2(F(.(.(nil, nil), .(z2, z3)))) 76.01/32.59
F(.(.(.(nil, .(y0, y1)), z2), z3)) → c2(F(.(.(nil, .(y0, y1)), .(z2, z3)))) 76.01/32.59
F(.(.(nil, .(.(y0, y1), z1)), z2)) → c2(F(.(nil, .(.(.(y0, y1), z1), z2)))) 76.01/32.59
F(.(.(nil, .(nil, nil)), z2)) → c2(F(.(nil, .(.(nil, nil), z2)))) 76.01/32.59
F(.(.(nil, .(nil, .(y0, y1))), z2)) → c2(F(.(nil, .(.(nil, .(y0, y1)), z2)))) 76.01/32.59
G(.(.(y0, nil), .(nil, nil))) → c5(G(.(.(.(y0, nil), nil), nil))) 76.01/32.59
G(.(.(y0, .(y1, y2)), .(nil, nil))) → c5(G(.(.(.(y0, .(y1, y2)), nil), nil))) 76.01/32.59
G(.(z0, .(z1, .(z2, .(y2, y3))))) → c5(G(.(.(z0, z1), .(z2, .(y2, y3))))) 76.01/32.59
G(.(z0, .(z1, .(nil, nil)))) → c5(G(.(.(z0, z1), .(nil, nil)))) 76.01/32.59
G(.(z0, .(z1, .(.(y1, y2), nil)))) → c5(G(.(.(z0, z1), .(.(y1, y2), nil)))) 76.01/32.59
G(.(z0, .(.(z1, .(y2, y3)), nil))) → c5(G(.(.(z0, .(z1, .(y2, y3))), nil))) 76.01/32.59
G(.(z0, .(.(nil, nil), nil))) → c5(G(.(.(z0, .(nil, nil)), nil))) 76.01/32.59
G(.(z0, .(.(.(y1, y2), nil), nil))) → c5(G(.(.(z0, .(.(y1, y2), nil)), nil)))
Defined Rule Symbols:

f, g

Defined Pair Symbols:

F, G

Compound Symbols:

c1, c2, c4, c5

76.01/32.59
76.01/32.59

(43) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
76.01/32.59
76.01/32.59

(44) BOUNDS(O(1), O(1))

76.01/32.59
76.01/32.59
76.30/32.65 EOF