* Step 1: Sum WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
f(f(x)) -> f(c(f(x)))
f(f(x)) -> f(d(f(x)))
g(c(x)) -> x
g(c(0())) -> g(d(1()))
g(c(1())) -> g(d(0()))
g(d(x)) -> x
- Signature:
{f/1,g/1} / {0/0,1/0,c/1,d/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,c,d}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
f(f(x)) -> f(c(f(x)))
f(f(x)) -> f(d(f(x)))
g(c(x)) -> x
g(c(0())) -> g(d(1()))
g(c(1())) -> g(d(0()))
g(d(x)) -> x
- Signature:
{f/1,g/1} / {0/0,1/0,c/1,d/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {f,g} and constructors {0,1,c,d}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
f#(f(x)) -> c_1(f#(c(f(x))),f#(x))
f#(f(x)) -> c_2(f#(d(f(x))),f#(x))
g#(c(x)) -> c_3()
g#(c(0())) -> c_4(g#(d(1())))
g#(c(1())) -> c_5(g#(d(0())))
g#(d(x)) -> c_6()
Weak DPs
and mark the set of starting terms.
* Step 3: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
f#(f(x)) -> c_1(f#(c(f(x))),f#(x))
f#(f(x)) -> c_2(f#(d(f(x))),f#(x))
g#(c(x)) -> c_3()
g#(c(0())) -> c_4(g#(d(1())))
g#(c(1())) -> c_5(g#(d(0())))
g#(d(x)) -> c_6()
- Weak TRS:
f(f(x)) -> f(c(f(x)))
f(f(x)) -> f(d(f(x)))
g(c(x)) -> x
g(c(0())) -> g(d(1()))
g(c(1())) -> g(d(0()))
g(d(x)) -> x
- Signature:
{f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
g#(c(x)) -> c_3()
g#(c(0())) -> c_4(g#(d(1())))
g#(c(1())) -> c_5(g#(d(0())))
g#(d(x)) -> c_6()
* Step 4: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
g#(c(x)) -> c_3()
g#(c(0())) -> c_4(g#(d(1())))
g#(c(1())) -> c_5(g#(d(0())))
g#(d(x)) -> c_6()
- Signature:
{f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:g#(c(x)) -> c_3()
2:S:g#(c(0())) -> c_4(g#(d(1())))
-->_1 g#(d(x)) -> c_6():4
3:S:g#(c(1())) -> c_5(g#(d(0())))
-->_1 g#(d(x)) -> c_6():4
4:S:g#(d(x)) -> c_6()
The dependency graph contains no loops, we remove all dependency pairs.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{f/1,g/1,f#/1,g#/1} / {0/0,1/0,c/1,d/1,c_1/2,c_2/2,c_3/0,c_4/1,c_5/1,c_6/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {f#,g#} and constructors {0,1,c,d}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))