WORST_CASE(?,O(n^1)) * Step 1: InnermostRuleRemoval WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) plus(N,0()) -> U11(isNat(N),N) plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,activate,and,isNat,plus ,s} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. plus(N,0()) -> U11(isNat(N),N) plus(N,s(M)) -> U21(and(isNat(M),n__isNat(N)),M,N) All above mentioned rules can be savely removed. * Step 2: Bounds WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,activate,and,isNat,plus ,s} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: Bounds {initialAutomaton = perSymbol, enrichment = match} + Details: The problem is match-bounded by 5. The enriched problem is compatible with follwoing automaton. 0_0() -> 1 0_1() -> 2 0_1() -> 4 0_1() -> 5 0_1() -> 19 0_1() -> 20 0_1() -> 23 0_1() -> 24 U11_0(7,7) -> 2 U11_0(7,8) -> 2 U11_0(7,9) -> 2 U11_0(7,10) -> 2 U11_0(7,13) -> 2 U11_0(8,7) -> 2 U11_0(8,8) -> 2 U11_0(8,9) -> 2 U11_0(8,10) -> 2 U11_0(8,13) -> 2 U11_0(9,7) -> 2 U11_0(9,8) -> 2 U11_0(9,9) -> 2 U11_0(9,10) -> 2 U11_0(9,13) -> 2 U11_0(10,7) -> 2 U11_0(10,8) -> 2 U11_0(10,9) -> 2 U11_0(10,10) -> 2 U11_0(10,13) -> 2 U11_0(13,7) -> 2 U11_0(13,8) -> 2 U11_0(13,9) -> 2 U11_0(13,10) -> 2 U11_0(13,13) -> 2 U21_0(7,7,7) -> 3 U21_0(7,7,8) -> 3 U21_0(7,7,9) -> 3 U21_0(7,7,10) -> 3 U21_0(7,7,13) -> 3 U21_0(7,8,7) -> 3 U21_0(7,8,8) -> 3 U21_0(7,8,9) -> 3 U21_0(7,8,10) -> 3 U21_0(7,8,13) -> 3 U21_0(7,9,7) -> 3 U21_0(7,9,8) -> 3 U21_0(7,9,9) -> 3 U21_0(7,9,10) -> 3 U21_0(7,9,13) -> 3 U21_0(7,10,7) -> 3 U21_0(7,10,8) -> 3 U21_0(7,10,9) -> 3 U21_0(7,10,10) -> 3 U21_0(7,10,13) -> 3 U21_0(7,13,7) -> 3 U21_0(7,13,8) -> 3 U21_0(7,13,9) -> 3 U21_0(7,13,10) -> 3 U21_0(7,13,13) -> 3 U21_0(8,7,7) -> 3 U21_0(8,7,8) -> 3 U21_0(8,7,9) -> 3 U21_0(8,7,10) -> 3 U21_0(8,7,13) -> 3 U21_0(8,8,7) -> 3 U21_0(8,8,8) -> 3 U21_0(8,8,9) -> 3 U21_0(8,8,10) -> 3 U21_0(8,8,13) -> 3 U21_0(8,9,7) -> 3 U21_0(8,9,8) -> 3 U21_0(8,9,9) -> 3 U21_0(8,9,10) -> 3 U21_0(8,9,13) -> 3 U21_0(8,10,7) -> 3 U21_0(8,10,8) -> 3 U21_0(8,10,9) -> 3 U21_0(8,10,10) -> 3 U21_0(8,10,13) -> 3 U21_0(8,13,7) -> 3 U21_0(8,13,8) -> 3 U21_0(8,13,9) -> 3 U21_0(8,13,10) -> 3 U21_0(8,13,13) -> 3 U21_0(9,7,7) -> 3 U21_0(9,7,8) -> 3 U21_0(9,7,9) -> 3 U21_0(9,7,10) -> 3 U21_0(9,7,13) -> 3 U21_0(9,8,7) -> 3 U21_0(9,8,8) -> 3 U21_0(9,8,9) -> 3 U21_0(9,8,10) -> 3 U21_0(9,8,13) -> 3 U21_0(9,9,7) -> 3 U21_0(9,9,8) -> 3 U21_0(9,9,9) -> 3 U21_0(9,9,10) -> 3 U21_0(9,9,13) -> 3 U21_0(9,10,7) -> 3 U21_0(9,10,8) -> 3 U21_0(9,10,9) -> 3 U21_0(9,10,10) -> 3 U21_0(9,10,13) -> 3 U21_0(9,13,7) -> 3 U21_0(9,13,8) -> 3 U21_0(9,13,9) -> 3 U21_0(9,13,10) -> 3 U21_0(9,13,13) -> 3 U21_0(10,7,7) -> 3 U21_0(10,7,8) -> 3 U21_0(10,7,9) -> 3 U21_0(10,7,10) -> 3 U21_0(10,7,13) -> 3 U21_0(10,8,7) -> 3 U21_0(10,8,8) -> 3 U21_0(10,8,9) -> 3 U21_0(10,8,10) -> 3 U21_0(10,8,13) -> 3 U21_0(10,9,7) -> 3 U21_0(10,9,8) -> 3 U21_0(10,9,9) -> 3 U21_0(10,9,10) -> 3 U21_0(10,9,13) -> 3 U21_0(10,10,7) -> 3 U21_0(10,10,8) -> 3 U21_0(10,10,9) -> 3 U21_0(10,10,10) -> 3 U21_0(10,10,13) -> 3 U21_0(10,13,7) -> 3 U21_0(10,13,8) -> 3 U21_0(10,13,9) -> 3 U21_0(10,13,10) -> 3 U21_0(10,13,13) -> 3 U21_0(13,7,7) -> 3 U21_0(13,7,8) -> 3 U21_0(13,7,9) -> 3 U21_0(13,7,10) -> 3 U21_0(13,7,13) -> 3 U21_0(13,8,7) -> 3 U21_0(13,8,8) -> 3 U21_0(13,8,9) -> 3 U21_0(13,8,10) -> 3 U21_0(13,8,13) -> 3 U21_0(13,9,7) -> 3 U21_0(13,9,8) -> 3 U21_0(13,9,9) -> 3 U21_0(13,9,10) -> 3 U21_0(13,9,13) -> 3 U21_0(13,10,7) -> 3 U21_0(13,10,8) -> 3 U21_0(13,10,9) -> 3 U21_0(13,10,10) -> 3 U21_0(13,10,13) -> 3 U21_0(13,13,7) -> 3 U21_0(13,13,8) -> 3 U21_0(13,13,9) -> 3 U21_0(13,13,10) -> 3 U21_0(13,13,13) -> 3 activate_0(7) -> 4 activate_0(8) -> 4 activate_0(9) -> 4 activate_0(10) -> 4 activate_0(13) -> 4 activate_1(7) -> 2 activate_1(7) -> 5 activate_1(8) -> 2 activate_1(8) -> 5 activate_1(9) -> 2 activate_1(9) -> 5 activate_1(10) -> 2 activate_1(10) -> 5 activate_1(13) -> 2 activate_1(13) -> 5 activate_1(16) -> 21 activate_1(16) -> 24 activate_1(18) -> 21 activate_1(18) -> 24 activate_2(7) -> 19 activate_2(7) -> 20 activate_2(8) -> 20 activate_2(9) -> 20 activate_2(10) -> 20 activate_2(13) -> 20 activate_2(16) -> 2 activate_2(16) -> 4 activate_2(16) -> 5 activate_2(16) -> 6 activate_2(16) -> 15 activate_2(16) -> 17 activate_2(16) -> 20 activate_2(16) -> 21 activate_2(16) -> 24 activate_2(18) -> 2 activate_2(18) -> 4 activate_2(18) -> 5 activate_2(18) -> 6 activate_2(18) -> 15 activate_2(18) -> 17 activate_2(18) -> 20 activate_2(18) -> 21 activate_2(18) -> 24 activate_2(22) -> 2 activate_2(22) -> 4 activate_2(22) -> 5 activate_2(22) -> 6 activate_2(22) -> 15 activate_2(22) -> 17 activate_2(22) -> 20 activate_2(22) -> 21 activate_2(22) -> 24 activate_3(7) -> 23 activate_3(7) -> 24 activate_3(8) -> 24 activate_3(9) -> 24 activate_3(10) -> 24 activate_3(13) -> 24 activate_3(18) -> 2 activate_3(18) -> 4 activate_3(18) -> 5 activate_3(18) -> 6 activate_3(18) -> 15 activate_3(18) -> 17 activate_3(18) -> 20 activate_3(18) -> 21 activate_3(18) -> 24 activate_3(22) -> 2 activate_3(22) -> 4 activate_3(22) -> 5 activate_3(22) -> 6 activate_3(22) -> 15 activate_3(22) -> 17 activate_3(22) -> 20 activate_3(22) -> 21 activate_3(22) -> 24 activate_4(22) -> 2 activate_4(22) -> 4 activate_4(22) -> 5 activate_4(22) -> 6 activate_4(22) -> 15 activate_4(22) -> 17 activate_4(22) -> 20 activate_4(22) -> 21 activate_4(22) -> 24 and_0(7,7) -> 5 and_0(7,8) -> 5 and_0(7,9) -> 5 and_0(7,10) -> 5 and_0(7,13) -> 5 and_0(8,7) -> 5 and_0(8,8) -> 5 and_0(8,9) -> 5 and_0(8,10) -> 5 and_0(8,13) -> 5 and_0(9,7) -> 5 and_0(9,8) -> 5 and_0(9,9) -> 5 and_0(9,10) -> 5 and_0(9,13) -> 5 and_0(10,7) -> 5 and_0(10,8) -> 5 and_0(10,9) -> 5 and_0(10,10) -> 5 and_0(10,13) -> 5 and_0(13,7) -> 5 and_0(13,8) -> 5 and_0(13,9) -> 5 and_0(13,10) -> 5 and_0(13,13) -> 5 and_1(15,16) -> 2 and_1(15,16) -> 4 and_1(15,16) -> 5 and_1(15,16) -> 6 and_1(15,16) -> 15 and_1(15,16) -> 17 and_1(15,16) -> 20 and_1(20,16) -> 21 and_1(20,16) -> 24 and_2(17,18) -> 2 and_2(17,18) -> 4 and_2(17,18) -> 5 and_2(17,18) -> 6 and_2(17,18) -> 15 and_2(17,18) -> 17 and_2(17,18) -> 20 and_2(20,18) -> 21 and_2(20,18) -> 24 and_3(21,22) -> 2 and_3(21,22) -> 4 and_3(21,22) -> 5 and_3(21,22) -> 6 and_3(21,22) -> 15 and_3(21,22) -> 17 and_3(21,22) -> 20 and_3(21,22) -> 21 and_3(21,22) -> 24 isNat_0(7) -> 6 isNat_0(8) -> 6 isNat_0(9) -> 6 isNat_0(10) -> 6 isNat_0(13) -> 6 isNat_1(5) -> 2 isNat_1(5) -> 4 isNat_1(5) -> 5 isNat_1(5) -> 6 isNat_1(5) -> 15 isNat_1(5) -> 17 isNat_1(5) -> 20 isNat_1(5) -> 21 isNat_1(5) -> 24 isNat_1(7) -> 2 isNat_1(7) -> 4 isNat_1(7) -> 5 isNat_1(7) -> 20 isNat_1(7) -> 24 isNat_1(8) -> 2 isNat_1(8) -> 4 isNat_1(8) -> 5 isNat_1(8) -> 20 isNat_1(8) -> 24 isNat_1(9) -> 2 isNat_1(9) -> 4 isNat_1(9) -> 5 isNat_1(9) -> 20 isNat_1(9) -> 24 isNat_1(10) -> 2 isNat_1(10) -> 4 isNat_1(10) -> 5 isNat_1(10) -> 20 isNat_1(10) -> 24 isNat_1(13) -> 2 isNat_1(13) -> 4 isNat_1(13) -> 5 isNat_1(13) -> 20 isNat_1(13) -> 24 isNat_2(5) -> 2 isNat_2(5) -> 4 isNat_2(5) -> 5 isNat_2(5) -> 6 isNat_2(5) -> 15 isNat_2(5) -> 17 isNat_2(5) -> 20 isNat_2(5) -> 21 isNat_2(5) -> 24 isNat_2(19) -> 17 isNat_2(20) -> 2 isNat_2(20) -> 4 isNat_2(20) -> 5 isNat_2(20) -> 6 isNat_2(20) -> 15 isNat_2(20) -> 17 isNat_2(20) -> 20 isNat_2(20) -> 21 isNat_2(20) -> 24 isNat_3(20) -> 2 isNat_3(20) -> 4 isNat_3(20) -> 5 isNat_3(20) -> 6 isNat_3(20) -> 15 isNat_3(20) -> 17 isNat_3(20) -> 20 isNat_3(20) -> 21 isNat_3(20) -> 24 isNat_3(23) -> 21 isNat_3(24) -> 2 isNat_3(24) -> 4 isNat_3(24) -> 5 isNat_3(24) -> 6 isNat_3(24) -> 15 isNat_3(24) -> 17 isNat_3(24) -> 20 isNat_3(24) -> 21 isNat_3(24) -> 24 isNat_4(24) -> 2 isNat_4(24) -> 4 isNat_4(24) -> 5 isNat_4(24) -> 6 isNat_4(24) -> 15 isNat_4(24) -> 17 isNat_4(24) -> 20 isNat_4(24) -> 21 isNat_4(24) -> 24 n__0_0() -> 2 n__0_0() -> 4 n__0_0() -> 5 n__0_0() -> 7 n__0_0() -> 19 n__0_0() -> 20 n__0_0() -> 23 n__0_0() -> 24 n__0_1() -> 1 n__0_2() -> 2 n__0_2() -> 4 n__0_2() -> 5 n__0_2() -> 19 n__0_2() -> 20 n__0_2() -> 23 n__0_2() -> 24 n__isNat_0(7) -> 2 n__isNat_0(7) -> 4 n__isNat_0(7) -> 5 n__isNat_0(7) -> 8 n__isNat_0(7) -> 20 n__isNat_0(7) -> 24 n__isNat_0(8) -> 2 n__isNat_0(8) -> 4 n__isNat_0(8) -> 5 n__isNat_0(8) -> 8 n__isNat_0(8) -> 20 n__isNat_0(8) -> 24 n__isNat_0(9) -> 2 n__isNat_0(9) -> 4 n__isNat_0(9) -> 5 n__isNat_0(9) -> 8 n__isNat_0(9) -> 20 n__isNat_0(9) -> 24 n__isNat_0(10) -> 2 n__isNat_0(10) -> 4 n__isNat_0(10) -> 5 n__isNat_0(10) -> 8 n__isNat_0(10) -> 20 n__isNat_0(10) -> 24 n__isNat_0(13) -> 2 n__isNat_0(13) -> 4 n__isNat_0(13) -> 5 n__isNat_0(13) -> 8 n__isNat_0(13) -> 20 n__isNat_0(13) -> 24 n__isNat_1(5) -> 2 n__isNat_1(5) -> 4 n__isNat_1(5) -> 5 n__isNat_1(5) -> 6 n__isNat_1(5) -> 15 n__isNat_1(5) -> 16 n__isNat_1(5) -> 17 n__isNat_1(5) -> 20 n__isNat_1(5) -> 21 n__isNat_1(5) -> 24 n__isNat_1(7) -> 6 n__isNat_1(8) -> 6 n__isNat_1(9) -> 6 n__isNat_1(10) -> 6 n__isNat_1(13) -> 6 n__isNat_2(5) -> 2 n__isNat_2(5) -> 4 n__isNat_2(5) -> 5 n__isNat_2(5) -> 6 n__isNat_2(5) -> 15 n__isNat_2(5) -> 17 n__isNat_2(5) -> 20 n__isNat_2(5) -> 21 n__isNat_2(5) -> 24 n__isNat_2(7) -> 2 n__isNat_2(7) -> 4 n__isNat_2(7) -> 5 n__isNat_2(7) -> 20 n__isNat_2(7) -> 24 n__isNat_2(8) -> 2 n__isNat_2(8) -> 4 n__isNat_2(8) -> 5 n__isNat_2(8) -> 20 n__isNat_2(8) -> 24 n__isNat_2(9) -> 2 n__isNat_2(9) -> 4 n__isNat_2(9) -> 5 n__isNat_2(9) -> 20 n__isNat_2(9) -> 24 n__isNat_2(10) -> 2 n__isNat_2(10) -> 4 n__isNat_2(10) -> 5 n__isNat_2(10) -> 20 n__isNat_2(10) -> 24 n__isNat_2(13) -> 2 n__isNat_2(13) -> 4 n__isNat_2(13) -> 5 n__isNat_2(13) -> 20 n__isNat_2(13) -> 24 n__isNat_2(20) -> 2 n__isNat_2(20) -> 4 n__isNat_2(20) -> 5 n__isNat_2(20) -> 6 n__isNat_2(20) -> 15 n__isNat_2(20) -> 17 n__isNat_2(20) -> 18 n__isNat_2(20) -> 20 n__isNat_2(20) -> 21 n__isNat_2(20) -> 24 n__isNat_3(5) -> 2 n__isNat_3(5) -> 4 n__isNat_3(5) -> 5 n__isNat_3(5) -> 6 n__isNat_3(5) -> 15 n__isNat_3(5) -> 17 n__isNat_3(5) -> 20 n__isNat_3(5) -> 21 n__isNat_3(5) -> 24 n__isNat_3(19) -> 17 n__isNat_3(20) -> 2 n__isNat_3(20) -> 4 n__isNat_3(20) -> 5 n__isNat_3(20) -> 6 n__isNat_3(20) -> 15 n__isNat_3(20) -> 17 n__isNat_3(20) -> 20 n__isNat_3(20) -> 21 n__isNat_3(20) -> 24 n__isNat_3(24) -> 2 n__isNat_3(24) -> 4 n__isNat_3(24) -> 5 n__isNat_3(24) -> 6 n__isNat_3(24) -> 15 n__isNat_3(24) -> 17 n__isNat_3(24) -> 20 n__isNat_3(24) -> 21 n__isNat_3(24) -> 22 n__isNat_3(24) -> 24 n__isNat_4(20) -> 2 n__isNat_4(20) -> 4 n__isNat_4(20) -> 5 n__isNat_4(20) -> 6 n__isNat_4(20) -> 15 n__isNat_4(20) -> 17 n__isNat_4(20) -> 20 n__isNat_4(20) -> 21 n__isNat_4(20) -> 24 n__isNat_4(23) -> 21 n__isNat_4(24) -> 2 n__isNat_4(24) -> 4 n__isNat_4(24) -> 5 n__isNat_4(24) -> 6 n__isNat_4(24) -> 15 n__isNat_4(24) -> 17 n__isNat_4(24) -> 20 n__isNat_4(24) -> 21 n__isNat_4(24) -> 24 n__isNat_5(24) -> 2 n__isNat_5(24) -> 4 n__isNat_5(24) -> 5 n__isNat_5(24) -> 6 n__isNat_5(24) -> 15 n__isNat_5(24) -> 17 n__isNat_5(24) -> 20 n__isNat_5(24) -> 21 n__isNat_5(24) -> 24 n__plus_0(7,7) -> 2 n__plus_0(7,7) -> 4 n__plus_0(7,7) -> 5 n__plus_0(7,7) -> 9 n__plus_0(7,7) -> 20 n__plus_0(7,7) -> 24 n__plus_0(7,8) -> 2 n__plus_0(7,8) -> 4 n__plus_0(7,8) -> 5 n__plus_0(7,8) -> 9 n__plus_0(7,8) -> 20 n__plus_0(7,8) -> 24 n__plus_0(7,9) -> 2 n__plus_0(7,9) -> 4 n__plus_0(7,9) -> 5 n__plus_0(7,9) -> 9 n__plus_0(7,9) -> 20 n__plus_0(7,9) -> 24 n__plus_0(7,10) -> 2 n__plus_0(7,10) -> 4 n__plus_0(7,10) -> 5 n__plus_0(7,10) -> 9 n__plus_0(7,10) -> 20 n__plus_0(7,10) -> 24 n__plus_0(7,13) -> 2 n__plus_0(7,13) -> 4 n__plus_0(7,13) -> 5 n__plus_0(7,13) -> 9 n__plus_0(7,13) -> 20 n__plus_0(7,13) -> 24 n__plus_0(8,7) -> 2 n__plus_0(8,7) -> 4 n__plus_0(8,7) -> 5 n__plus_0(8,7) -> 9 n__plus_0(8,7) -> 20 n__plus_0(8,7) -> 24 n__plus_0(8,8) -> 2 n__plus_0(8,8) -> 4 n__plus_0(8,8) -> 5 n__plus_0(8,8) -> 9 n__plus_0(8,8) -> 20 n__plus_0(8,8) -> 24 n__plus_0(8,9) -> 2 n__plus_0(8,9) -> 4 n__plus_0(8,9) -> 5 n__plus_0(8,9) -> 9 n__plus_0(8,9) -> 20 n__plus_0(8,9) -> 24 n__plus_0(8,10) -> 2 n__plus_0(8,10) -> 4 n__plus_0(8,10) -> 5 n__plus_0(8,10) -> 9 n__plus_0(8,10) -> 20 n__plus_0(8,10) -> 24 n__plus_0(8,13) -> 2 n__plus_0(8,13) -> 4 n__plus_0(8,13) -> 5 n__plus_0(8,13) -> 9 n__plus_0(8,13) -> 20 n__plus_0(8,13) -> 24 n__plus_0(9,7) -> 2 n__plus_0(9,7) -> 4 n__plus_0(9,7) -> 5 n__plus_0(9,7) -> 9 n__plus_0(9,7) -> 20 n__plus_0(9,7) -> 24 n__plus_0(9,8) -> 2 n__plus_0(9,8) -> 4 n__plus_0(9,8) -> 5 n__plus_0(9,8) -> 9 n__plus_0(9,8) -> 20 n__plus_0(9,8) -> 24 n__plus_0(9,9) -> 2 n__plus_0(9,9) -> 4 n__plus_0(9,9) -> 5 n__plus_0(9,9) -> 9 n__plus_0(9,9) -> 20 n__plus_0(9,9) -> 24 n__plus_0(9,10) -> 2 n__plus_0(9,10) -> 4 n__plus_0(9,10) -> 5 n__plus_0(9,10) -> 9 n__plus_0(9,10) -> 20 n__plus_0(9,10) -> 24 n__plus_0(9,13) -> 2 n__plus_0(9,13) -> 4 n__plus_0(9,13) -> 5 n__plus_0(9,13) -> 9 n__plus_0(9,13) -> 20 n__plus_0(9,13) -> 24 n__plus_0(10,7) -> 2 n__plus_0(10,7) -> 4 n__plus_0(10,7) -> 5 n__plus_0(10,7) -> 9 n__plus_0(10,7) -> 20 n__plus_0(10,7) -> 24 n__plus_0(10,8) -> 2 n__plus_0(10,8) -> 4 n__plus_0(10,8) -> 5 n__plus_0(10,8) -> 9 n__plus_0(10,8) -> 20 n__plus_0(10,8) -> 24 n__plus_0(10,9) -> 2 n__plus_0(10,9) -> 4 n__plus_0(10,9) -> 5 n__plus_0(10,9) -> 9 n__plus_0(10,9) -> 20 n__plus_0(10,9) -> 24 n__plus_0(10,10) -> 2 n__plus_0(10,10) -> 4 n__plus_0(10,10) -> 5 n__plus_0(10,10) -> 9 n__plus_0(10,10) -> 20 n__plus_0(10,10) -> 24 n__plus_0(10,13) -> 2 n__plus_0(10,13) -> 4 n__plus_0(10,13) -> 5 n__plus_0(10,13) -> 9 n__plus_0(10,13) -> 20 n__plus_0(10,13) -> 24 n__plus_0(13,7) -> 2 n__plus_0(13,7) -> 4 n__plus_0(13,7) -> 5 n__plus_0(13,7) -> 9 n__plus_0(13,7) -> 20 n__plus_0(13,7) -> 24 n__plus_0(13,8) -> 2 n__plus_0(13,8) -> 4 n__plus_0(13,8) -> 5 n__plus_0(13,8) -> 9 n__plus_0(13,8) -> 20 n__plus_0(13,8) -> 24 n__plus_0(13,9) -> 2 n__plus_0(13,9) -> 4 n__plus_0(13,9) -> 5 n__plus_0(13,9) -> 9 n__plus_0(13,9) -> 20 n__plus_0(13,9) -> 24 n__plus_0(13,10) -> 2 n__plus_0(13,10) -> 4 n__plus_0(13,10) -> 5 n__plus_0(13,10) -> 9 n__plus_0(13,10) -> 20 n__plus_0(13,10) -> 24 n__plus_0(13,13) -> 2 n__plus_0(13,13) -> 4 n__plus_0(13,13) -> 5 n__plus_0(13,13) -> 9 n__plus_0(13,13) -> 20 n__plus_0(13,13) -> 24 n__plus_1(7,7) -> 11 n__plus_1(7,8) -> 11 n__plus_1(7,9) -> 11 n__plus_1(7,10) -> 11 n__plus_1(7,13) -> 11 n__plus_1(8,7) -> 11 n__plus_1(8,8) -> 11 n__plus_1(8,9) -> 11 n__plus_1(8,10) -> 11 n__plus_1(8,13) -> 11 n__plus_1(9,7) -> 11 n__plus_1(9,8) -> 11 n__plus_1(9,9) -> 11 n__plus_1(9,10) -> 11 n__plus_1(9,13) -> 11 n__plus_1(10,7) -> 11 n__plus_1(10,8) -> 11 n__plus_1(10,9) -> 11 n__plus_1(10,10) -> 11 n__plus_1(10,13) -> 11 n__plus_1(13,7) -> 11 n__plus_1(13,8) -> 11 n__plus_1(13,9) -> 11 n__plus_1(13,10) -> 11 n__plus_1(13,13) -> 11 n__plus_2(2,2) -> 14 n__plus_2(7,7) -> 2 n__plus_2(7,7) -> 4 n__plus_2(7,7) -> 5 n__plus_2(7,7) -> 20 n__plus_2(7,7) -> 24 n__plus_2(7,8) -> 2 n__plus_2(7,8) -> 4 n__plus_2(7,8) -> 5 n__plus_2(7,8) -> 20 n__plus_2(7,8) -> 24 n__plus_2(7,9) -> 2 n__plus_2(7,9) -> 4 n__plus_2(7,9) -> 5 n__plus_2(7,9) -> 20 n__plus_2(7,9) -> 24 n__plus_2(7,10) -> 2 n__plus_2(7,10) -> 4 n__plus_2(7,10) -> 5 n__plus_2(7,10) -> 20 n__plus_2(7,10) -> 24 n__plus_2(7,13) -> 2 n__plus_2(7,13) -> 4 n__plus_2(7,13) -> 5 n__plus_2(7,13) -> 20 n__plus_2(7,13) -> 24 n__plus_2(8,7) -> 2 n__plus_2(8,7) -> 4 n__plus_2(8,7) -> 5 n__plus_2(8,7) -> 20 n__plus_2(8,7) -> 24 n__plus_2(8,8) -> 2 n__plus_2(8,8) -> 4 n__plus_2(8,8) -> 5 n__plus_2(8,8) -> 20 n__plus_2(8,8) -> 24 n__plus_2(8,9) -> 2 n__plus_2(8,9) -> 4 n__plus_2(8,9) -> 5 n__plus_2(8,9) -> 20 n__plus_2(8,9) -> 24 n__plus_2(8,10) -> 2 n__plus_2(8,10) -> 4 n__plus_2(8,10) -> 5 n__plus_2(8,10) -> 20 n__plus_2(8,10) -> 24 n__plus_2(8,13) -> 2 n__plus_2(8,13) -> 4 n__plus_2(8,13) -> 5 n__plus_2(8,13) -> 20 n__plus_2(8,13) -> 24 n__plus_2(9,7) -> 2 n__plus_2(9,7) -> 4 n__plus_2(9,7) -> 5 n__plus_2(9,7) -> 20 n__plus_2(9,7) -> 24 n__plus_2(9,8) -> 2 n__plus_2(9,8) -> 4 n__plus_2(9,8) -> 5 n__plus_2(9,8) -> 20 n__plus_2(9,8) -> 24 n__plus_2(9,9) -> 2 n__plus_2(9,9) -> 4 n__plus_2(9,9) -> 5 n__plus_2(9,9) -> 20 n__plus_2(9,9) -> 24 n__plus_2(9,10) -> 2 n__plus_2(9,10) -> 4 n__plus_2(9,10) -> 5 n__plus_2(9,10) -> 20 n__plus_2(9,10) -> 24 n__plus_2(9,13) -> 2 n__plus_2(9,13) -> 4 n__plus_2(9,13) -> 5 n__plus_2(9,13) -> 20 n__plus_2(9,13) -> 24 n__plus_2(10,7) -> 2 n__plus_2(10,7) -> 4 n__plus_2(10,7) -> 5 n__plus_2(10,7) -> 20 n__plus_2(10,7) -> 24 n__plus_2(10,8) -> 2 n__plus_2(10,8) -> 4 n__plus_2(10,8) -> 5 n__plus_2(10,8) -> 20 n__plus_2(10,8) -> 24 n__plus_2(10,9) -> 2 n__plus_2(10,9) -> 4 n__plus_2(10,9) -> 5 n__plus_2(10,9) -> 20 n__plus_2(10,9) -> 24 n__plus_2(10,10) -> 2 n__plus_2(10,10) -> 4 n__plus_2(10,10) -> 5 n__plus_2(10,10) -> 20 n__plus_2(10,10) -> 24 n__plus_2(10,13) -> 2 n__plus_2(10,13) -> 4 n__plus_2(10,13) -> 5 n__plus_2(10,13) -> 20 n__plus_2(10,13) -> 24 n__plus_2(13,7) -> 2 n__plus_2(13,7) -> 4 n__plus_2(13,7) -> 5 n__plus_2(13,7) -> 20 n__plus_2(13,7) -> 24 n__plus_2(13,8) -> 2 n__plus_2(13,8) -> 4 n__plus_2(13,8) -> 5 n__plus_2(13,8) -> 20 n__plus_2(13,8) -> 24 n__plus_2(13,9) -> 2 n__plus_2(13,9) -> 4 n__plus_2(13,9) -> 5 n__plus_2(13,9) -> 20 n__plus_2(13,9) -> 24 n__plus_2(13,10) -> 2 n__plus_2(13,10) -> 4 n__plus_2(13,10) -> 5 n__plus_2(13,10) -> 20 n__plus_2(13,10) -> 24 n__plus_2(13,13) -> 2 n__plus_2(13,13) -> 4 n__plus_2(13,13) -> 5 n__plus_2(13,13) -> 20 n__plus_2(13,13) -> 24 n__s_0(7) -> 2 n__s_0(7) -> 4 n__s_0(7) -> 5 n__s_0(7) -> 10 n__s_0(7) -> 20 n__s_0(7) -> 24 n__s_0(8) -> 2 n__s_0(8) -> 4 n__s_0(8) -> 5 n__s_0(8) -> 10 n__s_0(8) -> 20 n__s_0(8) -> 24 n__s_0(9) -> 2 n__s_0(9) -> 4 n__s_0(9) -> 5 n__s_0(9) -> 10 n__s_0(9) -> 20 n__s_0(9) -> 24 n__s_0(10) -> 2 n__s_0(10) -> 4 n__s_0(10) -> 5 n__s_0(10) -> 10 n__s_0(10) -> 20 n__s_0(10) -> 24 n__s_0(13) -> 2 n__s_0(13) -> 4 n__s_0(13) -> 5 n__s_0(13) -> 10 n__s_0(13) -> 20 n__s_0(13) -> 24 n__s_1(7) -> 12 n__s_1(8) -> 12 n__s_1(9) -> 12 n__s_1(10) -> 12 n__s_1(13) -> 12 n__s_2(7) -> 2 n__s_2(7) -> 4 n__s_2(7) -> 5 n__s_2(7) -> 20 n__s_2(7) -> 24 n__s_2(8) -> 2 n__s_2(8) -> 4 n__s_2(8) -> 5 n__s_2(8) -> 20 n__s_2(8) -> 24 n__s_2(9) -> 2 n__s_2(9) -> 4 n__s_2(9) -> 5 n__s_2(9) -> 20 n__s_2(9) -> 24 n__s_2(10) -> 2 n__s_2(10) -> 4 n__s_2(10) -> 5 n__s_2(10) -> 20 n__s_2(10) -> 24 n__s_2(13) -> 2 n__s_2(13) -> 4 n__s_2(13) -> 5 n__s_2(13) -> 20 n__s_2(13) -> 24 n__s_2(14) -> 3 plus_0(7,7) -> 11 plus_0(7,8) -> 11 plus_0(7,9) -> 11 plus_0(7,10) -> 11 plus_0(7,13) -> 11 plus_0(8,7) -> 11 plus_0(8,8) -> 11 plus_0(8,9) -> 11 plus_0(8,10) -> 11 plus_0(8,13) -> 11 plus_0(9,7) -> 11 plus_0(9,8) -> 11 plus_0(9,9) -> 11 plus_0(9,10) -> 11 plus_0(9,13) -> 11 plus_0(10,7) -> 11 plus_0(10,8) -> 11 plus_0(10,9) -> 11 plus_0(10,10) -> 11 plus_0(10,13) -> 11 plus_0(13,7) -> 11 plus_0(13,8) -> 11 plus_0(13,9) -> 11 plus_0(13,10) -> 11 plus_0(13,13) -> 11 plus_1(2,2) -> 14 plus_1(7,7) -> 2 plus_1(7,7) -> 4 plus_1(7,7) -> 5 plus_1(7,7) -> 20 plus_1(7,7) -> 24 plus_1(7,8) -> 2 plus_1(7,8) -> 4 plus_1(7,8) -> 5 plus_1(7,8) -> 20 plus_1(7,8) -> 24 plus_1(7,9) -> 2 plus_1(7,9) -> 4 plus_1(7,9) -> 5 plus_1(7,9) -> 20 plus_1(7,9) -> 24 plus_1(7,10) -> 2 plus_1(7,10) -> 4 plus_1(7,10) -> 5 plus_1(7,10) -> 20 plus_1(7,10) -> 24 plus_1(7,13) -> 2 plus_1(7,13) -> 4 plus_1(7,13) -> 5 plus_1(7,13) -> 20 plus_1(7,13) -> 24 plus_1(8,7) -> 2 plus_1(8,7) -> 4 plus_1(8,7) -> 5 plus_1(8,7) -> 20 plus_1(8,7) -> 24 plus_1(8,8) -> 2 plus_1(8,8) -> 4 plus_1(8,8) -> 5 plus_1(8,8) -> 20 plus_1(8,8) -> 24 plus_1(8,9) -> 2 plus_1(8,9) -> 4 plus_1(8,9) -> 5 plus_1(8,9) -> 20 plus_1(8,9) -> 24 plus_1(8,10) -> 2 plus_1(8,10) -> 4 plus_1(8,10) -> 5 plus_1(8,10) -> 20 plus_1(8,10) -> 24 plus_1(8,13) -> 2 plus_1(8,13) -> 4 plus_1(8,13) -> 5 plus_1(8,13) -> 20 plus_1(8,13) -> 24 plus_1(9,7) -> 2 plus_1(9,7) -> 4 plus_1(9,7) -> 5 plus_1(9,7) -> 20 plus_1(9,7) -> 24 plus_1(9,8) -> 2 plus_1(9,8) -> 4 plus_1(9,8) -> 5 plus_1(9,8) -> 20 plus_1(9,8) -> 24 plus_1(9,9) -> 2 plus_1(9,9) -> 4 plus_1(9,9) -> 5 plus_1(9,9) -> 20 plus_1(9,9) -> 24 plus_1(9,10) -> 2 plus_1(9,10) -> 4 plus_1(9,10) -> 5 plus_1(9,10) -> 20 plus_1(9,10) -> 24 plus_1(9,13) -> 2 plus_1(9,13) -> 4 plus_1(9,13) -> 5 plus_1(9,13) -> 20 plus_1(9,13) -> 24 plus_1(10,7) -> 2 plus_1(10,7) -> 4 plus_1(10,7) -> 5 plus_1(10,7) -> 20 plus_1(10,7) -> 24 plus_1(10,8) -> 2 plus_1(10,8) -> 4 plus_1(10,8) -> 5 plus_1(10,8) -> 20 plus_1(10,8) -> 24 plus_1(10,9) -> 2 plus_1(10,9) -> 4 plus_1(10,9) -> 5 plus_1(10,9) -> 20 plus_1(10,9) -> 24 plus_1(10,10) -> 2 plus_1(10,10) -> 4 plus_1(10,10) -> 5 plus_1(10,10) -> 20 plus_1(10,10) -> 24 plus_1(10,13) -> 2 plus_1(10,13) -> 4 plus_1(10,13) -> 5 plus_1(10,13) -> 20 plus_1(10,13) -> 24 plus_1(13,7) -> 2 plus_1(13,7) -> 4 plus_1(13,7) -> 5 plus_1(13,7) -> 20 plus_1(13,7) -> 24 plus_1(13,8) -> 2 plus_1(13,8) -> 4 plus_1(13,8) -> 5 plus_1(13,8) -> 20 plus_1(13,8) -> 24 plus_1(13,9) -> 2 plus_1(13,9) -> 4 plus_1(13,9) -> 5 plus_1(13,9) -> 20 plus_1(13,9) -> 24 plus_1(13,10) -> 2 plus_1(13,10) -> 4 plus_1(13,10) -> 5 plus_1(13,10) -> 20 plus_1(13,10) -> 24 plus_1(13,13) -> 2 plus_1(13,13) -> 4 plus_1(13,13) -> 5 plus_1(13,13) -> 20 plus_1(13,13) -> 24 s_0(7) -> 12 s_0(8) -> 12 s_0(9) -> 12 s_0(10) -> 12 s_0(13) -> 12 s_1(7) -> 2 s_1(7) -> 4 s_1(7) -> 5 s_1(7) -> 20 s_1(7) -> 24 s_1(8) -> 2 s_1(8) -> 4 s_1(8) -> 5 s_1(8) -> 20 s_1(8) -> 24 s_1(9) -> 2 s_1(9) -> 4 s_1(9) -> 5 s_1(9) -> 20 s_1(9) -> 24 s_1(10) -> 2 s_1(10) -> 4 s_1(10) -> 5 s_1(10) -> 20 s_1(10) -> 24 s_1(13) -> 2 s_1(13) -> 4 s_1(13) -> 5 s_1(13) -> 20 s_1(13) -> 24 s_1(14) -> 3 tt_0() -> 2 tt_0() -> 4 tt_0() -> 5 tt_0() -> 13 tt_0() -> 20 tt_0() -> 24 tt_1() -> 2 tt_1() -> 4 tt_1() -> 5 tt_1() -> 6 tt_1() -> 15 tt_1() -> 17 tt_1() -> 20 tt_1() -> 21 tt_1() -> 24 tt_2() -> 2 tt_2() -> 4 tt_2() -> 5 tt_2() -> 6 tt_2() -> 15 tt_2() -> 17 tt_2() -> 20 tt_2() -> 21 tt_2() -> 24 tt_3() -> 2 tt_3() -> 4 tt_3() -> 5 tt_3() -> 6 tt_3() -> 15 tt_3() -> 17 tt_3() -> 20 tt_3() -> 21 tt_3() -> 24 7 -> 2 7 -> 4 7 -> 5 7 -> 19 7 -> 20 7 -> 23 7 -> 24 8 -> 2 8 -> 4 8 -> 5 8 -> 20 8 -> 24 9 -> 2 9 -> 4 9 -> 5 9 -> 20 9 -> 24 10 -> 2 10 -> 4 10 -> 5 10 -> 20 10 -> 24 13 -> 2 13 -> 4 13 -> 5 13 -> 20 13 -> 24 16 -> 2 16 -> 4 16 -> 5 16 -> 6 16 -> 15 16 -> 17 16 -> 20 16 -> 21 16 -> 24 18 -> 2 18 -> 4 18 -> 5 18 -> 6 18 -> 15 18 -> 17 18 -> 20 18 -> 21 18 -> 24 22 -> 2 22 -> 4 22 -> 5 22 -> 6 22 -> 15 22 -> 17 22 -> 20 22 -> 21 22 -> 24 * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: 0() -> n__0() U11(tt(),N) -> activate(N) U21(tt(),M,N) -> s(plus(activate(N),activate(M))) activate(X) -> X activate(n__0()) -> 0() activate(n__isNat(X)) -> isNat(X) activate(n__plus(X1,X2)) -> plus(X1,X2) activate(n__s(X)) -> s(X) and(tt(),X) -> activate(X) isNat(X) -> n__isNat(X) isNat(n__0()) -> tt() isNat(n__plus(V1,V2)) -> and(isNat(activate(V1)),n__isNat(activate(V2))) isNat(n__s(V1)) -> isNat(activate(V1)) plus(X1,X2) -> n__plus(X1,X2) s(X) -> n__s(X) - Signature: {0/0,U11/2,U21/3,activate/1,and/2,isNat/1,plus/2,s/1} / {n__0/0,n__isNat/1,n__plus/2,n__s/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,U11,U21,activate,and,isNat,plus ,s} and constructors {n__0,n__isNat,n__plus,n__s,tt} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))