WORST_CASE(?,O(n^2))
* Step 1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
head(queue(cons(x,f),r)) -> x
head(queue(nil(),r)) -> errorHead()
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
tail(queue(cons(x,f),r)) -> checkF(queue(f,r))
tail(queue(nil(),r)) -> errorTail()
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0
,queue/2,s/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF,empty,enq,head,rev,rev',snoc
,tail} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
checkF#(queue(cons(x,xs),r)) -> c_1()
checkF#(queue(nil(),r)) -> c_2(rev#(r))
empty#() -> c_3()
enq#(0()) -> c_4(empty#())
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
head#(queue(cons(x,f),r)) -> c_6()
head#(queue(nil(),r)) -> c_7()
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
rev'#(nil(),ys) -> c_10()
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
tail#(queue(nil(),r)) -> c_13()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(cons(x,xs),r)) -> c_1()
checkF#(queue(nil(),r)) -> c_2(rev#(r))
empty#() -> c_3()
enq#(0()) -> c_4(empty#())
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
head#(queue(cons(x,f),r)) -> c_6()
head#(queue(nil(),r)) -> c_7()
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
rev'#(nil(),ys) -> c_10()
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
tail#(queue(nil(),r)) -> c_13()
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
head(queue(cons(x,f),r)) -> x
head(queue(nil(),r)) -> errorHead()
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
tail(queue(cons(x,f),r)) -> checkF(queue(f,r))
tail(queue(nil(),r)) -> errorTail()
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
checkF#(queue(cons(x,xs),r)) -> c_1()
checkF#(queue(nil(),r)) -> c_2(rev#(r))
empty#() -> c_3()
enq#(0()) -> c_4(empty#())
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
head#(queue(cons(x,f),r)) -> c_6()
head#(queue(nil(),r)) -> c_7()
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
rev'#(nil(),ys) -> c_10()
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
tail#(queue(nil(),r)) -> c_13()
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(cons(x,xs),r)) -> c_1()
checkF#(queue(nil(),r)) -> c_2(rev#(r))
empty#() -> c_3()
enq#(0()) -> c_4(empty#())
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
head#(queue(cons(x,f),r)) -> c_6()
head#(queue(nil(),r)) -> c_7()
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
rev'#(nil(),ys) -> c_10()
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
tail#(queue(nil(),r)) -> c_13()
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,3,6,7,10,13}
by application of
Pre({1,3,6,7,10,13}) = {4,8,9,11,12}.
Here rules are labelled as follows:
1: checkF#(queue(cons(x,xs),r)) -> c_1()
2: checkF#(queue(nil(),r)) -> c_2(rev#(r))
3: empty#() -> c_3()
4: enq#(0()) -> c_4(empty#())
5: enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
6: head#(queue(cons(x,f),r)) -> c_6()
7: head#(queue(nil(),r)) -> c_7()
8: rev#(xs) -> c_8(rev'#(xs,nil()))
9: rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
10: rev'#(nil(),ys) -> c_10()
11: snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
12: tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
13: tail#(queue(nil(),r)) -> c_13()
* Step 4: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
enq#(0()) -> c_4(empty#())
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
- Weak DPs:
checkF#(queue(cons(x,xs),r)) -> c_1()
empty#() -> c_3()
head#(queue(cons(x,f),r)) -> c_6()
head#(queue(nil(),r)) -> c_7()
rev'#(nil(),ys) -> c_10()
tail#(queue(nil(),r)) -> c_13()
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2}
by application of
Pre({2}) = {3}.
Here rules are labelled as follows:
1: checkF#(queue(nil(),r)) -> c_2(rev#(r))
2: enq#(0()) -> c_4(empty#())
3: enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
4: rev#(xs) -> c_8(rev'#(xs,nil()))
5: rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
6: snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
7: tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
8: checkF#(queue(cons(x,xs),r)) -> c_1()
9: empty#() -> c_3()
10: head#(queue(cons(x,f),r)) -> c_6()
11: head#(queue(nil(),r)) -> c_7()
12: rev'#(nil(),ys) -> c_10()
13: tail#(queue(nil(),r)) -> c_13()
* Step 5: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
- Weak DPs:
checkF#(queue(cons(x,xs),r)) -> c_1()
empty#() -> c_3()
enq#(0()) -> c_4(empty#())
head#(queue(cons(x,f),r)) -> c_6()
head#(queue(nil(),r)) -> c_7()
rev'#(nil(),ys) -> c_10()
tail#(queue(nil(),r)) -> c_13()
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:checkF#(queue(nil(),r)) -> c_2(rev#(r))
-->_1 rev#(xs) -> c_8(rev'#(xs,nil())):3
2:S:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_2 enq#(0()) -> c_4(empty#()):9
-->_1 snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r)))):5
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):2
3:S:rev#(xs) -> c_8(rev'#(xs,nil()))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
-->_1 rev'#(nil(),ys) -> c_10():12
4:S:rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
-->_1 rev'#(nil(),ys) -> c_10():12
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
5:S:snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
-->_1 checkF#(queue(cons(x,xs),r)) -> c_1():7
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
6:S:tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
-->_1 checkF#(queue(cons(x,xs),r)) -> c_1():7
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
7:W:checkF#(queue(cons(x,xs),r)) -> c_1()
8:W:empty#() -> c_3()
9:W:enq#(0()) -> c_4(empty#())
-->_1 empty#() -> c_3():8
10:W:head#(queue(cons(x,f),r)) -> c_6()
11:W:head#(queue(nil(),r)) -> c_7()
12:W:rev'#(nil(),ys) -> c_10()
13:W:tail#(queue(nil(),r)) -> c_13()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
13: tail#(queue(nil(),r)) -> c_13()
11: head#(queue(nil(),r)) -> c_7()
10: head#(queue(cons(x,f),r)) -> c_6()
7: checkF#(queue(cons(x,xs),r)) -> c_1()
9: enq#(0()) -> c_4(empty#())
8: empty#() -> c_3()
12: rev'#(nil(),ys) -> c_10()
* Step 6: RemoveHeads WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:checkF#(queue(nil(),r)) -> c_2(rev#(r))
-->_1 rev#(xs) -> c_8(rev'#(xs,nil())):3
2:S:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_1 snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r)))):5
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):2
3:S:rev#(xs) -> c_8(rev'#(xs,nil()))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
4:S:rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
5:S:snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
6:S:tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r)))
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts).
[(6,tail#(queue(cons(x,f),r)) -> c_12(checkF#(queue(f,r))))]
* Step 7: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
Problem (S)
- Strict DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
** Step 7.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
4: rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
The strictly oriented rules are moved into the weak component.
*** Step 7.a:1.a:1: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_2) = {1},
uargs(c_5) = {1,2},
uargs(c_8) = {1},
uargs(c_9) = {1},
uargs(c_11) = {1}
Following symbols are considered usable:
{checkF,empty,enq,snoc,checkF#,empty#,enq#,head#,rev#,rev'#,snoc#,tail#}
TcT has computed the following interpretation:
p(0) = [1]
[0]
[0]
p(checkF) = [1 0 0] [0]
[0 1 0] x1 + [0]
[0 0 0] [0]
p(cons) = [0 0 1] [0]
[0 1 0] x2 + [1]
[0 0 0] [0]
p(empty) = [0]
[1]
[0]
p(enq) = [1 0 0] [1]
[0 1 0] x1 + [1]
[0 0 0] [0]
p(errorHead) = [0]
[0]
[0]
p(errorTail) = [0]
[0]
[0]
p(head) = [0]
[0]
[0]
p(nil) = [0]
[0]
[0]
p(queue) = [1 0 0] [0]
[0 1 1] x2 + [1]
[0 0 0] [0]
p(rev) = [0]
[0]
[0]
p(rev') = [1 0 0] [0 1 0] [1]
[0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
p(s) = [1 1 0] [1]
[0 1 1] x1 + [1]
[0 0 0] [1]
p(snoc) = [0 1 0] [0 0 0] [0]
[0 1 0] x1 + [0 0 1] x2 + [1]
[0 0 0] [0 0 0] [0]
p(tail) = [0]
[0]
[0]
p(checkF#) = [0 1 0] [0]
[1 0 0] x1 + [1]
[0 0 0] [0]
p(empty#) = [0]
[0]
[0]
p(enq#) = [1 1 1] [0]
[1 1 0] x1 + [1]
[1 1 0] [0]
p(head#) = [0]
[0]
[0]
p(rev#) = [0 1 0] [1]
[1 1 1] x1 + [1]
[0 1 1] [1]
p(rev'#) = [0 1 0] [1 0 1] [0]
[0 0 1] x1 + [1 1 0] x2 + [0]
[0 0 0] [0 1 1] [1]
p(snoc#) = [0 1 0] [0 0 0] [1]
[0 1 0] x1 + [1 0 1] x2 + [0]
[0 0 0] [0 1 0] [1]
p(tail#) = [0]
[0]
[0]
p(c_1) = [0]
[0]
[0]
p(c_2) = [1 0 0] [0]
[0 0 0] x1 + [1]
[0 0 0] [0]
p(c_3) = [0]
[0]
[0]
p(c_4) = [0]
[0]
[0]
p(c_5) = [1 0 0] [1 0 0] [1]
[1 0 1] x1 + [0 0 0] x2 + [0]
[0 1 1] [0 0 0] [0]
p(c_6) = [0]
[0]
[0]
p(c_7) = [0]
[0]
[0]
p(c_8) = [1 0 1] [0]
[0 0 0] x1 + [0]
[0 1 0] [0]
p(c_9) = [1 0 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [1]
p(c_10) = [0]
[0]
[0]
p(c_11) = [1 0 0] [0]
[0 1 0] x1 + [0]
[0 0 0] [1]
p(c_12) = [0]
[0]
[0]
p(c_13) = [0]
[0]
[0]
Following rules are strictly oriented:
rev'#(cons(x,xs),ys) = [0 1 0] [1 0 1] [1]
[0 0 0] xs + [1 1 0] ys + [0]
[0 0 0] [0 1 1] [1]
> [0 1 0] [0 0 1] [0]
[0 0 0] xs + [0 0 0] ys + [0]
[0 0 0] [0 0 0] [1]
= c_9(rev'#(xs,cons(x,ys)))
Following rules are (at-least) weakly oriented:
checkF#(queue(nil(),r)) = [0 1 1] [1]
[1 0 0] r + [1]
[0 0 0] [0]
>= [0 1 0] [1]
[0 0 0] r + [1]
[0 0 0] [0]
= c_2(rev#(r))
enq#(s(n)) = [1 2 1] [3]
[1 2 1] n + [3]
[1 2 1] [2]
>= [1 2 1] [3]
[0 2 0] n + [3]
[1 2 1] [2]
= c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) = [0 1 0] [1]
[1 1 1] xs + [1]
[0 1 1] [1]
>= [0 1 0] [1]
[0 0 0] xs + [0]
[0 0 1] [0]
= c_8(rev'#(xs,nil()))
snoc#(queue(f,r),x) = [0 1 1] [0 0 0] [2]
[0 1 1] r + [1 0 1] x + [1]
[0 0 0] [0 1 0] [1]
>= [0 1 0] [2]
[0 0 1] r + [1]
[0 0 0] [1]
= c_11(checkF#(queue(f,cons(x,r))))
checkF(queue(cons(x,xs),r)) = [1 0 0] [0]
[0 1 1] r + [1]
[0 0 0] [0]
>= [1 0 0] [0]
[0 1 1] r + [1]
[0 0 0] [0]
= queue(cons(x,xs),r)
checkF(queue(nil(),r)) = [1 0 0] [0]
[0 1 1] r + [1]
[0 0 0] [0]
>= [0]
[1]
[0]
= queue(rev(r),nil())
empty() = [0]
[1]
[0]
>= [0]
[1]
[0]
= queue(nil(),nil())
enq(0()) = [2]
[1]
[0]
>= [0]
[1]
[0]
= empty()
enq(s(n)) = [1 1 0] [2]
[0 1 1] n + [2]
[0 0 0] [0]
>= [0 1 0] [1]
[0 1 1] n + [2]
[0 0 0] [0]
= snoc(enq(n),n)
snoc(queue(f,r),x) = [0 1 1] [0 0 0] [1]
[0 1 1] r + [0 0 1] x + [2]
[0 0 0] [0 0 0] [0]
>= [0 0 1] [0]
[0 1 0] r + [2]
[0 0 0] [0]
= checkF(queue(f,cons(x,r)))
*** Step 7.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 7.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:checkF#(queue(nil(),r)) -> c_2(rev#(r))
-->_1 rev#(xs) -> c_8(rev'#(xs,nil())):2
2:S:rev#(xs) -> c_8(rev'#(xs,nil()))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
3:W:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_1 snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r)))):5
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):3
4:W:rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
5:W:snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
*** Step 7.a:1.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:checkF#(queue(nil(),r)) -> c_2(rev#(r))
-->_1 rev#(xs) -> c_8(rev'#(xs,nil())):2
2:S:rev#(xs) -> c_8(rev'#(xs,nil()))
3:W:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_1 snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r)))):5
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):3
5:W:snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
rev#(xs) -> c_8()
*** Step 7.a:1.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8()
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: checkF#(queue(nil(),r)) -> c_2(rev#(r))
Consider the set of all dependency pairs
1: checkF#(queue(nil(),r)) -> c_2(rev#(r))
2: rev#(xs) -> c_8()
3: enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
4: snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
**** Step 7.a:1.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8()
- Weak DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_2) = {1},
uargs(c_5) = {1,2},
uargs(c_11) = {1}
Following symbols are considered usable:
{checkF#,empty#,enq#,head#,rev#,rev'#,snoc#,tail#}
TcT has computed the following interpretation:
p(0) = [0]
p(checkF) = [4] x1 + [4]
p(cons) = [1] x2 + [3]
p(empty) = [0]
p(enq) = [0]
p(errorHead) = [2]
p(errorTail) = [4]
p(head) = [0]
p(nil) = [3]
p(queue) = [1] x2 + [1]
p(rev) = [1] x1 + [2]
p(rev') = [1] x1 + [8]
p(s) = [1] x1 + [2]
p(snoc) = [4] x2 + [6]
p(tail) = [2] x1 + [1]
p(checkF#) = [1]
p(empty#) = [2]
p(enq#) = [8] x1 + [0]
p(head#) = [0]
p(rev#) = [0]
p(rev'#) = [1] x1 + [8] x2 + [1]
p(snoc#) = [2]
p(tail#) = [1] x1 + [0]
p(c_1) = [0]
p(c_2) = [8] x1 + [0]
p(c_3) = [0]
p(c_4) = [0]
p(c_5) = [8] x1 + [1] x2 + [0]
p(c_6) = [1]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [2] x1 + [8]
p(c_10) = [0]
p(c_11) = [2] x1 + [0]
p(c_12) = [2] x1 + [0]
p(c_13) = [4]
Following rules are strictly oriented:
checkF#(queue(nil(),r)) = [1]
> [0]
= c_2(rev#(r))
Following rules are (at-least) weakly oriented:
enq#(s(n)) = [8] n + [16]
>= [8] n + [16]
= c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) = [0]
>= [0]
= c_8()
snoc#(queue(f,r),x) = [2]
>= [2]
= c_11(checkF#(queue(f,cons(x,r))))
**** Step 7.a:1.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
rev#(xs) -> c_8()
- Weak DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 7.a:1.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
rev#(xs) -> c_8()
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:checkF#(queue(nil(),r)) -> c_2(rev#(r))
-->_1 rev#(xs) -> c_8():3
2:W:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_1 snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r)))):4
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):2
3:W:rev#(xs) -> c_8()
4:W:snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
4: snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
1: checkF#(queue(nil(),r)) -> c_2(rev#(r))
3: rev#(xs) -> c_8()
**** Step 7.a:1.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 7.b:1: PredecessorEstimation WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{2}
by application of
Pre({2}) = {1}.
Here rules are labelled as follows:
1: enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
2: snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
3: checkF#(queue(nil(),r)) -> c_2(rev#(r))
4: rev#(xs) -> c_8(rev'#(xs,nil()))
5: rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
** Step 7.b:2: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
- Weak DPs:
checkF#(queue(nil(),r)) -> c_2(rev#(r))
rev#(xs) -> c_8(rev'#(xs,nil()))
rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_1 snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r)))):5
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):1
2:W:checkF#(queue(nil(),r)) -> c_2(rev#(r))
-->_1 rev#(xs) -> c_8(rev'#(xs,nil())):3
3:W:rev#(xs) -> c_8(rev'#(xs,nil()))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
4:W:rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
-->_1 rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys))):4
5:W:snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
-->_1 checkF#(queue(nil(),r)) -> c_2(rev#(r)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: snoc#(queue(f,r),x) -> c_11(checkF#(queue(f,cons(x,r))))
2: checkF#(queue(nil(),r)) -> c_2(rev#(r))
3: rev#(xs) -> c_8(rev'#(xs,nil()))
4: rev'#(cons(x,xs),ys) -> c_9(rev'#(xs,cons(x,ys)))
** Step 7.b:3: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/2
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n))
-->_2 enq#(s(n)) -> c_5(snoc#(enq(n),n),enq#(n)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
enq#(s(n)) -> c_5(enq#(n))
** Step 7.b:4: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
enq#(s(n)) -> c_5(enq#(n))
- Weak TRS:
checkF(queue(cons(x,xs),r)) -> queue(cons(x,xs),r)
checkF(queue(nil(),r)) -> queue(rev(r),nil())
empty() -> queue(nil(),nil())
enq(0()) -> empty()
enq(s(n)) -> snoc(enq(n),n)
rev(xs) -> rev'(xs,nil())
rev'(cons(x,xs),ys) -> rev'(xs,cons(x,ys))
rev'(nil(),ys) -> ys
snoc(queue(f,r),x) -> checkF(queue(f,cons(x,r)))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
enq#(s(n)) -> c_5(enq#(n))
** Step 7.b:5: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
enq#(s(n)) -> c_5(enq#(n))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: enq#(s(n)) -> c_5(enq#(n))
The strictly oriented rules are moved into the weak component.
*** Step 7.b:5.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
enq#(s(n)) -> c_5(enq#(n))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_5) = {1}
Following symbols are considered usable:
{checkF#,empty#,enq#,head#,rev#,rev'#,snoc#,tail#}
TcT has computed the following interpretation:
p(0) = [1]
p(checkF) = [1] x1 + [8]
p(cons) = [1] x1 + [1] x2 + [0]
p(empty) = [0]
p(enq) = [0]
p(errorHead) = [0]
p(errorTail) = [0]
p(head) = [0]
p(nil) = [0]
p(queue) = [1] x1 + [1] x2 + [0]
p(rev) = [0]
p(rev') = [0]
p(s) = [1] x1 + [9]
p(snoc) = [0]
p(tail) = [0]
p(checkF#) = [0]
p(empty#) = [0]
p(enq#) = [1] x1 + [7]
p(head#) = [0]
p(rev#) = [0]
p(rev'#) = [1]
p(snoc#) = [1] x2 + [1]
p(tail#) = [1] x1 + [8]
p(c_1) = [1]
p(c_2) = [8]
p(c_3) = [1]
p(c_4) = [1] x1 + [1]
p(c_5) = [1] x1 + [0]
p(c_6) = [1]
p(c_7) = [1]
p(c_8) = [1]
p(c_9) = [1] x1 + [2]
p(c_10) = [2]
p(c_11) = [1] x1 + [1]
p(c_12) = [1] x1 + [0]
p(c_13) = [0]
Following rules are strictly oriented:
enq#(s(n)) = [1] n + [16]
> [1] n + [7]
= c_5(enq#(n))
Following rules are (at-least) weakly oriented:
*** Step 7.b:5.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
enq#(s(n)) -> c_5(enq#(n))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
*** Step 7.b:5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
enq#(s(n)) -> c_5(enq#(n))
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:enq#(s(n)) -> c_5(enq#(n))
-->_1 enq#(s(n)) -> c_5(enq#(n)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: enq#(s(n)) -> c_5(enq#(n))
*** Step 7.b:5.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Signature:
{checkF/1,empty/0,enq/1,head/1,rev/1,rev'/2,snoc/2,tail/1,checkF#/1,empty#/0,enq#/1,head#/1,rev#/1,rev'#/2
,snoc#/2,tail#/1} / {0/0,cons/2,errorHead/0,errorTail/0,nil/0,queue/2,s/1,c_1/0,c_2/1,c_3/0,c_4/1,c_5/1
,c_6/0,c_7/0,c_8/1,c_9/1,c_10/0,c_11/1,c_12/1,c_13/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {checkF#,empty#,enq#,head#,rev#,rev'#,snoc#
,tail#} and constructors {0,cons,errorHead,errorTail,nil,queue,s}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))