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:
M( f(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( g(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( .(x1, x2) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 1 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 | + | / | 1 | 1 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x2 |
76.01/32.58
M( nil ) = | / | 0 | \ |
76.01/32.58 \ | 4 | / |
76.01/32.58
|
76.01/32.58
Tuple symbols:
M( c5(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 1 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( f(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( c1(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 1 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( c2(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 1 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( c4(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 1 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( g(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( G(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( F(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 1 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
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:
M( f(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.58 \ | 0 | 0 | / |
76.01/32.58
| · | x1 |
76.01/32.58
M( g(x1) ) = | / | 0 | \ |
76.01/32.58 \ | 0 | / |
76.01/32.58
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( .(x1, x2) ) = | / | 0 | \ |
76.01/32.59 \ | 4 | / |
76.01/32.59
| + | / | 1 | 4 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 | + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 1 | / |
76.01/32.59
| · | x2 |
76.01/32.59
M( nil ) = | / | 0 | \ |
76.01/32.59 \ | 2 | / |
76.01/32.59
|
76.01/32.59
Tuple symbols:
M( c5(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( f(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c1(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 2 | / |
76.01/32.59
| + | / | 1 | 2 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c2(x1) ) = | / | 2 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 2 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c4(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( g(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( G(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 4 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( F(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 4 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
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:
M( f(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( g(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( .(x1, x2) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 1 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 | + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x2 |
76.01/32.59
M( nil ) = | / | 0 | \ |
76.01/32.59 \ | 1 | / |
76.01/32.59
|
76.01/32.59
Tuple symbols:
M( c5(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( f(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c1(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c2(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 2 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c4(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( g(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( G(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( F(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 4 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
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:
M( f(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( g(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( .(x1, x2) ) = | / | 1 | \ |
76.01/32.59 \ | 4 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 1 | / |
76.01/32.59
| · | x1 | + | / | 1 | 4 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x2 |
76.01/32.59
M( nil ) = | / | 2 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
|
76.01/32.59
Tuple symbols:
M( c5(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 1 | / |
76.01/32.59
| + | / | 1 | 1 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( f(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c1(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c2(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( c4(x1) ) = | / | 3 | \ |
76.01/32.59 \ | 1 | / |
76.01/32.59
| + | / | 1 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( g(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( G(x1) ) = | / | 1 | \ |
76.01/32.59 \ | 1 | / |
76.01/32.59
| + | / | 1 | 3 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
M( F(x1) ) = | / | 0 | \ |
76.01/32.59 \ | 0 | / |
76.01/32.59
| + | / | 0 | 0 | \ |
76.01/32.59 \ | 0 | 0 | / |
76.01/32.59
| · | x1 |
76.01/32.59
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