MAYBE
* Step 1: InnermostRuleRemoval MAYBE
+ Considered Problem:
- Strict TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
U31(tt(),N) -> activate(N)
U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(N,0()) -> U31(and(isNat(N),n__isNatKind(N)),N)
plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0,U11,U12,U13,U21,U22,U31,U41,activate,and,isNat
,isNatKind,plus,s} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
InnermostRuleRemoval
+ Details:
Arguments of following rules are not normal-forms.
plus(N,0()) -> U31(and(isNat(N),n__isNatKind(N)),N)
plus(N,s(M)) -> U41(and(and(isNat(M),n__isNatKind(M)),n__and(isNat(N),n__isNatKind(N))),M,N)
All above mentioned rules can be savely removed.
* Step 2: DependencyPairs MAYBE
+ Considered Problem:
- Strict TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
U31(tt(),N) -> activate(N)
U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0,U11,U12,U13,U21,U22,U31,U41,activate,and,isNat
,isNatKind,plus,s} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U13#(tt()) -> c_4()
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U22#(tt()) -> c_6()
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(X) -> c_9()
activate#(n__0()) -> c_10(0#())
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
activate#(n__s(X)) -> c_14(s#(X))
and#(X1,X2) -> c_15()
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__0()) -> c_17()
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(X) -> c_20()
isNatKind#(n__0()) -> c_21()
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_24()
s#(X) -> c_25()
Weak DPs
and mark the set of starting terms.
* Step 3: UsableRules MAYBE
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U13#(tt()) -> c_4()
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U22#(tt()) -> c_6()
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(X) -> c_9()
activate#(n__0()) -> c_10(0#())
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
activate#(n__s(X)) -> c_14(s#(X))
and#(X1,X2) -> c_15()
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__0()) -> c_17()
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(X) -> c_20()
isNatKind#(n__0()) -> c_21()
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_24()
s#(X) -> c_25()
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
U31(tt(),N) -> activate(N)
U41(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U13#(tt()) -> c_4()
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U22#(tt()) -> c_6()
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(X) -> c_9()
activate#(n__0()) -> c_10(0#())
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
activate#(n__s(X)) -> c_14(s#(X))
and#(X1,X2) -> c_15()
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__0()) -> c_17()
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(X) -> c_20()
isNatKind#(n__0()) -> c_21()
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_24()
s#(X) -> c_25()
* Step 4: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U13#(tt()) -> c_4()
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U22#(tt()) -> c_6()
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(X) -> c_9()
activate#(n__0()) -> c_10(0#())
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
activate#(n__s(X)) -> c_14(s#(X))
and#(X1,X2) -> c_15()
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__0()) -> c_17()
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(X) -> c_20()
isNatKind#(n__0()) -> c_21()
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_24()
s#(X) -> c_25()
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,4,6,9,15,17,20,21,24,25}
by application of
Pre({1,4,6,9,15,17,20,21,24,25}) = {2,3,5,7,8,10,11,12,13,14,16,18,19,22,23}.
Here rules are labelled as follows:
1: 0#() -> c_1()
2: U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
3: U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
4: U13#(tt()) -> c_4()
5: U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
6: U22#(tt()) -> c_6()
7: U31#(tt(),N) -> c_7(activate#(N))
8: U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
9: activate#(X) -> c_9()
10: activate#(n__0()) -> c_10(0#())
11: activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
12: activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
13: activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
14: activate#(n__s(X)) -> c_14(s#(X))
15: and#(X1,X2) -> c_15()
16: and#(tt(),X) -> c_16(activate#(X))
17: isNat#(n__0()) -> c_17()
18: isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
19: isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
20: isNatKind#(X) -> c_20()
21: isNatKind#(n__0()) -> c_21()
22: isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
23: isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
24: plus#(X1,X2) -> c_24()
25: s#(X) -> c_25()
* Step 5: PredecessorEstimation MAYBE
+ Considered Problem:
- Strict DPs:
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(n__0()) -> c_10(0#())
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
activate#(n__s(X)) -> c_14(s#(X))
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
- Weak DPs:
0#() -> c_1()
U13#(tt()) -> c_4()
U22#(tt()) -> c_6()
activate#(X) -> c_9()
and#(X1,X2) -> c_15()
isNat#(n__0()) -> c_17()
isNatKind#(X) -> c_20()
isNatKind#(n__0()) -> c_21()
plus#(X1,X2) -> c_24()
s#(X) -> c_25()
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{6,9,10}
by application of
Pre({6,9,10}) = {1,2,3,4,5,11,12,13,14,15}.
Here rules are labelled as follows:
1: U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
2: U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
3: U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
4: U31#(tt(),N) -> c_7(activate#(N))
5: U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
6: activate#(n__0()) -> c_10(0#())
7: activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
8: activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
9: activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
10: activate#(n__s(X)) -> c_14(s#(X))
11: and#(tt(),X) -> c_16(activate#(X))
12: isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
13: isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
14: isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
15: isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
16: 0#() -> c_1()
17: U13#(tt()) -> c_4()
18: U22#(tt()) -> c_6()
19: activate#(X) -> c_9()
20: and#(X1,X2) -> c_15()
21: isNat#(n__0()) -> c_17()
22: isNatKind#(X) -> c_20()
23: isNatKind#(n__0()) -> c_21()
24: plus#(X1,X2) -> c_24()
25: s#(X) -> c_25()
* Step 6: RemoveWeakSuffixes MAYBE
+ Considered Problem:
- Strict DPs:
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
- Weak DPs:
0#() -> c_1()
U13#(tt()) -> c_4()
U22#(tt()) -> c_6()
activate#(X) -> c_9()
activate#(n__0()) -> c_10(0#())
activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
activate#(n__s(X)) -> c_14(s#(X))
and#(X1,X2) -> c_15()
isNat#(n__0()) -> c_17()
isNatKind#(X) -> c_20()
isNatKind#(n__0()) -> c_21()
plus#(X1,X2) -> c_24()
s#(X) -> c_25()
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
-->_4 activate#(n__s(X)) -> c_14(s#(X)):19
-->_3 activate#(n__s(X)) -> c_14(s#(X)):19
-->_4 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_3 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_4 activate#(n__0()) -> c_10(0#()):17
-->_3 activate#(n__0()) -> c_10(0#()):17
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):2
-->_2 isNat#(n__0()) -> c_17():21
-->_4 activate#(X) -> c_9():16
-->_3 activate#(X) -> c_9():16
2:S:U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
-->_3 activate#(n__s(X)) -> c_14(s#(X)):19
-->_3 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_3 activate#(n__0()) -> c_10(0#()):17
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_2 isNat#(n__0()) -> c_17():21
-->_3 activate#(X) -> c_9():16
-->_1 U13#(tt()) -> c_4():14
3:S:U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
-->_3 activate#(n__s(X)) -> c_14(s#(X)):19
-->_3 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_3 activate#(n__0()) -> c_10(0#()):17
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_2 isNat#(n__0()) -> c_17():21
-->_3 activate#(X) -> c_9():16
-->_1 U22#(tt()) -> c_6():15
4:S:U31#(tt(),N) -> c_7(activate#(N))
-->_1 activate#(n__s(X)) -> c_14(s#(X)):19
-->_1 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_1 activate#(n__0()) -> c_10(0#()):17
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 activate#(X) -> c_9():16
5:S:U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
-->_4 activate#(n__s(X)) -> c_14(s#(X)):19
-->_3 activate#(n__s(X)) -> c_14(s#(X)):19
-->_4 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_3 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_4 activate#(n__0()) -> c_10(0#()):17
-->_3 activate#(n__0()) -> c_10(0#()):17
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 s#(X) -> c_25():25
-->_2 plus#(X1,X2) -> c_24():24
-->_4 activate#(X) -> c_9():16
-->_3 activate#(X) -> c_9():16
6:S:activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
-->_1 and#(tt(),X) -> c_16(activate#(X)):8
-->_1 and#(X1,X2) -> c_15():20
7:S:activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
-->_1 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_1 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_1 isNatKind#(n__0()) -> c_21():23
-->_1 isNatKind#(X) -> c_20():22
8:S:and#(tt(),X) -> c_16(activate#(X))
-->_1 activate#(n__s(X)) -> c_14(s#(X)):19
-->_1 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_1 activate#(n__0()) -> c_10(0#()):17
-->_1 activate#(X) -> c_9():16
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
9:S:isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
-->_7 activate#(n__s(X)) -> c_14(s#(X)):19
-->_6 activate#(n__s(X)) -> c_14(s#(X)):19
-->_5 activate#(n__s(X)) -> c_14(s#(X)):19
-->_4 activate#(n__s(X)) -> c_14(s#(X)):19
-->_7 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_6 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_5 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_4 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_7 activate#(n__0()) -> c_10(0#()):17
-->_6 activate#(n__0()) -> c_10(0#()):17
-->_5 activate#(n__0()) -> c_10(0#()):17
-->_4 activate#(n__0()) -> c_10(0#()):17
-->_3 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_3 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_3 isNatKind#(n__0()) -> c_21():23
-->_3 isNatKind#(X) -> c_20():22
-->_2 and#(X1,X2) -> c_15():20
-->_7 activate#(X) -> c_9():16
-->_6 activate#(X) -> c_9():16
-->_5 activate#(X) -> c_9():16
-->_4 activate#(X) -> c_9():16
-->_2 and#(tt(),X) -> c_16(activate#(X)):8
-->_7 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_6 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_5 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_7 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_6 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_5 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2)):1
10:S:isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
-->_4 activate#(n__s(X)) -> c_14(s#(X)):19
-->_3 activate#(n__s(X)) -> c_14(s#(X)):19
-->_4 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_3 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_4 activate#(n__0()) -> c_10(0#()):17
-->_3 activate#(n__0()) -> c_10(0#()):17
-->_2 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_2 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_2 isNatKind#(n__0()) -> c_21():23
-->_2 isNatKind#(X) -> c_20():22
-->_4 activate#(X) -> c_9():16
-->_3 activate#(X) -> c_9():16
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)):3
11:S:isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
-->_4 activate#(n__s(X)) -> c_14(s#(X)):19
-->_3 activate#(n__s(X)) -> c_14(s#(X)):19
-->_4 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_3 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_4 activate#(n__0()) -> c_10(0#()):17
-->_3 activate#(n__0()) -> c_10(0#()):17
-->_2 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_2 isNatKind#(n__0()) -> c_21():23
-->_2 isNatKind#(X) -> c_20():22
-->_1 and#(X1,X2) -> c_15():20
-->_4 activate#(X) -> c_9():16
-->_3 activate#(X) -> c_9():16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_1 and#(tt(),X) -> c_16(activate#(X)):8
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
12:S:isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
-->_2 activate#(n__s(X)) -> c_14(s#(X)):19
-->_2 activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2)):18
-->_2 activate#(n__0()) -> c_10(0#()):17
-->_1 isNatKind#(n__0()) -> c_21():23
-->_1 isNatKind#(X) -> c_20():22
-->_2 activate#(X) -> c_9():16
-->_1 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_1 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_2 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_2 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
13:W:0#() -> c_1()
14:W:U13#(tt()) -> c_4()
15:W:U22#(tt()) -> c_6()
16:W:activate#(X) -> c_9()
17:W:activate#(n__0()) -> c_10(0#())
-->_1 0#() -> c_1():13
18:W:activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
-->_1 plus#(X1,X2) -> c_24():24
19:W:activate#(n__s(X)) -> c_14(s#(X))
-->_1 s#(X) -> c_25():25
20:W:and#(X1,X2) -> c_15()
21:W:isNat#(n__0()) -> c_17()
22:W:isNatKind#(X) -> c_20()
23:W:isNatKind#(n__0()) -> c_21()
24:W:plus#(X1,X2) -> c_24()
25:W:s#(X) -> c_25()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
14: U13#(tt()) -> c_4()
15: U22#(tt()) -> c_6()
21: isNat#(n__0()) -> c_17()
20: and#(X1,X2) -> c_15()
16: activate#(X) -> c_9()
22: isNatKind#(X) -> c_20()
23: isNatKind#(n__0()) -> c_21()
17: activate#(n__0()) -> c_10(0#())
13: 0#() -> c_1()
18: activate#(n__plus(X1,X2)) -> c_13(plus#(X1,X2))
24: plus#(X1,X2) -> c_24()
19: activate#(n__s(X)) -> c_14(s#(X))
25: s#(X) -> c_25()
* Step 7: SimplifyRHS MAYBE
+ Considered Problem:
- Strict DPs:
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/3,c_4/0,c_5/3,c_6/0,c_7/1,c_8/4,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):2
2:S:U12#(tt(),V2) -> c_3(U13#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
3:S:U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
4:S:U31#(tt(),N) -> c_7(activate#(N))
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
5:S:U41#(tt(),M,N) -> c_8(s#(plus(activate(N),activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
6:S:activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
-->_1 and#(tt(),X) -> c_16(activate#(X)):8
7:S:activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
-->_1 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_1 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
8:S:and#(tt(),X) -> c_16(activate#(X))
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
9:S:isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
-->_3 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_3 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_2 and#(tt(),X) -> c_16(activate#(X)):8
-->_7 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_6 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_5 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_7 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_6 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_5 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2)):1
10:S:isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
-->_2 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_2 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U21#(tt(),V1) -> c_5(U22#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)):3
11:S:isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_2 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_1 and#(tt(),X) -> c_16(activate#(X)):8
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
12:S:isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
-->_1 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_1 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_2 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_2 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
U12#(tt(),V2) -> c_3(isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1))
U41#(tt(),M,N) -> c_8(activate#(N),activate#(M))
* Step 8: RemoveHeads MAYBE
+ Considered Problem:
- Strict DPs:
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1))
U31#(tt(),N) -> c_7(activate#(N))
U41#(tt(),M,N) -> c_8(activate#(N),activate#(M))
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/2,c_4/0,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
RemoveHeads
+ Details:
Consider the dependency graph
1:S:U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
-->_2 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_2 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U12#(tt(),V2) -> c_3(isNat#(activate(V2)),activate#(V2)):2
2:S:U12#(tt(),V2) -> c_3(isNat#(activate(V2)),activate#(V2))
-->_1 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_1 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_2 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_2 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
3:S:U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1))
-->_1 isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)):10
-->_1 isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2)):9
-->_2 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_2 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
4:S:U31#(tt(),N) -> c_7(activate#(N))
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
5:S:U41#(tt(),M,N) -> c_8(activate#(N),activate#(M))
-->_2 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_2 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
6:S:activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
-->_1 and#(tt(),X) -> c_16(activate#(X)):8
7:S:activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
-->_1 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_1 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
8:S:and#(tt(),X) -> c_16(activate#(X))
-->_1 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_1 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
9:S:isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
-->_3 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_3 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_2 and#(tt(),X) -> c_16(activate#(X)):8
-->_7 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_6 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_5 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_7 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_6 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_5 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2)):1
10:S:isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
-->_2 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_2 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_1 U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1)):3
11:S:isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_2 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_1 and#(tt(),X) -> c_16(activate#(X)):8
-->_4 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_3 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_4 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
-->_3 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
12:S:isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
-->_1 isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1)):12
-->_1 isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)):11
-->_2 activate#(n__isNatKind(X)) -> c_12(isNatKind#(X)):7
-->_2 activate#(n__and(X1,X2)) -> c_11(and#(X1,X2)):6
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).
[(4,U31#(tt(),N) -> c_7(activate#(N))),(5,U41#(tt(),M,N) -> c_8(activate#(N),activate#(M)))]
* Step 9: Failure MAYBE
+ Considered Problem:
- Strict DPs:
U11#(tt(),V1,V2) -> c_2(U12#(isNat(activate(V1)),activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
U12#(tt(),V2) -> c_3(isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_5(isNat#(activate(V1)),activate#(V1))
activate#(n__and(X1,X2)) -> c_11(and#(X1,X2))
activate#(n__isNatKind(X)) -> c_12(isNatKind#(X))
and#(tt(),X) -> c_16(activate#(X))
isNat#(n__plus(V1,V2)) -> c_18(U11#(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
,and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2)
,activate#(V1)
,activate#(V2))
isNat#(n__s(V1)) -> c_19(U21#(isNatKind(activate(V1)),activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_22(and#(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
isNatKind#(n__s(V1)) -> c_23(isNatKind#(activate(V1)),activate#(V1))
- Weak TRS:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNat(activate(V1)),activate(V2))
U12(tt(),V2) -> U13(isNat(activate(V2)))
U13(tt()) -> tt()
U21(tt(),V1) -> U22(isNat(activate(V1)))
U22(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__and(X1,X2)) -> and(X1,X2)
activate(n__isNatKind(X)) -> isNatKind(X)
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
and(X1,X2) -> n__and(X1,X2)
and(tt(),X) -> activate(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
,activate(V1)
,activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(X) -> n__isNatKind(X)
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> and(isNatKind(activate(V1)),n__isNatKind(activate(V2)))
isNatKind(n__s(V1)) -> isNatKind(activate(V1))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
- Signature:
{0/0,U11/3,U12/2,U13/1,U21/2,U22/1,U31/2,U41/3,activate/1,and/2,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3
,U12#/2,U13#/1,U21#/2,U22#/1,U31#/2,U41#/3,activate#/1,and#/2,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0
,n__and/2,n__isNatKind/1,n__plus/2,n__s/1,tt/0,c_1/0,c_2/4,c_3/2,c_4/0,c_5/2,c_6/0,c_7/1,c_8/2,c_9/0,c_10/1
,c_11/1,c_12/1,c_13/1,c_14/1,c_15/0,c_16/1,c_17/0,c_18/7,c_19/4,c_20/0,c_21/0,c_22/4,c_23/2,c_24/0,c_25/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {0#,U11#,U12#,U13#,U21#,U22#,U31#,U41#,activate#,and#
,isNat#,isNatKind#,plus#,s#} and constructors {n__0,n__and,n__isNatKind,n__plus,n__s,tt}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE