(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(f, a(f, x)) → a(x, g)
a(x, g) → a(f, a(g, a(f, x)))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, z0)) → a(z0, g)
a(z0, g) → a(f, a(g, a(f, z0)))
Tuples:
A(f, a(f, z0)) → c(A(z0, g))
A(z0, g) → c1(A(f, a(g, a(f, z0))), A(g, a(f, z0)), A(f, z0))
S tuples:
A(f, a(f, z0)) → c(A(z0, g))
A(z0, g) → c1(A(f, a(g, a(f, z0))), A(g, a(f, z0)), A(f, z0))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c1
(3) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
z0,
g) →
c1(
A(
f,
a(
g,
a(
f,
z0))),
A(
g,
a(
f,
z0)),
A(
f,
z0)) by
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
A(a(f, z0), g) → c1(A(f, a(g, a(z0, g))), A(g, a(f, a(f, z0))), A(f, a(f, z0)))
A(x0, g) → c1
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, z0)) → a(z0, g)
a(z0, g) → a(f, a(g, a(f, z0)))
Tuples:
A(f, a(f, z0)) → c(A(z0, g))
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
A(a(f, z0), g) → c1(A(f, a(g, a(z0, g))), A(g, a(f, a(f, z0))), A(f, a(f, z0)))
A(x0, g) → c1
S tuples:
A(f, a(f, z0)) → c(A(z0, g))
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
A(a(f, z0), g) → c1(A(f, a(g, a(z0, g))), A(g, a(f, a(f, z0))), A(f, a(f, z0)))
A(x0, g) → c1
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c, c1, c1
(5) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
A(f, a(f, z0)) → c(A(z0, g))
A(a(f, z0), g) → c1(A(f, a(g, a(z0, g))), A(g, a(f, a(f, z0))), A(f, a(f, z0)))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, z0)) → a(z0, g)
a(z0, g) → a(f, a(g, a(f, z0)))
Tuples:
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
A(x0, g) → c1
S tuples:
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
A(x0, g) → c1
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c1, c1
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
A(x0, g) → c1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, z0)) → a(z0, g)
a(z0, g) → a(f, a(g, a(f, z0)))
Tuples:
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
S tuples:
A(g, g) → c1(A(f, a(g, a(f, a(g, a(f, f))))), A(g, a(f, g)), A(f, g))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c1
(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing tuple parts
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, z0)) → a(z0, g)
a(z0, g) → a(f, a(g, a(f, z0)))
Tuples:
A(g, g) → c1(A(g, a(f, g)))
S tuples:
A(g, g) → c1(A(g, a(f, g)))
K tuples:none
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c1
(11) 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.
A(g, g) → c1(A(g, a(f, g)))
We considered the (Usable) Rules:
a(z0, g) → a(f, a(g, a(f, z0)))
a(f, a(f, z0)) → a(z0, g)
And the Tuples:
A(g, g) → c1(A(g, a(f, g)))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(A(x1, x2)) = [4]x2
POL(a(x1, x2)) = 0
POL(c1(x1)) = x1
POL(f) = [3]
POL(g) = [4]
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(f, a(f, z0)) → a(z0, g)
a(z0, g) → a(f, a(g, a(f, z0)))
Tuples:
A(g, g) → c1(A(g, a(f, g)))
S tuples:none
K tuples:
A(g, g) → c1(A(g, a(f, g)))
Defined Rule Symbols:
a
Defined Pair Symbols:
A
Compound Symbols:
c1
(13) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(14) BOUNDS(O(1), O(1))