572.43/242.65 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml

572.43/242.65

572.43/242.65
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS

572.43/242.65

↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳2 CdtProblem

572.43/242.65

↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳4 CdtProblem

572.43/242.65

↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳6 CdtProblem

572.43/242.65

↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳8 CdtProblem

572.43/242.65

↳9 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳10 CdtProblem

572.43/242.65

↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳12 CdtProblem

572.43/242.65

↳13 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳14 CdtProblem

572.43/242.65

↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳16 CdtProblem

572.43/242.65

↳17 CdtRewritingProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳18 CdtProblem

572.43/242.65

↳19 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳20 CdtProblem

572.43/242.65

↳21 CdtRewritingProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳22 CdtProblem

572.43/242.65

↳23 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳24 CdtProblem

572.43/242.65

↳25 CdtRewritingProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳26 CdtProblem

572.43/242.65

↳27 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳28 CdtProblem

572.43/242.65

↳29 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳30 CdtProblem

572.43/242.65

↳31 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳32 CdtProblem

572.43/242.65

↳33 CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳34 CdtProblem

572.43/242.65

↳35 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))

572.43/242.65

↳36 CdtProblem

572.43/242.65

572.43/242.65 572.43/242.65

572.43/242.65

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(s(x)) → s(f(f(p(s(x))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(x)) → x

Rewrite Strategy: INNERMOST

572.43/242.65

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

572.43/242.65

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(z0)) → c(F(f(p(s(z0)))), F(p(s(z0))), P(s(z0)))

S tuples:

F(s(z0)) → c(F(f(p(s(z0)))), F(p(s(z0))), P(s(z0)))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c

572.43/242.65

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

572.43/242.65

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(z0)) → c(F(f(p(s(z0)))), F(p(s(z0))))

S tuples:

F(s(z0)) → c(F(f(p(s(z0)))), F(p(s(z0))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c

572.43/242.65

(5) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(s(z0)) → c(F(f(p(s(z0)))), F(p(s(z0)))) by

F(s(z0)) → c(F(f(z0)), F(p(s(z0))))

572.43/242.65

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(z0)) → c(F(f(z0)), F(p(s(z0))))

S tuples:

F(s(z0)) → c(F(f(z0)), F(p(s(z0))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c

572.43/242.65

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(s(z0)) → c(F(f(z0)), F(p(s(z0)))) by

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(0)) → c(F(0), F(p(s(0)))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0))))

572.43/242.65

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(0)) → c(F(0), F(p(s(0)))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0))))

S tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(0)) → c(F(0), F(p(s(0)))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c

572.43/242.65

(9) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

572.43/242.65

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c(F(p(s(0))))

S tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c(F(p(s(0))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c

572.43/242.65

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace F(s(0)) → c(F(p(s(0)))) by

F(s(0)) → c(F(0))

572.43/242.65

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c(F(0))

S tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c(F(0))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c

572.43/242.65

(13) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing tuple parts

572.43/242.65

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c

S tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.65

(15) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(s(0)) → c

572.43/242.65

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c

S tuples:

F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) 572.43/242.65
F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.65

(17) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(p(s(s(z0))))) by F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0)))

572.43/242.65

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c 572.43/242.65
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0)))

S tuples:

F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c 572.43/242.65
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0)))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.65

(19) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(s(0)) → c

572.43/242.65

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c 572.43/242.65
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0)))

S tuples:

F(s(x0)) → c(F(p(s(x0)))) 572.43/242.65
F(s(0)) → c 572.43/242.65
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0)))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.65

(21) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace F(s(x0)) → c(F(p(s(x0)))) by F(s(z0)) → c(F(z0))

572.43/242.65

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.65
f(0) → 0 572.43/242.65
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.65
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0))) 572.43/242.66
F(s(z0)) → c(F(z0))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0))) 572.43/242.66
F(s(z0)) → c(F(z0))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(23) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(s(0)) → c

572.43/242.66

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0))) 572.43/242.66
F(s(z0)) → c(F(z0))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0))) 572.43/242.66
F(s(z0)) → c(F(z0))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(25) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace F(s(s(z0))) → c(F(s(f(f(p(s(z0)))))), F(s(z0))) by F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0)))

572.43/242.66

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(z0)) → c(F(z0)) 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0)))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(z0)) → c(F(z0)) 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0)))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(27) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

F(s(0)) → c

572.43/242.66

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(z0)) → c(F(z0)) 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0)))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(z0)) → c(F(z0)) 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0)))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(29) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(s(z0)) → c(F(z0)) by

F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(y0))) → c(F(s(y0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0))))

572.43/242.66

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(y0))) → c(F(s(y0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0))))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(y0))) → c(F(s(y0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(31) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

F(s(0)) → c 572.43/242.66
F(s(s(0))) → c(F(s(0)))

572.43/242.66

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(y0))) → c(F(s(y0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0))))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(y0))) → c(F(s(y0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(33) CdtForwardInstantiationProof (BOTH BOUNDS(ID, ID) transformation)

Use forward instantiation to replace F(s(s(y0))) → c(F(s(y0))) by

F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0)))) 572.43/242.66
F(s(s(s(0)))) → c(F(s(s(0)))) 572.43/242.66
F(s(s(s(s(y0))))) → c(F(s(s(s(y0)))))

572.43/242.66

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0)))) 572.43/242.66
F(s(s(s(0)))) → c(F(s(s(0)))) 572.43/242.66
F(s(s(s(s(y0))))) → c(F(s(s(s(y0)))))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0)))) 572.43/242.66
F(s(s(s(0)))) → c(F(s(s(0)))) 572.43/242.66
F(s(s(s(s(y0))))) → c(F(s(s(s(y0)))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66

(35) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

F(s(0)) → c 572.43/242.66
F(s(s(0))) → c(F(s(0)))

572.43/242.66

(36) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(s(z0)) → s(f(f(p(s(z0))))) 572.43/242.66
f(0) → 0 572.43/242.66
p(s(z0)) → z0

Tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0)))) 572.43/242.66
F(s(s(s(0)))) → c(F(s(s(0)))) 572.43/242.66
F(s(s(s(s(y0))))) → c(F(s(s(s(y0)))))

S tuples:

F(s(0)) → c 572.43/242.66
F(s(s(z0))) → c(F(s(f(f(z0)))), F(s(z0))) 572.43/242.66
F(s(s(0))) → c(F(s(0))) 572.43/242.66
F(s(s(s(y0)))) → c(F(s(s(y0)))) 572.43/242.66
F(s(s(s(0)))) → c(F(s(s(0)))) 572.43/242.66
F(s(s(s(s(y0))))) → c(F(s(s(s(y0)))))

K tuples:none
Defined Rule Symbols:

f, p

Defined Pair Symbols:

F

Compound Symbols:

c, c, c

572.43/242.66