*** 1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U11(tt(),N,X,XS) -> U12(splitAt(activate(N),activate(XS)),activate(X))
U12(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
and(tt(),X) -> activate(X)
fst(pair(X,Y)) -> X
head(cons(N,XS)) -> N
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
sel(N,XS) -> head(afterNth(N,XS))
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
splitAt(s(N),cons(X,XS)) -> U11(tt(),N,X,activate(XS))
tail(cons(N,XS)) -> activate(XS)
take(N,XS) -> fst(splitAt(N,XS))
Weak DP Rules:
Weak TRS Rules:
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0}
Obligation:
Innermost
basic terms: {U11,U12,activate,afterNth,and,fst,head,natsFrom,s,sel,snd,splitAt,tail,take}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
InnermostRuleRemoval
Proof:
Arguments of following rules are not normal-forms.
splitAt(s(N),cons(X,XS)) -> U11(tt(),N,X,activate(XS))
All above mentioned rules can be savely removed.
*** 1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
U11(tt(),N,X,XS) -> U12(splitAt(activate(N),activate(XS)),activate(X))
U12(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
and(tt(),X) -> activate(X)
fst(pair(X,Y)) -> X
head(cons(N,XS)) -> N
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
sel(N,XS) -> head(afterNth(N,XS))
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
tail(cons(N,XS)) -> activate(XS)
take(N,XS) -> fst(splitAt(N,XS))
Weak DP Rules:
Weak TRS Rules:
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0}
Obligation:
Innermost
basic terms: {U11,U12,activate,afterNth,and,fst,head,natsFrom,s,sel,snd,splitAt,tail,take}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following dependency tuples:
Strict DPs
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(X) -> c_3()
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
and#(tt(),X) -> c_7(activate#(X))
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
tail#(cons(N,XS)) -> c_16(activate#(XS))
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
Weak DPs
and mark the set of starting terms.
*** 1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(X) -> c_3()
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
and#(tt(),X) -> c_7(activate#(X))
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
tail#(cons(N,XS)) -> c_16(activate#(XS))
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
U11(tt(),N,X,XS) -> U12(splitAt(activate(N),activate(XS)),activate(X))
U12(pair(YS,ZS),X) -> pair(cons(activate(X),YS),ZS)
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
and(tt(),X) -> activate(X)
fst(pair(X,Y)) -> X
head(cons(N,XS)) -> N
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
sel(N,XS) -> head(afterNth(N,XS))
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
tail(cons(N,XS)) -> activate(XS)
take(N,XS) -> fst(splitAt(N,XS))
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/5,c_2/1,c_3/0,c_4/2,c_5/2,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(X) -> c_3()
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
and#(tt(),X) -> c_7(activate#(X))
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
tail#(cons(N,XS)) -> c_16(activate#(XS))
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
*** 1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(X) -> c_3()
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
and#(tt(),X) -> c_7(activate#(X))
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
tail#(cons(N,XS)) -> c_16(activate#(XS))
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/5,c_2/1,c_3/0,c_4/2,c_5/2,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{3,8,9,10,11,12,14,15}
by application of
Pre({3,8,9,10,11,12,14,15}) = {1,2,4,5,6,7,13,16,17}.
Here rules are labelled as follows:
1: U11#(tt(),N,X,XS) ->
c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,splitAt#(activate(N)
,activate(XS))
,activate#(N)
,activate#(XS)
,activate#(X))
2: U12#(pair(YS,ZS),X) ->
c_2(activate#(X))
3: activate#(X) -> c_3()
4: activate#(n__natsFrom(X)) ->
c_4(natsFrom#(activate(X))
,activate#(X))
5: activate#(n__s(X)) ->
c_5(s#(activate(X))
,activate#(X))
6: afterNth#(N,XS) ->
c_6(snd#(splitAt(N,XS))
,splitAt#(N,XS))
7: and#(tt(),X) ->
c_7(activate#(X))
8: fst#(pair(X,Y)) -> c_8()
9: head#(cons(N,XS)) -> c_9()
10: natsFrom#(N) -> c_10()
11: natsFrom#(X) -> c_11()
12: s#(X) -> c_12()
13: sel#(N,XS) ->
c_13(head#(afterNth(N,XS))
,afterNth#(N,XS))
14: snd#(pair(X,Y)) -> c_14()
15: splitAt#(0(),XS) -> c_15()
16: tail#(cons(N,XS)) ->
c_16(activate#(XS))
17: take#(N,XS) ->
c_17(fst#(splitAt(N,XS))
,splitAt#(N,XS))
*** 1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
and#(tt(),X) -> c_7(activate#(X))
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
tail#(cons(N,XS)) -> c_16(activate#(XS))
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
Strict TRS Rules:
Weak DP Rules:
activate#(X) -> c_3()
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/5,c_2/1,c_3/0,c_4/2,c_5/2,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{5,9}
by application of
Pre({5,9}) = {7}.
Here rules are labelled as follows:
1: U11#(tt(),N,X,XS) ->
c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,splitAt#(activate(N)
,activate(XS))
,activate#(N)
,activate#(XS)
,activate#(X))
2: U12#(pair(YS,ZS),X) ->
c_2(activate#(X))
3: activate#(n__natsFrom(X)) ->
c_4(natsFrom#(activate(X))
,activate#(X))
4: activate#(n__s(X)) ->
c_5(s#(activate(X))
,activate#(X))
5: afterNth#(N,XS) ->
c_6(snd#(splitAt(N,XS))
,splitAt#(N,XS))
6: and#(tt(),X) ->
c_7(activate#(X))
7: sel#(N,XS) ->
c_13(head#(afterNth(N,XS))
,afterNth#(N,XS))
8: tail#(cons(N,XS)) ->
c_16(activate#(XS))
9: take#(N,XS) ->
c_17(fst#(splitAt(N,XS))
,splitAt#(N,XS))
10: activate#(X) -> c_3()
11: fst#(pair(X,Y)) -> c_8()
12: head#(cons(N,XS)) -> c_9()
13: natsFrom#(N) -> c_10()
14: natsFrom#(X) -> c_11()
15: s#(X) -> c_12()
16: snd#(pair(X,Y)) -> c_14()
17: splitAt#(0(),XS) -> c_15()
*** 1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
and#(tt(),X) -> c_7(activate#(X))
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
tail#(cons(N,XS)) -> c_16(activate#(XS))
Strict TRS Rules:
Weak DP Rules:
activate#(X) -> c_3()
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/5,c_2/1,c_3/0,c_4/2,c_5/2,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{6}
by application of
Pre({6}) = {}.
Here rules are labelled as follows:
1: U11#(tt(),N,X,XS) ->
c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,splitAt#(activate(N)
,activate(XS))
,activate#(N)
,activate#(XS)
,activate#(X))
2: U12#(pair(YS,ZS),X) ->
c_2(activate#(X))
3: activate#(n__natsFrom(X)) ->
c_4(natsFrom#(activate(X))
,activate#(X))
4: activate#(n__s(X)) ->
c_5(s#(activate(X))
,activate#(X))
5: and#(tt(),X) ->
c_7(activate#(X))
6: sel#(N,XS) ->
c_13(head#(afterNth(N,XS))
,afterNth#(N,XS))
7: tail#(cons(N,XS)) ->
c_16(activate#(XS))
8: activate#(X) -> c_3()
9: afterNth#(N,XS) ->
c_6(snd#(splitAt(N,XS))
,splitAt#(N,XS))
10: fst#(pair(X,Y)) -> c_8()
11: head#(cons(N,XS)) -> c_9()
12: natsFrom#(N) -> c_10()
13: natsFrom#(X) -> c_11()
14: s#(X) -> c_12()
15: snd#(pair(X,Y)) -> c_14()
16: splitAt#(0(),XS) -> c_15()
17: take#(N,XS) ->
c_17(fst#(splitAt(N,XS))
,splitAt#(N,XS))
*** 1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
and#(tt(),X) -> c_7(activate#(X))
tail#(cons(N,XS)) -> c_16(activate#(XS))
Strict TRS Rules:
Weak DP Rules:
activate#(X) -> c_3()
afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
fst#(pair(X,Y)) -> c_8()
head#(cons(N,XS)) -> c_9()
natsFrom#(N) -> c_10()
natsFrom#(X) -> c_11()
s#(X) -> c_12()
sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
snd#(pair(X,Y)) -> c_14()
splitAt#(0(),XS) -> c_15()
take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/5,c_2/1,c_3/0,c_4/2,c_5/2,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
-->_5 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_4 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_3 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_5 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_4 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_3 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_1 U12#(pair(YS,ZS),X) -> c_2(activate#(X)):2
-->_2 splitAt#(0(),XS) -> c_15():16
-->_5 activate#(X) -> c_3():7
-->_4 activate#(X) -> c_3():7
-->_3 activate#(X) -> c_3():7
2:S:U12#(pair(YS,ZS),X) -> c_2(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_1 activate#(X) -> c_3():7
3:S:activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
-->_2 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 natsFrom#(X) -> c_11():12
-->_1 natsFrom#(N) -> c_10():11
-->_2 activate#(X) -> c_3():7
-->_2 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
4:S:activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
-->_1 s#(X) -> c_12():13
-->_2 activate#(X) -> c_3():7
-->_2 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_2 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
5:S:and#(tt(),X) -> c_7(activate#(X))
-->_1 activate#(X) -> c_3():7
-->_1 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
6:S:tail#(cons(N,XS)) -> c_16(activate#(XS))
-->_1 activate#(X) -> c_3():7
-->_1 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
7:W:activate#(X) -> c_3()
8:W:afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS))
-->_2 splitAt#(0(),XS) -> c_15():16
-->_1 snd#(pair(X,Y)) -> c_14():15
9:W:fst#(pair(X,Y)) -> c_8()
10:W:head#(cons(N,XS)) -> c_9()
11:W:natsFrom#(N) -> c_10()
12:W:natsFrom#(X) -> c_11()
13:W:s#(X) -> c_12()
14:W:sel#(N,XS) -> c_13(head#(afterNth(N,XS)),afterNth#(N,XS))
-->_1 head#(cons(N,XS)) -> c_9():10
-->_2 afterNth#(N,XS) -> c_6(snd#(splitAt(N,XS)),splitAt#(N,XS)):8
15:W:snd#(pair(X,Y)) -> c_14()
16:W:splitAt#(0(),XS) -> c_15()
17:W:take#(N,XS) -> c_17(fst#(splitAt(N,XS)),splitAt#(N,XS))
-->_2 splitAt#(0(),XS) -> c_15():16
-->_1 fst#(pair(X,Y)) -> c_8():9
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
17: take#(N,XS) ->
c_17(fst#(splitAt(N,XS))
,splitAt#(N,XS))
14: sel#(N,XS) ->
c_13(head#(afterNth(N,XS))
,afterNth#(N,XS))
10: head#(cons(N,XS)) -> c_9()
9: fst#(pair(X,Y)) -> c_8()
8: afterNth#(N,XS) ->
c_6(snd#(splitAt(N,XS))
,splitAt#(N,XS))
15: snd#(pair(X,Y)) -> c_14()
16: splitAt#(0(),XS) -> c_15()
11: natsFrom#(N) -> c_10()
12: natsFrom#(X) -> c_11()
7: activate#(X) -> c_3()
13: s#(X) -> c_12()
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
and#(tt(),X) -> c_7(activate#(X))
tail#(cons(N,XS)) -> c_16(activate#(XS))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/5,c_2/1,c_3/0,c_4/2,c_5/2,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),splitAt#(activate(N),activate(XS)),activate#(N),activate#(XS),activate#(X))
-->_5 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_4 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_3 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_5 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_4 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_3 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
-->_1 U12#(pair(YS,ZS),X) -> c_2(activate#(X)):2
2:S:U12#(pair(YS,ZS),X) -> c_2(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
3:S:activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X))
-->_2 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_2 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
4:S:activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X))
-->_2 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_2 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
5:S:and#(tt(),X) -> c_7(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
6:S:tail#(cons(N,XS)) -> c_16(activate#(XS))
-->_1 activate#(n__s(X)) -> c_5(s#(activate(X)),activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(natsFrom#(activate(X)),activate#(X)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
and#(tt(),X) -> c_7(activate#(X))
tail#(cons(N,XS)) -> c_16(activate#(XS))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
afterNth(N,XS) -> snd(splitAt(N,XS))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
snd(pair(X,Y)) -> Y
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
and#(tt(),X) -> c_7(activate#(X))
tail#(cons(N,XS)) -> c_16(activate#(XS))
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
and#(tt(),X) -> c_7(activate#(X))
tail#(cons(N,XS)) -> c_16(activate#(XS))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
RemoveHeads
Proof:
Consider the dependency graph
1:S:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
-->_4 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_3 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_2 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_4 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_3 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_2 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_1 U12#(pair(YS,ZS),X) -> c_2(activate#(X)):2
2:S:U12#(pair(YS,ZS),X) -> c_2(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
3:S:activate#(n__natsFrom(X)) -> c_4(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
4:S:activate#(n__s(X)) -> c_5(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
5:S:and#(tt(),X) -> c_7(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
6:S:tail#(cons(N,XS)) -> c_16(activate#(XS))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
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).
[(5,and#(tt(),X) -> c_7(activate#(X))),(6,tail#(cons(N,XS)) -> c_16(activate#(XS)))]
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
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 DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Problem (S)
Strict DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
*** 1.1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
4: activate#(n__s(X)) ->
c_5(activate#(X))
Consider the set of all dependency pairs
1: U11#(tt(),N,X,XS) ->
c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,activate#(N)
,activate#(XS)
,activate#(X))
2: U12#(pair(YS,ZS),X) ->
c_2(activate#(X))
3: activate#(n__natsFrom(X)) ->
c_4(activate#(X))
4: activate#(n__s(X)) ->
c_5(activate#(X))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{4}
These cover all (indirect) predecessors of dependency pairs
{1,2,4}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_1) = {1,2,3,4},
uargs(c_2) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1}
Following symbols are considered usable:
{activate,natsFrom,s,splitAt,U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}
TcT has computed the following interpretation:
p(0) = [2]
p(U11) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [1]
p(U12) = [1] x1 + [2]
p(activate) = [1] x1 + [0]
p(afterNth) = [2] x1 + [1]
p(and) = [8] x2 + [2]
p(cons) = [1] x1 + [0]
p(fst) = [1]
p(head) = [1] x1 + [1]
p(n__natsFrom) = [1] x1 + [0]
p(n__s) = [1] x1 + [2]
p(natsFrom) = [1] x1 + [0]
p(nil) = [1]
p(pair) = [12]
p(s) = [1] x1 + [2]
p(sel) = [2]
p(snd) = [1] x1 + [1]
p(splitAt) = [10] x1 + [10]
p(tail) = [1]
p(take) = [1] x1 + [2] x2 + [1]
p(tt) = [2]
p(U11#) = [8] x1 + [4] x2 + [12] x3 + [4] x4 + [4]
p(U12#) = [8] x2 + [12]
p(activate#) = [2] x1 + [0]
p(afterNth#) = [1] x1 + [8] x2 + [2]
p(and#) = [0]
p(fst#) = [2] x1 + [1]
p(head#) = [1]
p(natsFrom#) = [1] x1 + [2]
p(s#) = [1]
p(sel#) = [2] x2 + [4]
p(snd#) = [1] x1 + [1]
p(splitAt#) = [1]
p(tail#) = [1] x1 + [0]
p(take#) = [1] x2 + [0]
p(c_1) = [1] x1 + [2] x2 + [2] x3 + [2] x4 + [8]
p(c_2) = [4] x1 + [8]
p(c_3) = [1]
p(c_4) = [1] x1 + [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x2 + [8]
p(c_7) = [0]
p(c_8) = [1]
p(c_9) = [1]
p(c_10) = [1]
p(c_11) = [4]
p(c_12) = [1]
p(c_13) = [8] x1 + [0]
p(c_14) = [4]
p(c_15) = [8]
p(c_16) = [2]
p(c_17) = [1]
Following rules are strictly oriented:
activate#(n__s(X)) = [2] X + [4]
> [2] X + [0]
= c_5(activate#(X))
Following rules are (at-least) weakly oriented:
U11#(tt(),N,X,XS) = [4] N + [12] X + [4] XS + [20]
>= [4] N + [12] X + [4] XS + [20]
= c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,activate#(N)
,activate#(XS)
,activate#(X))
U12#(pair(YS,ZS),X) = [8] X + [12]
>= [8] X + [8]
= c_2(activate#(X))
activate#(n__natsFrom(X)) = [2] X + [0]
>= [2] X + [0]
= c_4(activate#(X))
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n__natsFrom(X)) = [1] X + [0]
>= [1] X + [0]
= natsFrom(activate(X))
activate(n__s(X)) = [1] X + [2]
>= [1] X + [2]
= s(activate(X))
natsFrom(N) = [1] N + [0]
>= [1] N + [0]
= cons(N,n__natsFrom(n__s(N)))
natsFrom(X) = [1] X + [0]
>= [1] X + [0]
= n__natsFrom(X)
s(X) = [1] X + [2]
>= [1] X + [2]
= n__s(X)
splitAt(0(),XS) = [30]
>= [12]
= pair(nil(),XS)
*** 1.1.1.1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(n__natsFrom(X)) -> c_4(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
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, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: activate#(n__natsFrom(X)) ->
c_4(activate#(X))
Consider the set of all dependency pairs
1: activate#(n__natsFrom(X)) ->
c_4(activate#(X))
2: U11#(tt(),N,X,XS) ->
c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,activate#(N)
,activate#(XS)
,activate#(X))
3: U12#(pair(YS,ZS),X) ->
c_2(activate#(X))
4: activate#(n__s(X)) ->
c_5(activate#(X))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}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,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
activate#(n__natsFrom(X)) -> c_4(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_1) = {1,2,3,4},
uargs(c_2) = {1},
uargs(c_4) = {1},
uargs(c_5) = {1}
Following symbols are considered usable:
{activate,natsFrom,s,U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}
TcT has computed the following interpretation:
p(0) = [0]
p(U11) = [4] x1 + [1] x2 + [1] x3 + [2] x4 + [8]
p(U12) = [2] x2 + [2]
p(activate) = [1] x1 + [0]
p(afterNth) = [1] x2 + [0]
p(and) = [1] x1 + [0]
p(cons) = [4]
p(fst) = [4] x1 + [0]
p(head) = [2] x1 + [0]
p(n__natsFrom) = [1] x1 + [4]
p(n__s) = [1] x1 + [13]
p(natsFrom) = [1] x1 + [4]
p(nil) = [0]
p(pair) = [1] x2 + [4]
p(s) = [1] x1 + [13]
p(sel) = [1] x1 + [1] x2 + [1]
p(snd) = [2] x1 + [2]
p(splitAt) = [8] x2 + [8]
p(tail) = [2] x1 + [2]
p(take) = [8] x1 + [0]
p(tt) = [8]
p(U11#) = [3] x1 + [12] x2 + [4] x3 + [1] x4 + [0]
p(U12#) = [1] x2 + [12]
p(activate#) = [1] x1 + [0]
p(afterNth#) = [1] x1 + [0]
p(and#) = [1] x1 + [1]
p(fst#) = [1]
p(head#) = [1] x1 + [1]
p(natsFrom#) = [1]
p(s#) = [8]
p(sel#) = [1] x1 + [4] x2 + [2]
p(snd#) = [1] x1 + [0]
p(splitAt#) = [1] x1 + [0]
p(tail#) = [1]
p(take#) = [2] x2 + [1]
p(c_1) = [2] x1 + [8] x2 + [1] x3 + [2] x4 + [0]
p(c_2) = [1] x1 + [2]
p(c_3) = [1]
p(c_4) = [1] x1 + [2]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [1] x1 + [1]
p(c_8) = [1]
p(c_9) = [8]
p(c_10) = [1]
p(c_11) = [2]
p(c_12) = [1]
p(c_13) = [1] x1 + [2]
p(c_14) = [2]
p(c_15) = [1]
p(c_16) = [1] x1 + [1]
p(c_17) = [1] x2 + [0]
Following rules are strictly oriented:
activate#(n__natsFrom(X)) = [1] X + [4]
> [1] X + [2]
= c_4(activate#(X))
Following rules are (at-least) weakly oriented:
U11#(tt(),N,X,XS) = [12] N + [4] X + [1] XS + [24]
>= [8] N + [4] X + [1] XS + [24]
= c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,activate#(N)
,activate#(XS)
,activate#(X))
U12#(pair(YS,ZS),X) = [1] X + [12]
>= [1] X + [2]
= c_2(activate#(X))
activate#(n__s(X)) = [1] X + [13]
>= [1] X + [0]
= c_5(activate#(X))
activate(X) = [1] X + [0]
>= [1] X + [0]
= X
activate(n__natsFrom(X)) = [1] X + [4]
>= [1] X + [4]
= natsFrom(activate(X))
activate(n__s(X)) = [1] X + [13]
>= [1] X + [13]
= s(activate(X))
natsFrom(N) = [1] N + [4]
>= [4]
= cons(N,n__natsFrom(n__s(N)))
natsFrom(X) = [1] X + [4]
>= [1] X + [4]
= n__natsFrom(X)
s(X) = [1] X + [13]
>= [1] X + [13]
= n__s(X)
*** 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.1.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
-->_4 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_3 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_2 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_4 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_3 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_2 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_1 U12#(pair(YS,ZS),X) -> c_2(activate#(X)):2
2:W:U12#(pair(YS,ZS),X) -> c_2(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
3:W:activate#(n__natsFrom(X)) -> c_4(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
4:W:activate#(n__s(X)) -> c_5(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: U11#(tt(),N,X,XS) ->
c_1(U12#(splitAt(activate(N)
,activate(XS))
,activate(X))
,activate#(N)
,activate#(XS)
,activate#(X))
2: U12#(pair(YS,ZS),X) ->
c_2(activate#(X))
4: activate#(n__s(X)) ->
c_5(activate#(X))
3: activate#(n__natsFrom(X)) ->
c_4(activate#(X))
*** 1.1.1.1.1.1.1.1.1.1.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
activate#(n__natsFrom(X)) -> c_4(activate#(X))
activate#(n__s(X)) -> c_5(activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:U12#(pair(YS,ZS),X) -> c_2(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
2:W:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
-->_4 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_3 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_2 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_4 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_3 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_2 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
-->_1 U12#(pair(YS,ZS),X) -> c_2(activate#(X)):1
3:W:activate#(n__natsFrom(X)) -> c_4(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
4:W:activate#(n__s(X)) -> c_5(activate#(X))
-->_1 activate#(n__s(X)) -> c_5(activate#(X)):4
-->_1 activate#(n__natsFrom(X)) -> c_4(activate#(X)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: activate#(n__s(X)) ->
c_5(activate#(X))
3: activate#(n__natsFrom(X)) ->
c_4(activate#(X))
*** 1.1.1.1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
U12#(pair(YS,ZS),X) -> c_2(activate#(X))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/4,c_2/1,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:U12#(pair(YS,ZS),X) -> c_2(activate#(X))
2:W:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)),activate#(N),activate#(XS),activate#(X))
-->_1 U12#(pair(YS,ZS),X) -> c_2(activate#(X)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)))
U12#(pair(YS,ZS),X) -> c_2()
*** 1.1.1.1.1.1.1.1.1.1.1.2.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
U12#(pair(YS,ZS),X) -> c_2()
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)))
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
Trivial
Proof:
Consider the dependency graph
1:S:U12#(pair(YS,ZS),X) -> c_2()
2:W:U11#(tt(),N,X,XS) -> c_1(U12#(splitAt(activate(N),activate(XS)),activate(X)))
-->_1 U12#(pair(YS,ZS),X) -> c_2():1
The dependency graph contains no loops, we remove all dependency pairs.
*** 1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
activate(X) -> X
activate(n__natsFrom(X)) -> natsFrom(activate(X))
activate(n__s(X)) -> s(activate(X))
natsFrom(N) -> cons(N,n__natsFrom(n__s(N)))
natsFrom(X) -> n__natsFrom(X)
s(X) -> n__s(X)
splitAt(0(),XS) -> pair(nil(),XS)
Signature:
{U11/4,U12/2,activate/1,afterNth/2,and/2,fst/1,head/1,natsFrom/1,s/1,sel/2,snd/1,splitAt/2,tail/1,take/2,U11#/4,U12#/2,activate#/1,afterNth#/2,and#/2,fst#/1,head#/1,natsFrom#/1,s#/1,sel#/2,snd#/1,splitAt#/2,tail#/1,take#/2} / {0/0,cons/2,n__natsFrom/1,n__s/1,nil/0,pair/2,tt/0,c_1/1,c_2/0,c_3/0,c_4/1,c_5/1,c_6/2,c_7/1,c_8/0,c_9/0,c_10/0,c_11/0,c_12/0,c_13/2,c_14/0,c_15/0,c_16/1,c_17/2}
Obligation:
Innermost
basic terms: {U11#,U12#,activate#,afterNth#,and#,fst#,head#,natsFrom#,s#,sel#,snd#,splitAt#,tail#,take#}/{0,cons,n__natsFrom,n__s,nil,pair,tt}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).