24.05/22.03
24.05/22.03
(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
f(x) → f(g(x))
Rewrite Strategy: INNERMOST
24.05/22.03
24.05/22.03
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
24.05/22.03
24.05/22.03
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → f(g(z0))
Tuples:
F(z0) → c(F(g(z0)))
S tuples:
F(z0) → c(F(g(z0)))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c
24.05/22.03
24.05/22.03
(3) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
z0) →
c(
F(
g(
z0))) by
F(g(x0)) → c(F(g(g(x0))))
24.05/22.03
24.05/22.03
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → f(g(z0))
Tuples:
F(g(x0)) → c(F(g(g(x0))))
S tuples:
F(g(x0)) → c(F(g(g(x0))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c
24.05/22.03
24.05/22.03
(5) CdtInstantiationProof (BOTH BOUNDS(ID, ID) transformation)
Use instantiation to replace
F(
g(
x0)) →
c(
F(
g(
g(
x0)))) by
F(g(g(x0))) → c(F(g(g(g(x0)))))
24.05/22.03
24.05/22.03
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
f(z0) → f(g(z0))
Tuples:
F(g(g(x0))) → c(F(g(g(g(x0)))))
S tuples:
F(g(g(x0))) → c(F(g(g(g(x0)))))
K tuples:none
Defined Rule Symbols:
f
Defined Pair Symbols:
F
Compound Symbols:
c
24.05/22.03