*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
U52(tt(),N) -> activate(N)
U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(N,0()) -> U51(isNat(N),N)
plus(N,s(M)) -> U61(isNat(M),M,N)
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1} / {n__0/0,n__plus/2,n__s/1,tt/0}
Obligation:
Innermost
basic terms: {0,U11,U12,U13,U14,U15,U16,U21,U22,U23,U31,U32,U41,U51,U52,U61,U62,U63,U64,activate,isNat,isNatKind,plus,s}/{n__0,n__plus,n__s,tt}
Applied Processor:
InnermostRuleRemoval
Proof:
Arguments of following rules are not normal-forms.
plus(N,0()) -> U51(isNat(N),N)
plus(N,s(M)) -> U61(isNat(M),M,N)
All above mentioned rules can be savely removed.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
U52(tt(),N) -> activate(N)
U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Weak DP Rules:
Weak TRS Rules:
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1} / {n__0/0,n__plus/2,n__s/1,tt/0}
Obligation:
Innermost
basic terms: {0,U11,U12,U13,U14,U15,U16,U21,U22,U23,U31,U32,U41,U51,U52,U61,U62,U63,U64,activate,isNat,isNatKind,plus,s}/{n__0,n__plus,n__s,tt}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following dependency tuples:
Strict DPs
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U16#(tt()) -> c_7()
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U23#(tt()) -> c_10()
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U52#(tt(),N) -> c_15(activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
activate#(X) -> c_20()
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__0()) -> c_24()
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__0()) -> c_27()
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
Weak DPs
and mark the set of starting terms.
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U16#(tt()) -> c_7()
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U23#(tt()) -> c_10()
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U52#(tt(),N) -> c_15(activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
activate#(X) -> c_20()
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__0()) -> c_24()
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__0()) -> c_27()
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
U51(tt(),N) -> U52(isNatKind(activate(N)),activate(N))
U52(tt(),N) -> activate(N)
U61(tt(),M,N) -> U62(isNatKind(activate(M)),activate(M),activate(N))
U62(tt(),M,N) -> U63(isNat(activate(N)),activate(M),activate(N))
U63(tt(),M,N) -> U64(isNatKind(activate(N)),activate(M),activate(N))
U64(tt(),M,N) -> s(plus(activate(N),activate(M)))
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/5,c_3/5,c_4/5,c_5/4,c_6/3,c_7/0,c_8/4,c_9/3,c_10/0,c_11/3,c_12/0,c_13/0,c_14/4,c_15/1,c_16/5,c_17/5,c_18/5,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/5,c_26/4,c_27/0,c_28/4,c_29/3,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(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#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U16#(tt()) -> c_7()
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U23#(tt()) -> c_10()
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U52#(tt(),N) -> c_15(activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
activate#(X) -> c_20()
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__0()) -> c_24()
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__0()) -> c_27()
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
0#() -> c_1()
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U16#(tt()) -> c_7()
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U23#(tt()) -> c_10()
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U52#(tt(),N) -> c_15(activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
activate#(X) -> c_20()
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__0()) -> c_24()
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__0()) -> c_27()
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/5,c_3/5,c_4/5,c_5/4,c_6/3,c_7/0,c_8/4,c_9/3,c_10/0,c_11/3,c_12/0,c_13/0,c_14/4,c_15/1,c_16/5,c_17/5,c_18/5,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/5,c_26/4,c_27/0,c_28/4,c_29/3,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1,7,10,12,13,20,24,27,30,31}
by application of
Pre({1,7,10,12,13,20,24,27,30,31}) = {2,3,4,5,6,8,9,11,14,15,16,17,18,19,21,22,23,25,26,28,29}.
Here rules are labelled as follows:
1: 0#() -> c_1()
2: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)
,activate#(V2))
3: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2))
,activate#(V2)
,activate#(V1)
,activate#(V2))
4: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2))
,activate#(V2)
,activate#(V1)
,activate#(V2))
5: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
6: U15#(tt(),V2) ->
c_6(U16#(isNat(activate(V2)))
,isNat#(activate(V2))
,activate#(V2))
7: U16#(tt()) -> c_7()
8: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
9: U22#(tt(),V1) ->
c_9(U23#(isNat(activate(V1)))
,isNat#(activate(V1))
,activate#(V1))
10: U23#(tt()) -> c_10()
11: U31#(tt(),V2) ->
c_11(U32#(isNatKind(activate(V2)))
,isNatKind#(activate(V2))
,activate#(V2))
12: U32#(tt()) -> c_12()
13: U41#(tt()) -> c_13()
14: U51#(tt(),N) ->
c_14(U52#(isNatKind(activate(N))
,activate(N))
,isNatKind#(activate(N))
,activate#(N)
,activate#(N))
15: U52#(tt(),N) ->
c_15(activate#(N))
16: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M))
,activate#(M)
,activate#(M)
,activate#(N))
17: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N))
,activate#(N)
,activate#(M)
,activate#(N))
18: U63#(tt(),M,N) ->
c_18(U64#(isNatKind(activate(N))
,activate(M)
,activate(N))
,isNatKind#(activate(N))
,activate#(N)
,activate#(M)
,activate#(N))
19: U64#(tt(),M,N) ->
c_19(s#(plus(activate(N)
,activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
20: activate#(X) -> c_20()
21: activate#(n__0()) -> c_21(0#())
22: activate#(n__plus(X1,X2)) ->
c_22(plus#(X1,X2))
23: activate#(n__s(X)) ->
c_23(s#(X))
24: isNat#(n__0()) -> c_24()
25: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)
,activate#(V2))
26: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
27: isNatKind#(n__0()) -> c_27()
28: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
29: isNatKind#(n__s(V1)) ->
c_29(U41#(isNatKind(activate(V1)))
,isNatKind#(activate(V1))
,activate#(V1))
30: plus#(X1,X2) -> c_30()
31: s#(X) -> c_31()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U52#(tt(),N) -> c_15(activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
Strict TRS Rules:
Weak DP Rules:
0#() -> c_1()
U16#(tt()) -> c_7()
U23#(tt()) -> c_10()
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
activate#(X) -> c_20()
isNat#(n__0()) -> c_24()
isNatKind#(n__0()) -> c_27()
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/5,c_3/5,c_4/5,c_5/4,c_6/3,c_7/0,c_8/4,c_9/3,c_10/0,c_11/3,c_12/0,c_13/0,c_14/4,c_15/1,c_16/5,c_17/5,c_18/5,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/5,c_26/4,c_27/0,c_28/4,c_29/3,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{15,16,17}
by application of
Pre({15,16,17}) = {1,2,3,4,5,6,7,8,9,10,11,12,13,14,18,19,20,21}.
Here rules are labelled as follows:
1: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)
,activate#(V2))
2: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2))
,activate#(V2)
,activate#(V1)
,activate#(V2))
3: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2))
,activate#(V2)
,activate#(V1)
,activate#(V2))
4: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
5: U15#(tt(),V2) ->
c_6(U16#(isNat(activate(V2)))
,isNat#(activate(V2))
,activate#(V2))
6: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
7: U22#(tt(),V1) ->
c_9(U23#(isNat(activate(V1)))
,isNat#(activate(V1))
,activate#(V1))
8: U31#(tt(),V2) ->
c_11(U32#(isNatKind(activate(V2)))
,isNatKind#(activate(V2))
,activate#(V2))
9: U51#(tt(),N) ->
c_14(U52#(isNatKind(activate(N))
,activate(N))
,isNatKind#(activate(N))
,activate#(N)
,activate#(N))
10: U52#(tt(),N) ->
c_15(activate#(N))
11: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M))
,activate#(M)
,activate#(M)
,activate#(N))
12: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N))
,activate#(N)
,activate#(M)
,activate#(N))
13: U63#(tt(),M,N) ->
c_18(U64#(isNatKind(activate(N))
,activate(M)
,activate(N))
,isNatKind#(activate(N))
,activate#(N)
,activate#(M)
,activate#(N))
14: U64#(tt(),M,N) ->
c_19(s#(plus(activate(N)
,activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
15: activate#(n__0()) -> c_21(0#())
16: activate#(n__plus(X1,X2)) ->
c_22(plus#(X1,X2))
17: activate#(n__s(X)) ->
c_23(s#(X))
18: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)
,activate#(V2))
19: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
20: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
21: isNatKind#(n__s(V1)) ->
c_29(U41#(isNatKind(activate(V1)))
,isNatKind#(activate(V1))
,activate#(V1))
22: 0#() -> c_1()
23: U16#(tt()) -> c_7()
24: U23#(tt()) -> c_10()
25: U32#(tt()) -> c_12()
26: U41#(tt()) -> c_13()
27: activate#(X) -> c_20()
28: isNat#(n__0()) -> c_24()
29: isNatKind#(n__0()) -> c_27()
30: plus#(X1,X2) -> c_30()
31: s#(X) -> c_31()
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U52#(tt(),N) -> c_15(activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
Strict TRS Rules:
Weak DP Rules:
0#() -> c_1()
U16#(tt()) -> c_7()
U23#(tt()) -> c_10()
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
activate#(X) -> c_20()
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__0()) -> c_24()
isNatKind#(n__0()) -> c_27()
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/5,c_3/5,c_4/5,c_5/4,c_6/3,c_7/0,c_8/4,c_9/3,c_10/0,c_11/3,c_12/0,c_13/0,c_14/4,c_15/1,c_16/5,c_17/5,c_18/5,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/5,c_26/4,c_27/0,c_28/4,c_29/3,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{10,14}
by application of
Pre({10,14}) = {9,13}.
Here rules are labelled as follows:
1: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)
,activate#(V2))
2: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2))
,activate#(V2)
,activate#(V1)
,activate#(V2))
3: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2))
,activate#(V2)
,activate#(V1)
,activate#(V2))
4: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1))
,activate#(V1)
,activate#(V2))
5: U15#(tt(),V2) ->
c_6(U16#(isNat(activate(V2)))
,isNat#(activate(V2))
,activate#(V2))
6: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
7: U22#(tt(),V1) ->
c_9(U23#(isNat(activate(V1)))
,isNat#(activate(V1))
,activate#(V1))
8: U31#(tt(),V2) ->
c_11(U32#(isNatKind(activate(V2)))
,isNatKind#(activate(V2))
,activate#(V2))
9: U51#(tt(),N) ->
c_14(U52#(isNatKind(activate(N))
,activate(N))
,isNatKind#(activate(N))
,activate#(N)
,activate#(N))
10: U52#(tt(),N) ->
c_15(activate#(N))
11: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M))
,activate#(M)
,activate#(M)
,activate#(N))
12: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N))
,activate#(N)
,activate#(M)
,activate#(N))
13: U63#(tt(),M,N) ->
c_18(U64#(isNatKind(activate(N))
,activate(M)
,activate(N))
,isNatKind#(activate(N))
,activate#(N)
,activate#(M)
,activate#(N))
14: U64#(tt(),M,N) ->
c_19(s#(plus(activate(N)
,activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
15: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1)
,activate#(V2))
16: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V1))
17: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1))
,activate#(V1)
,activate#(V2))
18: isNatKind#(n__s(V1)) ->
c_29(U41#(isNatKind(activate(V1)))
,isNatKind#(activate(V1))
,activate#(V1))
19: 0#() -> c_1()
20: U16#(tt()) -> c_7()
21: U23#(tt()) -> c_10()
22: U32#(tt()) -> c_12()
23: U41#(tt()) -> c_13()
24: activate#(X) -> c_20()
25: activate#(n__0()) -> c_21(0#())
26: activate#(n__plus(X1,X2)) ->
c_22(plus#(X1,X2))
27: activate#(n__s(X)) ->
c_23(s#(X))
28: isNat#(n__0()) -> c_24()
29: isNatKind#(n__0()) -> c_27()
30: plus#(X1,X2) -> c_30()
31: s#(X) -> c_31()
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
Strict TRS Rules:
Weak DP Rules:
0#() -> c_1()
U16#(tt()) -> c_7()
U23#(tt()) -> c_10()
U32#(tt()) -> c_12()
U41#(tt()) -> c_13()
U52#(tt(),N) -> c_15(activate#(N))
U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
activate#(X) -> c_20()
activate#(n__0()) -> c_21(0#())
activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
activate#(n__s(X)) -> c_23(s#(X))
isNat#(n__0()) -> c_24()
isNatKind#(n__0()) -> c_27()
plus#(X1,X2) -> c_30()
s#(X) -> c_31()
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/5,c_3/5,c_4/5,c_5/4,c_6/3,c_7/0,c_8/4,c_9/3,c_10/0,c_11/3,c_12/0,c_13/0,c_14/4,c_15/1,c_16/5,c_17/5,c_18/5,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/5,c_26/4,c_27/0,c_28/4,c_29/3,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2)):2
-->_2 isNatKind#(n__0()) -> c_27():29
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
2:S:U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2)):3
-->_2 isNatKind#(n__0()) -> c_27():29
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
3:S:U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2)):4
-->_2 isNatKind#(n__0()) -> c_27():29
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
4:S:U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
-->_1 U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):5
-->_2 isNat#(n__0()) -> c_24():28
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
5:S:U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
-->_2 isNat#(n__0()) -> c_24():28
-->_3 activate#(X) -> c_20():24
-->_1 U16#(tt()) -> c_7():18
6:S:U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)):7
-->_2 isNatKind#(n__0()) -> c_27():29
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
7:S:U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
-->_2 isNat#(n__0()) -> c_24():28
-->_3 activate#(X) -> c_20():24
-->_1 U23#(tt()) -> c_10():19
8:S:U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_2 isNatKind#(n__0()) -> c_27():29
-->_3 activate#(X) -> c_20():24
-->_1 U32#(tt()) -> c_12():20
9:S:U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_1 U52#(tt(),N) -> c_15(activate#(N)):22
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_2 isNatKind#(n__0()) -> c_27():29
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
10:S:U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N)):11
-->_2 isNatKind#(n__0()) -> c_27():29
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
11:S:U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
-->_1 U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N)):12
-->_2 isNat#(n__0()) -> c_24():28
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
12:S:U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_1 U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M)):23
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_2 isNatKind#(n__0()) -> c_27():29
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
13:S:isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
-->_5 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_5 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_5 activate#(n__0()) -> c_21(0#()):25
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_2 isNatKind#(n__0()) -> c_27():29
-->_5 activate#(X) -> c_20():24
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):1
14:S:isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_2 isNatKind#(n__0()) -> c_27():29
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
-->_1 U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):6
15:S:isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__0()) -> c_27():29
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2)):8
16:S:isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_2 isNatKind#(n__0()) -> c_27():29
-->_3 activate#(X) -> c_20():24
-->_1 U41#(tt()) -> c_13():21
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
17:W:0#() -> c_1()
18:W:U16#(tt()) -> c_7()
19:W:U23#(tt()) -> c_10()
20:W:U32#(tt()) -> c_12()
21:W:U41#(tt()) -> c_13()
22:W:U52#(tt(),N) -> c_15(activate#(N))
-->_1 activate#(n__s(X)) -> c_23(s#(X)):27
-->_1 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_1 activate#(n__0()) -> c_21(0#()):25
-->_1 activate#(X) -> c_20():24
23:W:U64#(tt(),M,N) -> c_19(s#(plus(activate(N),activate(M))),plus#(activate(N),activate(M)),activate#(N),activate#(M))
-->_4 activate#(n__s(X)) -> c_23(s#(X)):27
-->_3 activate#(n__s(X)) -> c_23(s#(X)):27
-->_4 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_3 activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2)):26
-->_4 activate#(n__0()) -> c_21(0#()):25
-->_3 activate#(n__0()) -> c_21(0#()):25
-->_1 s#(X) -> c_31():31
-->_2 plus#(X1,X2) -> c_30():30
-->_4 activate#(X) -> c_20():24
-->_3 activate#(X) -> c_20():24
24:W:activate#(X) -> c_20()
25:W:activate#(n__0()) -> c_21(0#())
-->_1 0#() -> c_1():17
26:W:activate#(n__plus(X1,X2)) -> c_22(plus#(X1,X2))
-->_1 plus#(X1,X2) -> c_30():30
27:W:activate#(n__s(X)) -> c_23(s#(X))
-->_1 s#(X) -> c_31():31
28:W:isNat#(n__0()) -> c_24()
29:W:isNatKind#(n__0()) -> c_27()
30:W:plus#(X1,X2) -> c_30()
31:W:s#(X) -> c_31()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
23: U64#(tt(),M,N) ->
c_19(s#(plus(activate(N)
,activate(M)))
,plus#(activate(N),activate(M))
,activate#(N)
,activate#(M))
22: U52#(tt(),N) ->
c_15(activate#(N))
18: U16#(tt()) -> c_7()
19: U23#(tt()) -> c_10()
28: isNat#(n__0()) -> c_24()
20: U32#(tt()) -> c_12()
21: U41#(tt()) -> c_13()
24: activate#(X) -> c_20()
29: isNatKind#(n__0()) -> c_27()
25: activate#(n__0()) -> c_21(0#())
17: 0#() -> c_1()
26: activate#(n__plus(X1,X2)) ->
c_22(plus#(X1,X2))
30: plus#(X1,X2) -> c_30()
27: activate#(n__s(X)) ->
c_23(s#(X))
31: s#(X) -> c_31()
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/5,c_3/5,c_4/5,c_5/4,c_6/3,c_7/0,c_8/4,c_9/3,c_10/0,c_11/3,c_12/0,c_13/0,c_14/4,c_15/1,c_16/5,c_17/5,c_18/5,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/5,c_26/4,c_27/0,c_28/4,c_29/3,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2)):2
2:S:U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2)):3
3:S:U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)),activate#(V2),activate#(V1),activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2)):4
4:S:U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)),activate#(V1),activate#(V2))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
-->_1 U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2)):5
5:S:U15#(tt(),V2) -> c_6(U16#(isNat(activate(V2))),isNat#(activate(V2)),activate#(V2))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
6:S:U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1)):7
7:S:U22#(tt(),V1) -> c_9(U23#(isNat(activate(V1))),isNat#(activate(V1)),activate#(V1))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
8:S:U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
9:S:U51#(tt(),N) -> c_14(U52#(isNatKind(activate(N)),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(N))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
10:S:U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)),activate#(M),activate#(M),activate#(N))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N)):11
11:S:U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)),activate#(N),activate#(M),activate#(N))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):13
-->_1 U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N)):12
12:S:U63#(tt(),M,N) -> c_18(U64#(isNatKind(activate(N)),activate(M),activate(N)),isNatKind#(activate(N)),activate#(N),activate#(M),activate#(N))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
13:S:isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V1),activate#(V2)):1
14:S:isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)),activate#(V1),activate#(V1)):6
15:S:isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
-->_1 U31#(tt(),V2) -> c_11(U32#(isNatKind(activate(V2))),isNatKind#(activate(V2)),activate#(V2)):8
16:S:isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1))
-->_2 isNatKind#(n__s(V1)) -> c_29(U41#(isNatKind(activate(V1))),isNatKind#(activate(V1)),activate#(V1)):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)),activate#(V1),activate#(V2)):15
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,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(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Problem (S)
Strict DP Rules:
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
8: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
Consider the set of all dependency pairs
1: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
2: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
3: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
4: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
5: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
6: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
7: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
8: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
9: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
10: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
11: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
12: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
13: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
14: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
15: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{8,16}
These cover all (indirect) predecessors of dependency pairs
{8,9,10,11,12,16}
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 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, 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 polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1,2},
uargs(c_5) = {1,2},
uargs(c_6) = {1},
uargs(c_8) = {1,2},
uargs(c_9) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1},
uargs(c_16) = {1,2},
uargs(c_17) = {1,2},
uargs(c_18) = {1},
uargs(c_25) = {1,2},
uargs(c_26) = {1,2},
uargs(c_28) = {1,2},
uargs(c_29) = {1}
Following symbols are considered usable:
{0,U31,U32,U41,activate,isNatKind,plus,s,0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}
TcT has computed the following interpretation:
p(0) = 1
p(U11) = x1*x3 + x3^2
p(U12) = 1 + x1 + x1*x3
p(U13) = x2 + x2*x3 + x3 + x3^2
p(U14) = x1*x3 + x2^2
p(U15) = x1 + x1^2
p(U16) = 1
p(U21) = 0
p(U22) = x1
p(U23) = 0
p(U31) = x1 + x2
p(U32) = 1 + x1
p(U41) = 1 + x1
p(U51) = 0
p(U52) = 0
p(U61) = 0
p(U62) = 0
p(U63) = 0
p(U64) = 0
p(activate) = x1
p(isNat) = 1
p(isNatKind) = x1
p(n__0) = 1
p(n__plus) = 1 + x1 + x2
p(n__s) = 1 + x1
p(plus) = 1 + x1 + x2
p(s) = 1 + x1
p(tt) = 1
p(0#) = 0
p(U11#) = 1 + x2 + x2*x3 + x2^2 + x3 + x3^2
p(U12#) = 1 + x1*x3 + x2^2 + x3 + x3^2
p(U13#) = x2^2 + x3 + x3^2
p(U14#) = x2^2 + x3^2
p(U15#) = x2^2
p(U16#) = 0
p(U21#) = x2 + x2^2
p(U22#) = x2^2
p(U23#) = 0
p(U31#) = 1 + x2
p(U32#) = 0
p(U41#) = 0
p(U51#) = x1*x2
p(U52#) = 0
p(U61#) = x1 + x1*x2 + x1^2 + x2 + x2*x3 + x2^2 + x3 + x3^2
p(U62#) = 1 + x1^2 + x2*x3 + x3 + x3^2
p(U63#) = 1 + x3
p(U64#) = 0
p(activate#) = 0
p(isNat#) = x1^2
p(isNatKind#) = x1
p(plus#) = 0
p(s#) = 0
p(c_1) = 0
p(c_2) = x1 + x2
p(c_3) = 1 + x1 + x2
p(c_4) = x1 + x2
p(c_5) = x1 + x2
p(c_6) = x1
p(c_7) = 0
p(c_8) = x1 + x2
p(c_9) = x1
p(c_10) = 0
p(c_11) = x1
p(c_12) = 0
p(c_13) = 0
p(c_14) = x1
p(c_15) = 0
p(c_16) = 1 + x1 + x2
p(c_17) = x1 + x2
p(c_18) = x1
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 0
p(c_23) = 0
p(c_24) = 0
p(c_25) = x1 + x2
p(c_26) = 1 + x1 + x2
p(c_27) = 0
p(c_28) = x1 + x2
p(c_29) = x1
p(c_30) = 0
p(c_31) = 0
Following rules are strictly oriented:
U31#(tt(),V2) = 1 + V2
> V2
= c_11(isNatKind#(activate(V2)))
isNatKind#(n__s(V1)) = 1 + V1
> V1
= c_29(isNatKind#(activate(V1)))
Following rules are (at-least) weakly oriented:
U11#(tt(),V1,V2) = 1 + V1 + V1*V2 + V1^2 + V2 + V2^2
>= 1 + V1 + V1*V2 + V1^2 + V2 + V2^2
= c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
U12#(tt(),V1,V2) = 1 + V1^2 + 2*V2 + V2^2
>= 1 + V1^2 + 2*V2 + V2^2
= c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
U13#(tt(),V1,V2) = V1^2 + V2 + V2^2
>= V1^2 + V2 + V2^2
= c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
U14#(tt(),V1,V2) = V1^2 + V2^2
>= V1^2 + V2^2
= c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
U15#(tt(),V2) = V2^2
>= V2^2
= c_6(isNat#(activate(V2)))
U21#(tt(),V1) = V1 + V1^2
>= V1 + V1^2
= c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
U22#(tt(),V1) = V1^2
>= V1^2
= c_9(isNat#(activate(V1)))
U51#(tt(),N) = N
>= N
= c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) = 2 + 2*M + M*N + M^2 + N + N^2
>= 2 + M + M*N + M^2 + N + N^2
= c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
U62#(tt(),M,N) = 2 + M*N + N + N^2
>= 1 + N + N^2
= c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
U63#(tt(),M,N) = 1 + N
>= N
= c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) = 1 + 2*V1 + 2*V1*V2 + V1^2 + 2*V2 + V2^2
>= 1 + 2*V1 + V1*V2 + V1^2 + V2 + V2^2
= c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
isNat#(n__s(V1)) = 1 + 2*V1 + V1^2
>= 1 + 2*V1 + V1^2
= c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) = 1 + V1 + V2
>= 1 + V1 + V2
= c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
0() = 1
>= 1
= n__0()
U31(tt(),V2) = 1 + V2
>= 1 + V2
= U32(isNatKind(activate(V2)))
U32(tt()) = 2
>= 1
= tt()
U41(tt()) = 2
>= 1
= tt()
activate(X) = X
>= X
= X
activate(n__0()) = 1
>= 1
= 0()
activate(n__plus(X1,X2)) = 1 + X1 + X2
>= 1 + X1 + X2
= plus(X1,X2)
activate(n__s(X)) = 1 + X
>= 1 + X
= s(X)
isNatKind(n__0()) = 1
>= 1
= tt()
isNatKind(n__plus(V1,V2)) = 1 + V1 + V2
>= V1 + V2
= U31(isNatKind(activate(V1))
,activate(V2))
isNatKind(n__s(V1)) = 1 + V1
>= 1 + V1
= U41(isNatKind(activate(V1)))
plus(X1,X2) = 1 + X1 + X2
>= 1 + X1 + X2
= n__plus(X1,X2)
s(X) = 1 + X
>= 1 + X
= n__s(X)
*** 1.1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
8: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
9: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
10: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
Consider the set of all dependency pairs
1: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
2: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
3: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
4: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
5: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
6: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
7: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
8: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
9: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
10: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
11: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
12: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
13: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
14: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
15: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{8,9,10}
These cover all (indirect) predecessors of dependency pairs
{1,2,3,4,5,6,7,8,9,10,11,12,13,14,15}
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.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, 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 polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_2) = {1,2},
uargs(c_3) = {1,2},
uargs(c_4) = {1,2},
uargs(c_5) = {1,2},
uargs(c_6) = {1},
uargs(c_8) = {1,2},
uargs(c_9) = {1},
uargs(c_11) = {1},
uargs(c_14) = {1},
uargs(c_16) = {1,2},
uargs(c_17) = {1,2},
uargs(c_18) = {1},
uargs(c_25) = {1,2},
uargs(c_26) = {1,2},
uargs(c_28) = {1,2},
uargs(c_29) = {1}
Following symbols are considered usable:
{0,U31,U32,U41,activate,isNatKind,plus,s,0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}
TcT has computed the following interpretation:
p(0) = 1
p(U11) = x1*x3
p(U12) = x1 + x1*x2 + x2^2
p(U13) = 1 + x1 + x3
p(U14) = x1*x2 + x1^2 + x2^2 + x3 + x3^2
p(U15) = 0
p(U16) = x1
p(U21) = x1 + x1*x2 + x2^2
p(U22) = x1^2
p(U23) = x1^2
p(U31) = x1
p(U32) = 1
p(U41) = 1
p(U51) = 0
p(U52) = 0
p(U61) = 0
p(U62) = 0
p(U63) = 0
p(U64) = 0
p(activate) = x1
p(isNat) = 0
p(isNatKind) = x1
p(n__0) = 1
p(n__plus) = 1 + x1 + x2
p(n__s) = 1 + x1
p(plus) = 1 + x1 + x2
p(s) = 1 + x1
p(tt) = 1
p(0#) = 0
p(U11#) = x1*x3 + x2 + x2*x3 + x2^2 + x3^2
p(U12#) = x1*x3 + x2^2 + x3 + x3^2
p(U13#) = x2^2 + x3 + x3^2
p(U14#) = x2^2 + x3^2
p(U15#) = x2^2
p(U16#) = 0
p(U21#) = x2 + x2^2
p(U22#) = x2^2
p(U23#) = 0
p(U31#) = x2
p(U32#) = 0
p(U41#) = 0
p(U51#) = x1 + x2
p(U52#) = 0
p(U61#) = 1 + x1 + x1*x2 + x1^2 + x2*x3 + x3^2
p(U62#) = 1 + x1*x3 + x3^2
p(U63#) = x3
p(U64#) = 0
p(activate#) = 0
p(isNat#) = x1^2
p(isNatKind#) = x1
p(plus#) = 0
p(s#) = 0
p(c_1) = 0
p(c_2) = x1 + x2
p(c_3) = x1 + x2
p(c_4) = x1 + x2
p(c_5) = x1 + x2
p(c_6) = x1
p(c_7) = 0
p(c_8) = x1 + x2
p(c_9) = x1
p(c_10) = 0
p(c_11) = x1
p(c_12) = 0
p(c_13) = 0
p(c_14) = x1
p(c_15) = 0
p(c_16) = 1 + x1 + x2
p(c_17) = x1 + x2
p(c_18) = x1
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 0
p(c_23) = 0
p(c_24) = 0
p(c_25) = x1 + x2
p(c_26) = x1 + x2
p(c_27) = 0
p(c_28) = x1 + x2
p(c_29) = 1 + x1
p(c_30) = 0
p(c_31) = 0
Following rules are strictly oriented:
isNat#(n__plus(V1,V2)) = 1 + 2*V1 + 2*V1*V2 + V1^2 + 2*V2 + V2^2
> 2*V1 + 2*V1*V2 + V1^2 + V2^2
= c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
isNat#(n__s(V1)) = 1 + 2*V1 + V1^2
> 2*V1 + V1^2
= c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) = 1 + V1 + V2
> V1 + V2
= c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
Following rules are (at-least) weakly oriented:
U11#(tt(),V1,V2) = V1 + V1*V2 + V1^2 + V2 + V2^2
>= V1 + V1*V2 + V1^2 + V2 + V2^2
= c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
U12#(tt(),V1,V2) = V1^2 + 2*V2 + V2^2
>= V1^2 + 2*V2 + V2^2
= c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
U13#(tt(),V1,V2) = V1^2 + V2 + V2^2
>= V1^2 + V2 + V2^2
= c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
U14#(tt(),V1,V2) = V1^2 + V2^2
>= V1^2 + V2^2
= c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
U15#(tt(),V2) = V2^2
>= V2^2
= c_6(isNat#(activate(V2)))
U21#(tt(),V1) = V1 + V1^2
>= V1 + V1^2
= c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
U22#(tt(),V1) = V1^2
>= V1^2
= c_9(isNat#(activate(V1)))
U31#(tt(),V2) = V2
>= V2
= c_11(isNatKind#(activate(V2)))
U51#(tt(),N) = 1 + N
>= N
= c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) = 3 + M + M*N + N^2
>= 2 + M + M*N + N^2
= c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
U62#(tt(),M,N) = 1 + N + N^2
>= N + N^2
= c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
U63#(tt(),M,N) = N
>= N
= c_18(isNatKind#(activate(N)))
isNatKind#(n__s(V1)) = 1 + V1
>= 1 + V1
= c_29(isNatKind#(activate(V1)))
0() = 1
>= 1
= n__0()
U31(tt(),V2) = 1
>= 1
= U32(isNatKind(activate(V2)))
U32(tt()) = 1
>= 1
= tt()
U41(tt()) = 1
>= 1
= tt()
activate(X) = X
>= X
= X
activate(n__0()) = 1
>= 1
= 0()
activate(n__plus(X1,X2)) = 1 + X1 + X2
>= 1 + X1 + X2
= plus(X1,X2)
activate(n__s(X)) = 1 + X
>= 1 + X
= s(X)
isNatKind(n__0()) = 1
>= 1
= tt()
isNatKind(n__plus(V1,V2)) = 1 + V1 + V2
>= V1
= U31(isNatKind(activate(V1))
,activate(V2))
isNatKind(n__s(V1)) = 1 + V1
>= 1
= U41(isNatKind(activate(V1)))
plus(X1,X2) = 1 + X1 + X2
>= 1 + X1 + X2
= n__plus(X1,X2)
s(X) = 1 + X
>= 1 + X
= n__s(X)
*** 1.1.1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
Strict TRS Rules:
Weak DP Rules:
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
Assumption
Proof:
()
*** 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(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2))):2
2:W:U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2))):3
3:W:U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1))):4
4:W:U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
-->_1 U15#(tt(),V2) -> c_6(isNat#(activate(V2))):5
5:W:U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
-->_1 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_1 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
6:W:U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U22#(tt(),V1) -> c_9(isNat#(activate(V1))):7
7:W:U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
-->_1 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_1 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
8:W:U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
9:W:U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
10:W:U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N))):11
11:W:U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
-->_1 U63#(tt(),M,N) -> c_18(isNatKind#(activate(N))):12
12:W:U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
13:W:isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):1
14:W:isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):6
15:W:isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U31#(tt(),V2) -> c_11(isNatKind#(activate(V2))):8
16:W:isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
10: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
11: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
12: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
9: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
1: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
13: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
7: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
6: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
14: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
5: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
4: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
3: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
2: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
15: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
8: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
*** 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:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,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.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1,4}
by application of
Pre({1,4}) = {3}.
Here rules are labelled as follows:
1: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
2: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
3: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
4: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
5: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
6: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
7: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
8: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
9: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
10: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
11: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
12: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
13: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
14: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
15: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
*** 1.1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{2}
by application of
Pre({2}) = {1}.
Here rules are labelled as follows:
1: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
2: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
3: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
4: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
5: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
6: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
7: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
8: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
9: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
10: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
11: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
12: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
13: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
14: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
15: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
*** 1.1.1.1.1.1.1.1.1.2.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
Strict TRS Rules:
Weak DP Rules:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1}
by application of
Pre({1}) = {}.
Here rules are labelled as follows:
1: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
2: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
3: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
4: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
5: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
6: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
7: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
8: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
9: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
10: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
11: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
12: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
13: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
14: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
15: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
*** 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:
U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2))):2
2:W:U12#(tt(),V1,V2) -> c_3(U13#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2))):3
3:W:U13#(tt(),V1,V2) -> c_4(U14#(isNatKind(activate(V2)),activate(V1),activate(V2)),isNatKind#(activate(V2)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1))):4
4:W:U14#(tt(),V1,V2) -> c_5(U15#(isNat(activate(V1)),activate(V2)),isNat#(activate(V1)))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
-->_1 U15#(tt(),V2) -> c_6(isNat#(activate(V2))):5
5:W:U15#(tt(),V2) -> c_6(isNat#(activate(V2)))
-->_1 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_1 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
6:W:U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U22#(tt(),V1) -> c_9(isNat#(activate(V1))):7
7:W:U22#(tt(),V1) -> c_9(isNat#(activate(V1)))
-->_1 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_1 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
8:W:U31#(tt(),V2) -> c_11(isNatKind#(activate(V2)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
9:W:U51#(tt(),N) -> c_14(isNatKind#(activate(N)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
10:W:U61#(tt(),M,N) -> c_16(U62#(isNatKind(activate(M)),activate(M),activate(N)),isNatKind#(activate(M)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N))):11
11:W:U62#(tt(),M,N) -> c_17(U63#(isNat(activate(N)),activate(M),activate(N)),isNat#(activate(N)))
-->_2 isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):14
-->_2 isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):13
-->_1 U63#(tt(),M,N) -> c_18(isNatKind#(activate(N))):12
12:W:U63#(tt(),M,N) -> c_18(isNatKind#(activate(N)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
13:W:isNat#(n__plus(V1,V2)) -> c_25(U11#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U11#(tt(),V1,V2) -> c_2(U12#(isNatKind(activate(V1)),activate(V1),activate(V2)),isNatKind#(activate(V1))):1
14:W:isNat#(n__s(V1)) -> c_26(U21#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U21#(tt(),V1) -> c_8(U22#(isNatKind(activate(V1)),activate(V1)),isNatKind#(activate(V1))):6
15:W:isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1)))
-->_2 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_2 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
-->_1 U31#(tt(),V2) -> c_11(isNatKind#(activate(V2))):8
16:W:isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1)))
-->_1 isNatKind#(n__s(V1)) -> c_29(isNatKind#(activate(V1))):16
-->_1 isNatKind#(n__plus(V1,V2)) -> c_28(U31#(isNatKind(activate(V1)),activate(V2)),isNatKind#(activate(V1))):15
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
10: U61#(tt(),M,N) ->
c_16(U62#(isNatKind(activate(M))
,activate(M)
,activate(N))
,isNatKind#(activate(M)))
11: U62#(tt(),M,N) ->
c_17(U63#(isNat(activate(N))
,activate(M)
,activate(N))
,isNat#(activate(N)))
12: U63#(tt(),M,N) ->
c_18(isNatKind#(activate(N)))
9: U51#(tt(),N) ->
c_14(isNatKind#(activate(N)))
1: U11#(tt(),V1,V2) ->
c_2(U12#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
13: isNat#(n__plus(V1,V2)) ->
c_25(U11#(isNatKind(activate(V1))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V1)))
7: U22#(tt(),V1) ->
c_9(isNat#(activate(V1)))
6: U21#(tt(),V1) ->
c_8(U22#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
14: isNat#(n__s(V1)) ->
c_26(U21#(isNatKind(activate(V1))
,activate(V1))
,isNatKind#(activate(V1)))
5: U15#(tt(),V2) ->
c_6(isNat#(activate(V2)))
4: U14#(tt(),V1,V2) ->
c_5(U15#(isNat(activate(V1))
,activate(V2))
,isNat#(activate(V1)))
3: U13#(tt(),V1,V2) ->
c_4(U14#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
2: U12#(tt(),V1,V2) ->
c_3(U13#(isNatKind(activate(V2))
,activate(V1)
,activate(V2))
,isNatKind#(activate(V2)))
16: isNatKind#(n__s(V1)) ->
c_29(isNatKind#(activate(V1)))
15: isNatKind#(n__plus(V1,V2)) ->
c_28(U31#(isNatKind(activate(V1))
,activate(V2))
,isNatKind#(activate(V1)))
8: U31#(tt(),V2) ->
c_11(isNatKind#(activate(V2)))
*** 1.1.1.1.1.1.1.1.1.2.1.1.1.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
0() -> n__0()
U11(tt(),V1,V2) -> U12(isNatKind(activate(V1)),activate(V1),activate(V2))
U12(tt(),V1,V2) -> U13(isNatKind(activate(V2)),activate(V1),activate(V2))
U13(tt(),V1,V2) -> U14(isNatKind(activate(V2)),activate(V1),activate(V2))
U14(tt(),V1,V2) -> U15(isNat(activate(V1)),activate(V2))
U15(tt(),V2) -> U16(isNat(activate(V2)))
U16(tt()) -> tt()
U21(tt(),V1) -> U22(isNatKind(activate(V1)),activate(V1))
U22(tt(),V1) -> U23(isNat(activate(V1)))
U23(tt()) -> tt()
U31(tt(),V2) -> U32(isNatKind(activate(V2)))
U32(tt()) -> tt()
U41(tt()) -> tt()
activate(X) -> X
activate(n__0()) -> 0()
activate(n__plus(X1,X2)) -> plus(X1,X2)
activate(n__s(X)) -> s(X)
isNat(n__0()) -> tt()
isNat(n__plus(V1,V2)) -> U11(isNatKind(activate(V1)),activate(V1),activate(V2))
isNat(n__s(V1)) -> U21(isNatKind(activate(V1)),activate(V1))
isNatKind(n__0()) -> tt()
isNatKind(n__plus(V1,V2)) -> U31(isNatKind(activate(V1)),activate(V2))
isNatKind(n__s(V1)) -> U41(isNatKind(activate(V1)))
plus(X1,X2) -> n__plus(X1,X2)
s(X) -> n__s(X)
Signature:
{0/0,U11/3,U12/3,U13/3,U14/3,U15/2,U16/1,U21/2,U22/2,U23/1,U31/2,U32/1,U41/1,U51/2,U52/2,U61/3,U62/3,U63/3,U64/3,activate/1,isNat/1,isNatKind/1,plus/2,s/1,0#/0,U11#/3,U12#/3,U13#/3,U14#/3,U15#/2,U16#/1,U21#/2,U22#/2,U23#/1,U31#/2,U32#/1,U41#/1,U51#/2,U52#/2,U61#/3,U62#/3,U63#/3,U64#/3,activate#/1,isNat#/1,isNatKind#/1,plus#/2,s#/1} / {n__0/0,n__plus/2,n__s/1,tt/0,c_1/0,c_2/2,c_3/2,c_4/2,c_5/2,c_6/1,c_7/0,c_8/2,c_9/1,c_10/0,c_11/1,c_12/0,c_13/0,c_14/1,c_15/1,c_16/2,c_17/2,c_18/1,c_19/4,c_20/0,c_21/1,c_22/1,c_23/1,c_24/0,c_25/2,c_26/2,c_27/0,c_28/2,c_29/1,c_30/0,c_31/0}
Obligation:
Innermost
basic terms: {0#,U11#,U12#,U13#,U14#,U15#,U16#,U21#,U22#,U23#,U31#,U32#,U41#,U51#,U52#,U61#,U62#,U63#,U64#,activate#,isNat#,isNatKind#,plus#,s#}/{n__0,n__plus,n__s,tt}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).