MAYBE
* Step 1: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
f(s(x),s(y)) -> f(-(x,min(x,y)),s(twice(min(x,y))))
f(s(x),s(y)) -> f(-(y,min(x,y)),s(twice(min(x,y))))
min(x,0()) -> 0()
min(0(),y) -> 0()
min(s(x),s(y)) -> s(min(x,y))
twice(0()) -> 0()
twice(s(x)) -> s(s(twice(x)))
- Signature:
{-/2,f/2,min/2,twice/1} / {0/0,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-,f,min,twice} and constructors {0,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
-#(x,0()) -> c_1()
-#(s(x),s(y)) -> c_2(-#(x,y))
f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
min#(x,0()) -> c_5()
min#(0(),y) -> c_6()
min#(s(x),s(y)) -> c_7(min#(x,y))
twice#(0()) -> c_8()
twice#(s(x)) -> c_9(twice#(x))
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
-#(x,0()) -> c_1()
-#(s(x),s(y)) -> c_2(-#(x,y))
f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
min#(x,0()) -> c_5()
min#(0(),y) -> c_6()
min#(s(x),s(y)) -> c_7(min#(x,y))
twice#(0()) -> c_8()
twice#(s(x)) -> c_9(twice#(x))
- Weak TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
f(s(x),s(y)) -> f(-(x,min(x,y)),s(twice(min(x,y))))
f(s(x),s(y)) -> f(-(y,min(x,y)),s(twice(min(x,y))))
min(x,0()) -> 0()
min(0(),y) -> 0()
min(s(x),s(y)) -> s(min(x,y))
twice(0()) -> 0()
twice(s(x)) -> s(s(twice(x)))
- Signature:
{-/2,f/2,min/2,twice/1,-#/2,f#/2,min#/2,twice#/1} / {0/0,s/1,c_1/0,c_2/1,c_3/5,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0
,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-#,f#,min#,twice#} and constructors {0,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
min(x,0()) -> 0()
min(0(),y) -> 0()
min(s(x),s(y)) -> s(min(x,y))
twice(0()) -> 0()
twice(s(x)) -> s(s(twice(x)))
-#(x,0()) -> c_1()
-#(s(x),s(y)) -> c_2(-#(x,y))
f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
min#(x,0()) -> c_5()
min#(0(),y) -> c_6()
min#(s(x),s(y)) -> c_7(min#(x,y))
twice#(0()) -> c_8()
twice#(s(x)) -> c_9(twice#(x))
* Step 3: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
-#(x,0()) -> c_1()
-#(s(x),s(y)) -> c_2(-#(x,y))
f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
min#(x,0()) -> c_5()
min#(0(),y) -> c_6()
min#(s(x),s(y)) -> c_7(min#(x,y))
twice#(0()) -> c_8()
twice#(s(x)) -> c_9(twice#(x))
- Weak TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
min(x,0()) -> 0()
min(0(),y) -> 0()
min(s(x),s(y)) -> s(min(x,y))
twice(0()) -> 0()
twice(s(x)) -> s(s(twice(x)))
- Signature:
{-/2,f/2,min/2,twice/1,-#/2,f#/2,min#/2,twice#/1} / {0/0,s/1,c_1/0,c_2/1,c_3/5,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0
,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-#,f#,min#,twice#} and constructors {0,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,5,6,8}
by application of
Pre({1,5,6,8}) = {2,3,4,7,9}.
Here rules are labelled as follows:
1: -#(x,0()) -> c_1()
2: -#(s(x),s(y)) -> c_2(-#(x,y))
3: f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
4: f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
5: min#(x,0()) -> c_5()
6: min#(0(),y) -> c_6()
7: min#(s(x),s(y)) -> c_7(min#(x,y))
8: twice#(0()) -> c_8()
9: twice#(s(x)) -> c_9(twice#(x))
* Step 4: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
-#(s(x),s(y)) -> c_2(-#(x,y))
f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
min#(s(x),s(y)) -> c_7(min#(x,y))
twice#(s(x)) -> c_9(twice#(x))
- Weak DPs:
-#(x,0()) -> c_1()
min#(x,0()) -> c_5()
min#(0(),y) -> c_6()
twice#(0()) -> c_8()
- Weak TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
min(x,0()) -> 0()
min(0(),y) -> 0()
min(s(x),s(y)) -> s(min(x,y))
twice(0()) -> 0()
twice(s(x)) -> s(s(twice(x)))
- Signature:
{-/2,f/2,min/2,twice/1,-#/2,f#/2,min#/2,twice#/1} / {0/0,s/1,c_1/0,c_2/1,c_3/5,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0
,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-#,f#,min#,twice#} and constructors {0,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:-#(s(x),s(y)) -> c_2(-#(x,y))
-->_1 -#(x,0()) -> c_1():6
-->_1 -#(s(x),s(y)) -> c_2(-#(x,y)):1
2:S:f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
-->_4 twice#(s(x)) -> c_9(twice#(x)):5
-->_5 min#(s(x),s(y)) -> c_7(min#(x,y)):4
-->_3 min#(s(x),s(y)) -> c_7(min#(x,y)):4
-->_1 f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y)):3
-->_4 twice#(0()) -> c_8():9
-->_5 min#(0(),y) -> c_6():8
-->_3 min#(0(),y) -> c_6():8
-->_5 min#(x,0()) -> c_5():7
-->_3 min#(x,0()) -> c_5():7
-->_2 -#(x,0()) -> c_1():6
-->_1 f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y)):2
-->_2 -#(s(x),s(y)) -> c_2(-#(x,y)):1
3:S:f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
-->_4 twice#(s(x)) -> c_9(twice#(x)):5
-->_5 min#(s(x),s(y)) -> c_7(min#(x,y)):4
-->_3 min#(s(x),s(y)) -> c_7(min#(x,y)):4
-->_4 twice#(0()) -> c_8():9
-->_5 min#(0(),y) -> c_6():8
-->_3 min#(0(),y) -> c_6():8
-->_5 min#(x,0()) -> c_5():7
-->_3 min#(x,0()) -> c_5():7
-->_2 -#(x,0()) -> c_1():6
-->_1 f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y)):3
-->_1 f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y)):2
-->_2 -#(s(x),s(y)) -> c_2(-#(x,y)):1
4:S:min#(s(x),s(y)) -> c_7(min#(x,y))
-->_1 min#(0(),y) -> c_6():8
-->_1 min#(x,0()) -> c_5():7
-->_1 min#(s(x),s(y)) -> c_7(min#(x,y)):4
5:S:twice#(s(x)) -> c_9(twice#(x))
-->_1 twice#(0()) -> c_8():9
-->_1 twice#(s(x)) -> c_9(twice#(x)):5
6:W:-#(x,0()) -> c_1()
7:W:min#(x,0()) -> c_5()
8:W:min#(0(),y) -> c_6()
9:W:twice#(0()) -> c_8()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: min#(x,0()) -> c_5()
8: min#(0(),y) -> c_6()
9: twice#(0()) -> c_8()
6: -#(x,0()) -> c_1()
* Step 5: Failure MAYBE
+ Considered Problem:
- Strict DPs:
-#(s(x),s(y)) -> c_2(-#(x,y))
f#(s(x),s(y)) -> c_3(f#(-(x,min(x,y)),s(twice(min(x,y))))
,-#(x,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
f#(s(x),s(y)) -> c_4(f#(-(y,min(x,y)),s(twice(min(x,y))))
,-#(y,min(x,y))
,min#(x,y)
,twice#(min(x,y))
,min#(x,y))
min#(s(x),s(y)) -> c_7(min#(x,y))
twice#(s(x)) -> c_9(twice#(x))
- Weak TRS:
-(x,0()) -> x
-(s(x),s(y)) -> -(x,y)
min(x,0()) -> 0()
min(0(),y) -> 0()
min(s(x),s(y)) -> s(min(x,y))
twice(0()) -> 0()
twice(s(x)) -> s(s(twice(x)))
- Signature:
{-/2,f/2,min/2,twice/1,-#/2,f#/2,min#/2,twice#/1} / {0/0,s/1,c_1/0,c_2/1,c_3/5,c_4/5,c_5/0,c_6/0,c_7/1,c_8/0
,c_9/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {-#,f#,min#,twice#} and constructors {0,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE