(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(0, b(0, x)) → b(0, a(0, x))
a(0, x) → b(0, b(0, x))
a(0, a(1, a(x, y))) → a(1, a(0, a(x, y)))
b(0, a(1, a(x, y))) → b(1, a(0, a(x, y)))
a(0, a(x, y)) → a(1, a(1, a(x, y)))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0))
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
S tuples:
A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0))
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(1, a(1, a(z0, z1))), A(1, a(z0, z1)), A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(B(1, a(0, a(z0, z1))), A(0, a(z0, z1)), A(z0, z1))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c, c1, c2, c3, c4
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 4 trailing tuple parts
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0))
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
S tuples:
A(0, b(0, z0)) → c(B(0, a(0, z0)), A(0, z0))
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c, c1, c2, c3, c4
(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
0,
b(
0,
z0)) →
c(
B(
0,
a(
0,
z0)),
A(
0,
z0)) by
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, x0)) → c
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, x0)) → c
S tuples:
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, x0)) → c
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c3, c4, c, c
(7) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
A(0, b(0, x0)) → c
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
S tuples:
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, z0)) → c(B(0, b(0, b(0, z0))), A(0, z0))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c3, c4, c
(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, z0)) → c(A(0, z0))
S tuples:
A(0, z0) → c1(B(0, b(0, z0)), B(0, z0))
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, z0)) → c(A(0, z0))
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c1, c2, c3, c4, c, c
(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)
Use narrowing to replace
A(
0,
z0) →
c1(
B(
0,
b(
0,
z0)),
B(
0,
z0)) by
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, x0) → c1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, z0)) → c(A(0, z0))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, x0) → c1
S tuples:
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, z0)) → c(A(0, z0))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
A(0, x0) → c1
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A, B
Compound Symbols:
c2, c3, c4, c, c, c1, c1
(13) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
A(0, a(1, a(z0, z1))) → c2(A(0, a(z0, z1)), A(z0, z1))
A(0, a(z0, z1)) → c3(A(z0, z1))
B(0, a(1, a(z0, z1))) → c4(A(0, a(z0, z1)), A(z0, z1))
A(0, b(0, b(0, z0))) → c(B(0, b(0, a(0, z0))), A(0, b(0, z0)))
A(0, b(0, a(z0, z1))) → c(B(0, a(1, a(1, a(z0, z1)))), A(0, a(z0, z1)))
A(0, b(0, z0)) → c(A(0, z0))
A(0, a(1, a(z0, z1))) → c1(B(0, b(1, a(0, a(z0, z1)))), B(0, a(1, a(z0, z1))))
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:
A(0, x0) → c1
S tuples:
A(0, x0) → c1
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:
A
Compound Symbols:
c1
(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
A(0, x0) → c1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(0, b(0, z0)) → b(0, a(0, z0))
a(0, z0) → b(0, b(0, z0))
a(0, a(1, a(z0, z1))) → a(1, a(0, a(z0, z1)))
a(0, a(z0, z1)) → a(1, a(1, a(z0, z1)))
b(0, a(1, a(z0, z1))) → b(1, a(0, a(z0, z1)))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
a, b
Defined Pair Symbols:none
Compound Symbols:none
(17) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(18) BOUNDS(O(1), O(1))