20.28/9.31
20.28/9.31
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
+(+(x, y), z) → +(x, +(y, z))
20.28/9.31
+(f(x), f(y)) → f(+(x, y))
20.28/9.31
+(f(x), +(f(y), z)) → +(f(+(x, y)), z)
Rewrite Strategy: INNERMOST
20.28/9.31
20.28/9.31
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
20.28/9.31
20.28/9.31
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(+(z0, z1), z2) → +(z0, +(z1, z2))
20.28/9.31
+(f(z0), f(z1)) → f(+(z0, z1))
20.28/9.31
+(f(z0), +(f(z1), z2)) → +(f(+(z0, z1)), z2)
Tuples:
+'(+(z0, z1), z2) → c(+'(z0, +(z1, z2)), +'(z1, z2))
20.28/9.31
+'(f(z0), f(z1)) → c1(+'(z0, z1))
20.28/9.31
+'(f(z0), +(f(z1), z2)) → c2(+'(f(+(z0, z1)), z2), +'(z0, z1))
S tuples:
+'(+(z0, z1), z2) → c(+'(z0, +(z1, z2)), +'(z1, z2))
20.28/9.31
+'(f(z0), f(z1)) → c1(+'(z0, z1))
20.28/9.31
+'(f(z0), +(f(z1), z2)) → c2(+'(f(+(z0, z1)), z2), +'(z0, z1))
K tuples:none
Defined Rule Symbols:
+
Defined Pair Symbols:
+'
Compound Symbols:
c, c1, c2
20.28/9.31
20.28/9.31
(3) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
+'(
f(
z0),
f(
z1)) →
c1(
+'(
z0,
z1)) by
+'(f(+(y0, y1)), f(z1)) → c1(+'(+(y0, y1), z1))
20.28/9.32
+'(f(f(y0)), f(f(y1))) → c1(+'(f(y0), f(y1)))
20.28/9.32
+'(f(f(y0)), f(+(f(y1), y2))) → c1(+'(f(y0), +(f(y1), y2)))
20.28/9.32
20.28/9.32
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(+(z0, z1), z2) → +(z0, +(z1, z2))
20.28/9.32
+(f(z0), f(z1)) → f(+(z0, z1))
20.28/9.32
+(f(z0), +(f(z1), z2)) → +(f(+(z0, z1)), z2)
Tuples:
+'(+(z0, z1), z2) → c(+'(z0, +(z1, z2)), +'(z1, z2))
20.28/9.32
+'(f(z0), +(f(z1), z2)) → c2(+'(f(+(z0, z1)), z2), +'(z0, z1))
20.28/9.32
+'(f(+(y0, y1)), f(z1)) → c1(+'(+(y0, y1), z1))
20.28/9.32
+'(f(f(y0)), f(f(y1))) → c1(+'(f(y0), f(y1)))
20.28/9.32
+'(f(f(y0)), f(+(f(y1), y2))) → c1(+'(f(y0), +(f(y1), y2)))
S tuples:
+'(+(z0, z1), z2) → c(+'(z0, +(z1, z2)), +'(z1, z2))
20.28/9.32
+'(f(z0), +(f(z1), z2)) → c2(+'(f(+(z0, z1)), z2), +'(z0, z1))
20.28/9.32
+'(f(+(y0, y1)), f(z1)) → c1(+'(+(y0, y1), z1))
20.28/9.32
+'(f(f(y0)), f(f(y1))) → c1(+'(f(y0), f(y1)))
20.28/9.32
+'(f(f(y0)), f(+(f(y1), y2))) → c1(+'(f(y0), +(f(y1), y2)))
K tuples:none
Defined Rule Symbols:
+
Defined Pair Symbols:
+'
Compound Symbols:
c, c2, c1
20.28/9.32
20.28/9.32
(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
+'(
f(
f(
y0)),
f(
f(
y1))) →
c1(
+'(
f(
y0),
f(
y1))) by
+'(f(f(+(y0, y1))), f(f(z1))) → c1(+'(f(+(y0, y1)), f(z1)))
20.28/9.32
+'(f(f(f(y0))), f(f(f(y1)))) → c1(+'(f(f(y0)), f(f(y1))))
20.28/9.32
+'(f(f(f(y0))), f(f(+(f(y1), y2)))) → c1(+'(f(f(y0)), f(+(f(y1), y2))))
20.28/9.32
20.28/9.32
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(+(z0, z1), z2) → +(z0, +(z1, z2))
20.28/9.32
+(f(z0), f(z1)) → f(+(z0, z1))
20.28/9.32
+(f(z0), +(f(z1), z2)) → +(f(+(z0, z1)), z2)
Tuples:
+'(+(z0, z1), z2) → c(+'(z0, +(z1, z2)), +'(z1, z2))
20.28/9.32
+'(f(z0), +(f(z1), z2)) → c2(+'(f(+(z0, z1)), z2), +'(z0, z1))
20.28/9.32
+'(f(+(y0, y1)), f(z1)) → c1(+'(+(y0, y1), z1))
20.28/9.32
+'(f(f(y0)), f(+(f(y1), y2))) → c1(+'(f(y0), +(f(y1), y2)))
20.28/9.32
+'(f(f(+(y0, y1))), f(f(z1))) → c1(+'(f(+(y0, y1)), f(z1)))
20.28/9.32
+'(f(f(f(y0))), f(f(f(y1)))) → c1(+'(f(f(y0)), f(f(y1))))
20.28/9.32
+'(f(f(f(y0))), f(f(+(f(y1), y2)))) → c1(+'(f(f(y0)), f(+(f(y1), y2))))
S tuples:
+'(+(z0, z1), z2) → c(+'(z0, +(z1, z2)), +'(z1, z2))
20.28/9.32
+'(f(z0), +(f(z1), z2)) → c2(+'(f(+(z0, z1)), z2), +'(z0, z1))
20.28/9.32
+'(f(+(y0, y1)), f(z1)) → c1(+'(+(y0, y1), z1))
20.28/9.32
+'(f(f(y0)), f(+(f(y1), y2))) → c1(+'(f(y0), +(f(y1), y2)))
20.28/9.32
+'(f(f(+(y0, y1))), f(f(z1))) → c1(+'(f(+(y0, y1)), f(z1)))
20.28/9.32
+'(f(f(f(y0))), f(f(f(y1)))) → c1(+'(f(f(y0)), f(f(y1))))
20.28/9.32
+'(f(f(f(y0))), f(f(+(f(y1), y2)))) → c1(+'(f(f(y0)), f(+(f(y1), y2))))
K tuples:none
Defined Rule Symbols:
+
Defined Pair Symbols:
+'
Compound Symbols:
c, c2, c1
20.28/9.32