* Step 1: Sum WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
dec(Cons(Cons(x,xs),Nil())) -> dec(Nil())
dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs))
dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs))
dec(Cons(Nil(),Nil())) -> Nil()
goal(x) -> nestdec(x)
isNilNil(Cons(Cons(x,xs),Nil())) -> False()
isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False()
isNilNil(Cons(Nil(),Cons(x,xs))) -> False()
isNilNil(Cons(Nil(),Nil())) -> True()
nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs)))
nestdec(Nil()) -> Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Nil())))))))))))))))))
number17(n) -> Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Nil())))))))))))))))))
- Signature:
{dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec
,number17} and constructors {Cons,False,Nil,True}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: Bounds WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
dec(Cons(Cons(x,xs),Nil())) -> dec(Nil())
dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs))
dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs))
dec(Cons(Nil(),Nil())) -> Nil()
goal(x) -> nestdec(x)
isNilNil(Cons(Cons(x,xs),Nil())) -> False()
isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False()
isNilNil(Cons(Nil(),Cons(x,xs))) -> False()
isNilNil(Cons(Nil(),Nil())) -> True()
nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs)))
nestdec(Nil()) -> Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Nil())))))))))))))))))
number17(n) -> Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Nil())))))))))))))))))
- Signature:
{dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec
,number17} and constructors {Cons,False,Nil,True}
+ Applied Processor:
Bounds {initialAutomaton = perSymbol, enrichment = match}
+ Details:
The problem is match-bounded by 2.
The enriched problem is compatible with follwoing automaton.
Cons_0(1,1) -> 1
Cons_0(1,2) -> 1
Cons_0(1,3) -> 1
Cons_0(1,4) -> 1
Cons_0(2,1) -> 1
Cons_0(2,2) -> 1
Cons_0(2,3) -> 1
Cons_0(2,4) -> 1
Cons_0(3,1) -> 1
Cons_0(3,2) -> 1
Cons_0(3,3) -> 1
Cons_0(3,4) -> 1
Cons_0(4,1) -> 1
Cons_0(4,2) -> 1
Cons_0(4,3) -> 1
Cons_0(4,4) -> 1
Cons_1(1,1) -> 10
Cons_1(1,2) -> 10
Cons_1(1,3) -> 10
Cons_1(1,4) -> 10
Cons_1(2,1) -> 10
Cons_1(2,2) -> 10
Cons_1(2,3) -> 10
Cons_1(2,4) -> 10
Cons_1(3,1) -> 10
Cons_1(3,2) -> 10
Cons_1(3,3) -> 10
Cons_1(3,4) -> 10
Cons_1(4,1) -> 10
Cons_1(4,2) -> 10
Cons_1(4,3) -> 10
Cons_1(4,4) -> 10
Cons_1(10,10) -> 26
Cons_1(10,11) -> 6
Cons_1(10,11) -> 8
Cons_1(10,11) -> 9
Cons_1(10,12) -> 11
Cons_1(10,13) -> 12
Cons_1(10,14) -> 13
Cons_1(10,15) -> 14
Cons_1(10,16) -> 15
Cons_1(10,17) -> 16
Cons_1(10,18) -> 17
Cons_1(10,19) -> 18
Cons_1(10,20) -> 19
Cons_1(10,21) -> 20
Cons_1(10,22) -> 21
Cons_1(10,23) -> 22
Cons_1(10,24) -> 23
Cons_1(10,25) -> 24
Cons_1(10,26) -> 25
Cons_2(27,28) -> 6
Cons_2(29,30) -> 28
Cons_2(31,32) -> 30
Cons_2(33,34) -> 32
Cons_2(35,36) -> 34
Cons_2(37,38) -> 36
Cons_2(39,40) -> 38
Cons_2(41,42) -> 40
Cons_2(43,44) -> 42
Cons_2(45,46) -> 44
Cons_2(47,48) -> 46
Cons_2(49,50) -> 48
Cons_2(51,52) -> 50
Cons_2(53,54) -> 52
Cons_2(55,56) -> 54
Cons_2(57,58) -> 56
Cons_2(59,60) -> 58
Cons_2(60,28) -> 8
False_0() -> 2
False_1() -> 7
Nil_0() -> 3
Nil_1() -> 5
Nil_1() -> 10
Nil_2() -> 27
Nil_2() -> 29
Nil_2() -> 31
Nil_2() -> 33
Nil_2() -> 35
Nil_2() -> 37
Nil_2() -> 39
Nil_2() -> 41
Nil_2() -> 43
Nil_2() -> 45
Nil_2() -> 47
Nil_2() -> 49
Nil_2() -> 51
Nil_2() -> 53
Nil_2() -> 55
Nil_2() -> 57
Nil_2() -> 59
Nil_2() -> 60
True_0() -> 4
True_1() -> 7
dec_0(1) -> 5
dec_0(2) -> 5
dec_0(3) -> 5
dec_0(4) -> 5
dec_1(10) -> 5
goal_0(1) -> 6
goal_0(2) -> 6
goal_0(3) -> 6
goal_0(4) -> 6
isNilNil_0(1) -> 7
isNilNil_0(2) -> 7
isNilNil_0(3) -> 7
isNilNil_0(4) -> 7
nestdec_0(1) -> 8
nestdec_0(2) -> 8
nestdec_0(3) -> 8
nestdec_0(4) -> 8
nestdec_1(1) -> 6
nestdec_1(2) -> 6
nestdec_1(3) -> 6
nestdec_1(4) -> 6
nestdec_1(5) -> 6
nestdec_1(5) -> 8
number17_0(1) -> 9
number17_0(2) -> 9
number17_0(3) -> 9
number17_0(4) -> 9
* Step 3: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
dec(Cons(Cons(x,xs),Nil())) -> dec(Nil())
dec(Cons(Cons(x',xs'),Cons(x,xs))) -> dec(Cons(x,xs))
dec(Cons(Nil(),Cons(x,xs))) -> dec(Cons(x,xs))
dec(Cons(Nil(),Nil())) -> Nil()
goal(x) -> nestdec(x)
isNilNil(Cons(Cons(x,xs),Nil())) -> False()
isNilNil(Cons(Cons(x',xs'),Cons(x,xs))) -> False()
isNilNil(Cons(Nil(),Cons(x,xs))) -> False()
isNilNil(Cons(Nil(),Nil())) -> True()
nestdec(Cons(x,xs)) -> nestdec(dec(Cons(x,xs)))
nestdec(Nil()) -> Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Nil())))))))))))))))))
number17(n) -> Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Cons(Nil()
,Nil())))))))))))))))))
- Signature:
{dec/1,goal/1,isNilNil/1,nestdec/1,number17/1} / {Cons/2,False/0,Nil/0,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {dec,goal,isNilNil,nestdec
,number17} and constructors {Cons,False,Nil,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^1))