(0) Obligation:
The Runtime Complexity (innermost) of the given
CpxTRS could be proven to be
BOUNDS(1, n^1).
The TRS R consists of the following rules:
dbl(S(0), S(0)) → S(S(S(S(0))))
save(S(x)) → dbl(0, save(x))
save(0) → 0
dbl(0, y) → y
Rewrite Strategy: INNERMOST
(1) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)
A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.
The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1, 2]
transitions:
S0(0) → 0
00() → 0
dbl0(0, 0) → 1
save0(0) → 2
01() → 5
S1(5) → 4
S1(4) → 3
S1(3) → 3
S1(3) → 1
01() → 6
save1(0) → 7
dbl1(6, 7) → 2
01() → 2
dbl1(6, 7) → 7
01() → 7
0 → 1
7 → 2
(2) BOUNDS(1, n^1)
(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted Cpx (relative) TRS to CDT
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
dbl(S(0), S(0)) → S(S(S(S(0))))
dbl(0, z0) → z0
save(S(z0)) → dbl(0, save(z0))
save(0) → 0
Tuples:
DBL(S(0), S(0)) → c
DBL(0, z0) → c1
SAVE(S(z0)) → c2(DBL(0, save(z0)), SAVE(z0))
SAVE(0) → c3
S tuples:
DBL(S(0), S(0)) → c
DBL(0, z0) → c1
SAVE(S(z0)) → c2(DBL(0, save(z0)), SAVE(z0))
SAVE(0) → c3
K tuples:none
Defined Rule Symbols:
dbl, save
Defined Pair Symbols:
DBL, SAVE
Compound Symbols:
c, c1, c2, c3
(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 3 trailing nodes:
SAVE(0) → c3
DBL(0, z0) → c1
DBL(S(0), S(0)) → c
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
dbl(S(0), S(0)) → S(S(S(S(0))))
dbl(0, z0) → z0
save(S(z0)) → dbl(0, save(z0))
save(0) → 0
Tuples:
SAVE(S(z0)) → c2(DBL(0, save(z0)), SAVE(z0))
S tuples:
SAVE(S(z0)) → c2(DBL(0, save(z0)), SAVE(z0))
K tuples:none
Defined Rule Symbols:
dbl, save
Defined Pair Symbols:
SAVE
Compound Symbols:
c2
(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
dbl(S(0), S(0)) → S(S(S(S(0))))
dbl(0, z0) → z0
save(S(z0)) → dbl(0, save(z0))
save(0) → 0
Tuples:
SAVE(S(z0)) → c2(SAVE(z0))
S tuples:
SAVE(S(z0)) → c2(SAVE(z0))
K tuples:none
Defined Rule Symbols:
dbl, save
Defined Pair Symbols:
SAVE
Compound Symbols:
c2
(9) CdtUsableRulesProof (EQUIVALENT transformation)
The following rules are not usable and were removed:
dbl(S(0), S(0)) → S(S(S(S(0))))
dbl(0, z0) → z0
save(S(z0)) → dbl(0, save(z0))
save(0) → 0
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
SAVE(S(z0)) → c2(SAVE(z0))
S tuples:
SAVE(S(z0)) → c2(SAVE(z0))
K tuples:none
Defined Rule Symbols:none
Defined Pair Symbols:
SAVE
Compound Symbols:
c2
(11) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
SAVE(S(z0)) → c2(SAVE(z0))
We considered the (Usable) Rules:none
And the Tuples:
SAVE(S(z0)) → c2(SAVE(z0))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(S(x1)) = [1] + x1
POL(SAVE(x1)) = x1
POL(c2(x1)) = x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:none
Tuples:
SAVE(S(z0)) → c2(SAVE(z0))
S tuples:none
K tuples:
SAVE(S(z0)) → c2(SAVE(z0))
Defined Rule Symbols:none
Defined Pair Symbols:
SAVE
Compound Symbols:
c2
(13) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)
The set S is empty
(14) BOUNDS(1, 1)