(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(x, y), z) → +(x, +(y, z))
+(p1, +(p1, x)) → +(p2, x)
+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, x)) → +(p1, +(p2, x))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p5, +(p5, x)) → +(p10, x)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, x)) → +(p1, +(p10, x))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, x)) → +(p5, +(p10, x))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:
+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, p1) → c6(+'(p1, p2))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, p2)) → c8(+'(p1, p5))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p1) → c10(+'(p1, p5))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p2) → c12(+'(p2, p5))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, p1) → c15(+'(p1, p10))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, p5) → c19(+'(p5, p10))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
S tuples:
+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, p1) → c6(+'(p1, p2))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, p2)) → c8(+'(p1, p5))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p1) → c10(+'(p1, p5))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p2) → c12(+'(p2, p5))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, p1) → c15(+'(p1, p10))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, p5) → c19(+'(p5, p10))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
K tuples:none
Defined Rule Symbols:
+
Defined Pair Symbols:
+'
Compound Symbols:
c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, p2)) → c8(+'(p1, p5))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:
+'(p2, p1) → c6(+'(p1, p2))
+'(p5, p1) → c10(+'(p1, p5))
+'(p5, p2) → c12(+'(p2, p5))
+'(p10, p1) → c15(+'(p1, p10))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, p5) → c19(+'(p5, p10))
S tuples:
+'(p2, p1) → c6(+'(p1, p2))
+'(p5, p1) → c10(+'(p1, p5))
+'(p5, p2) → c12(+'(p2, p5))
+'(p10, p1) → c15(+'(p1, p10))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, p5) → c19(+'(p5, p10))
K tuples:none
Defined Rule Symbols:
+
Defined Pair Symbols:
+'
Compound Symbols:
c6, c10, c12, c15, c17, c19
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 6 trailing nodes:
+'(p2, p1) → c6(+'(p1, p2))
+'(p5, p1) → c10(+'(p1, p5))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, p5) → c19(+'(p5, p10))
+'(p5, p2) → c12(+'(p2, p5))
+'(p10, p1) → c15(+'(p1, p10))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
+
Defined Pair Symbols:none
Compound Symbols:none
(7) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(8) BOUNDS(O(1), O(1))