(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
a(h, h, h, x) → s(x)
a(l, x, s(y), h) → a(l, x, y, s(h))
a(l, x, s(y), s(z)) → a(l, x, y, a(l, x, s(y), z))
a(l, s(x), h, z) → a(l, x, z, z)
a(s(l), h, h, z) → a(l, z, h, z)
+(x, h) → x
+(h, x) → x
+(s(x), s(y)) → s(s(+(x, y)))
+(+(x, y), z) → +(x, +(y, z))
s(h) → 1
*(h, x) → h
*(x, h) → h
*(s(x), s(y)) → s(+(+(*(x, y), x), y))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(h, h, h, z0) → s(z0)
a(z0, z1, s(z2), h) → a(z0, z1, z2, s(h))
a(z0, z1, s(z2), s(z3)) → a(z0, z1, z2, a(z0, z1, s(z2), z3))
a(z0, s(z1), h, z2) → a(z0, z1, z2, z2)
a(s(z0), h, h, z1) → a(z0, z1, h, z1)
+(z0, h) → z0
+(h, z0) → z0
+(s(z0), s(z1)) → s(s(+(z0, z1)))
+(+(z0, z1), z2) → +(z0, +(z1, z2))
s(h) → 1
*(h, z0) → h
*(z0, h) → h
*(s(z0), s(z1)) → s(+(+(*(z0, z1), z0), z1))
Tuples:
A(h, h, h, z0) → c(S(z0))
A(z0, z1, s(z2), h) → c1(A(z0, z1, z2, s(h)), S(h))
A(z0, z1, s(z2), s(z3)) → c2(A(z0, z1, z2, a(z0, z1, s(z2), z3)), A(z0, z1, s(z2), z3), S(z2))
A(z0, s(z1), h, z2) → c3(A(z0, z1, z2, z2))
A(s(z0), h, h, z1) → c4(A(z0, z1, h, z1))
+'(s(z0), s(z1)) → c7(S(s(+(z0, z1))), S(+(z0, z1)), +'(z0, z1))
+'(+(z0, z1), z2) → c8(+'(z0, +(z1, z2)), +'(z1, z2))
*'(s(z0), s(z1)) → c12(S(+(+(*(z0, z1), z0), z1)), +'(+(*(z0, z1), z0), z1), +'(*(z0, z1), z0), *'(z0, z1))
S tuples:
A(h, h, h, z0) → c(S(z0))
A(z0, z1, s(z2), h) → c1(A(z0, z1, z2, s(h)), S(h))
A(z0, z1, s(z2), s(z3)) → c2(A(z0, z1, z2, a(z0, z1, s(z2), z3)), A(z0, z1, s(z2), z3), S(z2))
A(z0, s(z1), h, z2) → c3(A(z0, z1, z2, z2))
A(s(z0), h, h, z1) → c4(A(z0, z1, h, z1))
+'(s(z0), s(z1)) → c7(S(s(+(z0, z1))), S(+(z0, z1)), +'(z0, z1))
+'(+(z0, z1), z2) → c8(+'(z0, +(z1, z2)), +'(z1, z2))
*'(s(z0), s(z1)) → c12(S(+(+(*(z0, z1), z0), z1)), +'(+(*(z0, z1), z0), z1), +'(*(z0, z1), z0), *'(z0, z1))
K tuples:none
Defined Rule Symbols:
a, +, s, *
Defined Pair Symbols:
A, +', *'
Compound Symbols:
c, c1, c2, c3, c4, c7, c8, c12
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
A(z0, z1, s(z2), h) → c1(A(z0, z1, z2, s(h)), S(h))
A(z0, z1, s(z2), s(z3)) → c2(A(z0, z1, z2, a(z0, z1, s(z2), z3)), A(z0, z1, s(z2), z3), S(z2))
A(z0, s(z1), h, z2) → c3(A(z0, z1, z2, z2))
A(s(z0), h, h, z1) → c4(A(z0, z1, h, z1))
+'(s(z0), s(z1)) → c7(S(s(+(z0, z1))), S(+(z0, z1)), +'(z0, z1))
+'(+(z0, z1), z2) → c8(+'(z0, +(z1, z2)), +'(z1, z2))
*'(s(z0), s(z1)) → c12(S(+(+(*(z0, z1), z0), z1)), +'(+(*(z0, z1), z0), z1), +'(*(z0, z1), z0), *'(z0, z1))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(h, h, h, z0) → s(z0)
a(z0, z1, s(z2), h) → a(z0, z1, z2, s(h))
a(z0, z1, s(z2), s(z3)) → a(z0, z1, z2, a(z0, z1, s(z2), z3))
a(z0, s(z1), h, z2) → a(z0, z1, z2, z2)
a(s(z0), h, h, z1) → a(z0, z1, h, z1)
+(z0, h) → z0
+(h, z0) → z0
+(s(z0), s(z1)) → s(s(+(z0, z1)))
+(+(z0, z1), z2) → +(z0, +(z1, z2))
s(h) → 1
*(h, z0) → h
*(z0, h) → h
*(s(z0), s(z1)) → s(+(+(*(z0, z1), z0), z1))
Tuples:
A(h, h, h, z0) → c(S(z0))
S tuples:
A(h, h, h, z0) → c(S(z0))
K tuples:none
Defined Rule Symbols:
a, +, s, *
Defined Pair Symbols:
A
Compound Symbols:
c
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing nodes:
A(h, h, h, z0) → c(S(z0))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
a(h, h, h, z0) → s(z0)
a(z0, z1, s(z2), h) → a(z0, z1, z2, s(h))
a(z0, z1, s(z2), s(z3)) → a(z0, z1, z2, a(z0, z1, s(z2), z3))
a(z0, s(z1), h, z2) → a(z0, z1, z2, z2)
a(s(z0), h, h, z1) → a(z0, z1, h, z1)
+(z0, h) → z0
+(h, z0) → z0
+(s(z0), s(z1)) → s(s(+(z0, z1)))
+(+(z0, z1), z2) → +(z0, +(z1, z2))
s(h) → 1
*(h, z0) → h
*(z0, h) → h
*(s(z0), s(z1)) → s(+(+(*(z0, z1), z0), z1))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
a, +, s, *
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))