13.32/5.67
13.32/5.67
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(0) → 1
13.32/5.67
f(s(x)) → g(f(x))
13.32/5.67
g(x) → +(x, s(x))
13.32/5.67
f(s(x)) → +(f(x), s(f(x)))
Rewrite Strategy: INNERMOST
13.32/5.67
13.32/5.67
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
13.32/5.67
13.32/5.67
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.67
f(s(z0)) → g(f(z0))
13.32/5.67
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.67
g(z0) → +(z0, s(z0))
Tuples:
F(s(z0)) → c1(G(f(z0)), F(z0))
13.32/5.67
F(s(z0)) → c2(F(z0), F(z0))
S tuples:
F(s(z0)) → c1(G(f(z0)), F(z0))
13.32/5.67
F(s(z0)) → c2(F(z0), F(z0))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
13.32/5.67
13.32/5.67
(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
13.32/5.67
13.32/5.67
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.67
f(s(z0)) → g(f(z0))
13.32/5.67
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.67
g(z0) → +(z0, s(z0))
Tuples:
F(s(z0)) → c2(F(z0), F(z0))
13.32/5.67
F(s(z0)) → c1(F(z0))
S tuples:
F(s(z0)) → c2(F(z0), F(z0))
13.32/5.67
F(s(z0)) → c1(F(z0))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c2, c1
13.32/5.67
13.32/5.67
(5) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
z0)) →
c2(
F(
z0),
F(
z0)) by
F(s(s(y0))) → c2(F(s(y0)), F(s(y0)))
13.32/5.67
13.32/5.67
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.67
f(s(z0)) → g(f(z0))
13.32/5.67
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.67
g(z0) → +(z0, s(z0))
Tuples:
F(s(z0)) → c1(F(z0))
13.32/5.67
F(s(s(y0))) → c2(F(s(y0)), F(s(y0)))
S tuples:
F(s(z0)) → c1(F(z0))
13.32/5.67
F(s(s(y0))) → c2(F(s(y0)), F(s(y0)))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
13.32/5.67
13.32/5.67
(7) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
z0)) →
c1(
F(
z0)) by
F(s(s(y0))) → c1(F(s(y0)))
13.32/5.67
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.67
13.32/5.67
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.67
f(s(z0)) → g(f(z0))
13.32/5.67
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.67
g(z0) → +(z0, s(z0))
Tuples:
F(s(s(y0))) → c2(F(s(y0)), F(s(y0)))
13.32/5.67
F(s(s(y0))) → c1(F(s(y0)))
13.32/5.67
F(s(s(s(y0)))) → c1(F(s(s(y0))))
S tuples:
F(s(s(y0))) → c2(F(s(y0)), F(s(y0)))
13.32/5.67
F(s(s(y0))) → c1(F(s(y0)))
13.32/5.67
F(s(s(s(y0)))) → c1(F(s(s(y0))))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c2, c1
13.32/5.68
13.32/5.68
(9) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
s(
y0))) →
c2(
F(
s(
y0)),
F(
s(
y0))) by
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
13.32/5.68
13.32/5.68
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.68
f(s(z0)) → g(f(z0))
13.32/5.68
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.68
g(z0) → +(z0, s(z0))
Tuples:
F(s(s(y0))) → c1(F(s(y0)))
13.32/5.68
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.68
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
S tuples:
F(s(s(y0))) → c1(F(s(y0)))
13.32/5.68
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.68
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
13.32/5.68
13.32/5.68
(11) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
s(
y0))) →
c1(
F(
s(
y0))) by
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c1(F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(s(y0)))))) → c1(F(s(s(s(s(y0))))))
13.32/5.68
13.32/5.68
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.68
f(s(z0)) → g(f(z0))
13.32/5.68
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.68
g(z0) → +(z0, s(z0))
Tuples:
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.68
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(y0))))) → c1(F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(s(y0)))))) → c1(F(s(s(s(s(y0))))))
S tuples:
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.68
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(y0))))) → c1(F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(s(y0)))))) → c1(F(s(s(s(s(y0))))))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
13.32/5.68
13.32/5.68
(13) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use forward instantiation to replace
F(
s(
s(
s(
y0)))) →
c1(
F(
s(
s(
y0)))) by
F(s(s(s(s(y0))))) → c1(F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(s(y0)))))) → c1(F(s(s(s(s(y0))))))
13.32/5.68
F(s(s(s(s(s(s(y0))))))) → c1(F(s(s(s(s(s(y0)))))))
13.32/5.68
13.32/5.68
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(0) → 1
13.32/5.68
f(s(z0)) → g(f(z0))
13.32/5.68
f(s(z0)) → +(f(z0), s(f(z0)))
13.32/5.68
g(z0) → +(z0, s(z0))
Tuples:
F(s(s(s(y0)))) → c1(F(s(s(y0))))
13.32/5.68
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(y0))))) → c1(F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(s(y0)))))) → c1(F(s(s(s(s(y0))))))
13.32/5.68
F(s(s(s(s(s(s(y0))))))) → c1(F(s(s(s(s(s(y0)))))))
S tuples:
F(s(s(s(y0)))) → c2(F(s(s(y0))), F(s(s(y0))))
13.32/5.68
F(s(s(s(s(y0))))) → c2(F(s(s(s(y0)))), F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(y0))))) → c1(F(s(s(s(y0)))))
13.32/5.68
F(s(s(s(s(s(y0)))))) → c1(F(s(s(s(s(y0))))))
13.32/5.68
F(s(s(s(s(s(s(y0))))))) → c1(F(s(s(s(s(s(y0)))))))
K tuples:none
Defined Rule Symbols:
f, g
Defined Pair Symbols:
F
Compound Symbols:
c1, c2
13.32/5.68