MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(plus(X1,X2)) -> plus(X1,active(X2)) active(plus(X1,X2)) -> plus(active(X1),X2) active(s(X)) -> s(active(X)) active(x(N,0())) -> mark(0()) active(x(N,s(M))) -> mark(plus(x(N,M),N)) active(x(X1,X2)) -> x(X1,active(X2)) active(x(X1,X2)) -> x(active(X1),X2) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(x(X1,X2)) -> x(proper(X1),proper(X2)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) x(X1,mark(X2)) -> mark(x(X1,X2)) x(mark(X1),X2) -> mark(x(X1,X2)) x(ok(X1),ok(X2)) -> ok(x(X1,X2)) - Signature: {active/1,and/2,plus/2,proper/1,s/1,top/1,x/2} / {0/0,mark/1,ok/1,tt/0} - Obligation: innermost runtime complexity wrt. defined symbols {active,and,plus,proper,s,top,x} and constructors {0,mark ,ok,tt} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_2() active#(plus(N,0())) -> c_3() active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) active#(s(X)) -> c_7(s#(active(X)),active#(X)) active#(x(N,0())) -> c_8() active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) and#(mark(X1),X2) -> c_12(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) proper#(0()) -> c_17() proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) proper#(tt()) -> c_21() proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(mark(X)) -> c_23(s#(X)) s#(ok(X)) -> c_24(s#(X)) top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_26(top#(active(X)),active#(X)) x#(X1,mark(X2)) -> c_27(x#(X1,X2)) x#(mark(X1),X2) -> c_28(x#(X1,X2)) x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_2() active#(plus(N,0())) -> c_3() active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) active#(s(X)) -> c_7(s#(active(X)),active#(X)) active#(x(N,0())) -> c_8() active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) and#(mark(X1),X2) -> c_12(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) proper#(0()) -> c_17() proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) proper#(tt()) -> c_21() proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(mark(X)) -> c_23(s#(X)) s#(ok(X)) -> c_24(s#(X)) top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_26(top#(active(X)),active#(X)) x#(X1,mark(X2)) -> c_27(x#(X1,X2)) x#(mark(X1),X2) -> c_28(x#(X1,X2)) x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) - Weak TRS: active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(plus(X1,X2)) -> plus(X1,active(X2)) active(plus(X1,X2)) -> plus(active(X1),X2) active(s(X)) -> s(active(X)) active(x(N,0())) -> mark(0()) active(x(N,s(M))) -> mark(plus(x(N,M),N)) active(x(X1,X2)) -> x(X1,active(X2)) active(x(X1,X2)) -> x(active(X1),X2) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(x(X1,X2)) -> x(proper(X1),proper(X2)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) x(X1,mark(X2)) -> mark(x(X1,X2)) x(mark(X1),X2) -> mark(x(X1,X2)) x(ok(X1),ok(X2)) -> ok(x(X1,X2)) - Signature: {active/1,and/2,plus/2,proper/1,s/1,top/1,x/2,active#/1,and#/2,plus#/2,proper#/1,s#/1,top#/1,x#/2} / {0/0 ,mark/1,ok/1,tt/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/2,c_6/2,c_7/2,c_8/0,c_9/2,c_10/2,c_11/2,c_12/1,c_13/1,c_14/1 ,c_15/1,c_16/1,c_17/0,c_18/3,c_19/3,c_20/2,c_21/0,c_22/3,c_23/1,c_24/1,c_25/2,c_26/2,c_27/1,c_28/1,c_29/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,and#,plus#,proper#,s#,top# ,x#} and constructors {0,mark,ok,tt} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(plus(X1,X2)) -> plus(X1,active(X2)) active(plus(X1,X2)) -> plus(active(X1),X2) active(s(X)) -> s(active(X)) active(x(N,0())) -> mark(0()) active(x(N,s(M))) -> mark(plus(x(N,M),N)) active(x(X1,X2)) -> x(X1,active(X2)) active(x(X1,X2)) -> x(active(X1),X2) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(x(X1,X2)) -> x(proper(X1),proper(X2)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) x(X1,mark(X2)) -> mark(x(X1,X2)) x(mark(X1),X2) -> mark(x(X1,X2)) x(ok(X1),ok(X2)) -> ok(x(X1,X2)) active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_2() active#(plus(N,0())) -> c_3() active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) active#(s(X)) -> c_7(s#(active(X)),active#(X)) active#(x(N,0())) -> c_8() active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) and#(mark(X1),X2) -> c_12(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) proper#(0()) -> c_17() proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) proper#(tt()) -> c_21() proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(mark(X)) -> c_23(s#(X)) s#(ok(X)) -> c_24(s#(X)) top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_26(top#(active(X)),active#(X)) x#(X1,mark(X2)) -> c_27(x#(X1,X2)) x#(mark(X1),X2) -> c_28(x#(X1,X2)) x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_2() active#(plus(N,0())) -> c_3() active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) active#(s(X)) -> c_7(s#(active(X)),active#(X)) active#(x(N,0())) -> c_8() active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) and#(mark(X1),X2) -> c_12(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) proper#(0()) -> c_17() proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) proper#(tt()) -> c_21() proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(mark(X)) -> c_23(s#(X)) s#(ok(X)) -> c_24(s#(X)) top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_26(top#(active(X)),active#(X)) x#(X1,mark(X2)) -> c_27(x#(X1,X2)) x#(mark(X1),X2) -> c_28(x#(X1,X2)) x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) - Weak TRS: active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(plus(X1,X2)) -> plus(X1,active(X2)) active(plus(X1,X2)) -> plus(active(X1),X2) active(s(X)) -> s(active(X)) active(x(N,0())) -> mark(0()) active(x(N,s(M))) -> mark(plus(x(N,M),N)) active(x(X1,X2)) -> x(X1,active(X2)) active(x(X1,X2)) -> x(active(X1),X2) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(x(X1,X2)) -> x(proper(X1),proper(X2)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) x(X1,mark(X2)) -> mark(x(X1,X2)) x(mark(X1),X2) -> mark(x(X1,X2)) x(ok(X1),ok(X2)) -> ok(x(X1,X2)) - Signature: {active/1,and/2,plus/2,proper/1,s/1,top/1,x/2,active#/1,and#/2,plus#/2,proper#/1,s#/1,top#/1,x#/2} / {0/0 ,mark/1,ok/1,tt/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/2,c_6/2,c_7/2,c_8/0,c_9/2,c_10/2,c_11/2,c_12/1,c_13/1,c_14/1 ,c_15/1,c_16/1,c_17/0,c_18/3,c_19/3,c_20/2,c_21/0,c_22/3,c_23/1,c_24/1,c_25/2,c_26/2,c_27/1,c_28/1,c_29/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,and#,plus#,proper#,s#,top# ,x#} and constructors {0,mark,ok,tt} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,8,17,21} by application of Pre({2,3,8,17,21}) = {1,5,6,7,10,11,18,19,20,22,25,26}. Here rules are labelled as follows: 1: active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) 2: active#(and(tt(),X)) -> c_2() 3: active#(plus(N,0())) -> c_3() 4: active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) 5: active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) 6: active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) 7: active#(s(X)) -> c_7(s#(active(X)),active#(X)) 8: active#(x(N,0())) -> c_8() 9: active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) 10: active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) 11: active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) 12: and#(mark(X1),X2) -> c_12(and#(X1,X2)) 13: and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) 14: plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) 15: plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) 16: plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) 17: proper#(0()) -> c_17() 18: proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 19: proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 20: proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) 21: proper#(tt()) -> c_21() 22: proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 23: s#(mark(X)) -> c_23(s#(X)) 24: s#(ok(X)) -> c_24(s#(X)) 25: top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) 26: top#(ok(X)) -> c_26(top#(active(X)),active#(X)) 27: x#(X1,mark(X2)) -> c_27(x#(X1,X2)) 28: x#(mark(X1),X2) -> c_28(x#(X1,X2)) 29: x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) active#(s(X)) -> c_7(s#(active(X)),active#(X)) active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) and#(mark(X1),X2) -> c_12(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(mark(X)) -> c_23(s#(X)) s#(ok(X)) -> c_24(s#(X)) top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_26(top#(active(X)),active#(X)) x#(X1,mark(X2)) -> c_27(x#(X1,X2)) x#(mark(X1),X2) -> c_28(x#(X1,X2)) x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) - Weak DPs: active#(and(tt(),X)) -> c_2() active#(plus(N,0())) -> c_3() active#(x(N,0())) -> c_8() proper#(0()) -> c_17() proper#(tt()) -> c_21() - Weak TRS: active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(plus(X1,X2)) -> plus(X1,active(X2)) active(plus(X1,X2)) -> plus(active(X1),X2) active(s(X)) -> s(active(X)) active(x(N,0())) -> mark(0()) active(x(N,s(M))) -> mark(plus(x(N,M),N)) active(x(X1,X2)) -> x(X1,active(X2)) active(x(X1,X2)) -> x(active(X1),X2) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(x(X1,X2)) -> x(proper(X1),proper(X2)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) x(X1,mark(X2)) -> mark(x(X1,X2)) x(mark(X1),X2) -> mark(x(X1,X2)) x(ok(X1),ok(X2)) -> ok(x(X1,X2)) - Signature: {active/1,and/2,plus/2,proper/1,s/1,top/1,x/2,active#/1,and#/2,plus#/2,proper#/1,s#/1,top#/1,x#/2} / {0/0 ,mark/1,ok/1,tt/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/2,c_6/2,c_7/2,c_8/0,c_9/2,c_10/2,c_11/2,c_12/1,c_13/1,c_14/1 ,c_15/1,c_16/1,c_17/0,c_18/3,c_19/3,c_20/2,c_21/0,c_22/3,c_23/1,c_24/1,c_25/2,c_26/2,c_27/1,c_28/1,c_29/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,and#,plus#,proper#,s#,top# ,x#} and constructors {0,mark,ok,tt} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) -->_1 and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)):10 -->_1 and#(mark(X1),X2) -> c_12(and#(X1,X2)):9 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 2:S:active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) -->_1 s#(ok(X)) -> c_24(s#(X)):19 -->_1 s#(mark(X)) -> c_23(s#(X)):18 -->_2 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_2 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_2 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 3:S:active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 4:S:active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 5:S:active#(s(X)) -> c_7(s#(active(X)),active#(X)) -->_1 s#(ok(X)) -> c_24(s#(X)):19 -->_1 s#(mark(X)) -> c_23(s#(X)):18 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 6:S:active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) -->_2 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_2 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_2 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 7:S:active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) -->_1 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_1 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_1 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 8:S:active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) -->_1 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_1 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_1 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 9:S:and#(mark(X1),X2) -> c_12(and#(X1,X2)) -->_1 and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)):10 -->_1 and#(mark(X1),X2) -> c_12(and#(X1,X2)):9 10:S:and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) -->_1 and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)):10 -->_1 and#(mark(X1),X2) -> c_12(and#(X1,X2)):9 11:S:plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 12:S:plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 13:S:plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 14:S:proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_2 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_3 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_2 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_3 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_3 proper#(tt()) -> c_21():29 -->_2 proper#(tt()) -> c_21():29 -->_3 proper#(0()) -> c_17():28 -->_2 proper#(0()) -> c_17():28 -->_3 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 -->_2 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 -->_1 and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)):10 -->_1 and#(mark(X1),X2) -> c_12(and#(X1,X2)):9 15:S:proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_2 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_3 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_2 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_3 proper#(tt()) -> c_21():29 -->_2 proper#(tt()) -> c_21():29 -->_3 proper#(0()) -> c_17():28 -->_2 proper#(0()) -> c_17():28 -->_3 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_3 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 -->_2 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 -->_1 plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)):13 -->_1 plus#(mark(X1),X2) -> c_15(plus#(X1,X2)):12 -->_1 plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)):11 16:S:proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_24(s#(X)):19 -->_1 s#(mark(X)) -> c_23(s#(X)):18 -->_2 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_2 proper#(tt()) -> c_21():29 -->_2 proper#(0()) -> c_17():28 -->_2 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_2 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 17:S:proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_1 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_1 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_1 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 -->_3 proper#(tt()) -> c_21():29 -->_2 proper#(tt()) -> c_21():29 -->_3 proper#(0()) -> c_17():28 -->_2 proper#(0()) -> c_17():28 -->_3 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_2 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_3 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_2 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_3 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_3 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 -->_2 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 18:S:s#(mark(X)) -> c_23(s#(X)) -->_1 s#(ok(X)) -> c_24(s#(X)):19 -->_1 s#(mark(X)) -> c_23(s#(X)):18 19:S:s#(ok(X)) -> c_24(s#(X)) -->_1 s#(ok(X)) -> c_24(s#(X)):19 -->_1 s#(mark(X)) -> c_23(s#(X)):18 20:S:top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_26(top#(active(X)),active#(X)):21 -->_2 proper#(tt()) -> c_21():29 -->_2 proper#(0()) -> c_17():28 -->_1 top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)):20 -->_2 proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):17 -->_2 proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)):16 -->_2 proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):15 -->_2 proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):14 21:S:top#(ok(X)) -> c_26(top#(active(X)),active#(X)) -->_2 active#(x(N,0())) -> c_8():27 -->_2 active#(plus(N,0())) -> c_3():26 -->_2 active#(and(tt(),X)) -> c_2():25 -->_1 top#(ok(X)) -> c_26(top#(active(X)),active#(X)):21 -->_1 top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)):20 -->_2 active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)):8 -->_2 active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)):7 -->_2 active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)):6 -->_2 active#(s(X)) -> c_7(s#(active(X)),active#(X)):5 -->_2 active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)):4 -->_2 active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)):3 -->_2 active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)):2 -->_2 active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)):1 22:S:x#(X1,mark(X2)) -> c_27(x#(X1,X2)) -->_1 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_1 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_1 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 23:S:x#(mark(X1),X2) -> c_28(x#(X1,X2)) -->_1 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_1 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_1 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 24:S:x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) -->_1 x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)):24 -->_1 x#(mark(X1),X2) -> c_28(x#(X1,X2)):23 -->_1 x#(X1,mark(X2)) -> c_27(x#(X1,X2)):22 25:W:active#(and(tt(),X)) -> c_2() 26:W:active#(plus(N,0())) -> c_3() 27:W:active#(x(N,0())) -> c_8() 28:W:proper#(0()) -> c_17() 29:W:proper#(tt()) -> c_21() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 28: proper#(0()) -> c_17() 29: proper#(tt()) -> c_21() 25: active#(and(tt(),X)) -> c_2() 26: active#(plus(N,0())) -> c_3() 27: active#(x(N,0())) -> c_8() * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: active#(and(X1,X2)) -> c_1(and#(active(X1),X2),active#(X1)) active#(plus(N,s(M))) -> c_4(s#(plus(N,M)),plus#(N,M)) active#(plus(X1,X2)) -> c_5(plus#(X1,active(X2)),active#(X2)) active#(plus(X1,X2)) -> c_6(plus#(active(X1),X2),active#(X1)) active#(s(X)) -> c_7(s#(active(X)),active#(X)) active#(x(N,s(M))) -> c_9(plus#(x(N,M),N),x#(N,M)) active#(x(X1,X2)) -> c_10(x#(X1,active(X2)),active#(X2)) active#(x(X1,X2)) -> c_11(x#(active(X1),X2),active#(X1)) and#(mark(X1),X2) -> c_12(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_13(and#(X1,X2)) plus#(X1,mark(X2)) -> c_14(plus#(X1,X2)) plus#(mark(X1),X2) -> c_15(plus#(X1,X2)) plus#(ok(X1),ok(X2)) -> c_16(plus#(X1,X2)) proper#(and(X1,X2)) -> c_18(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(plus(X1,X2)) -> c_19(plus#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(s(X)) -> c_20(s#(proper(X)),proper#(X)) proper#(x(X1,X2)) -> c_22(x#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) s#(mark(X)) -> c_23(s#(X)) s#(ok(X)) -> c_24(s#(X)) top#(mark(X)) -> c_25(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_26(top#(active(X)),active#(X)) x#(X1,mark(X2)) -> c_27(x#(X1,X2)) x#(mark(X1),X2) -> c_28(x#(X1,X2)) x#(ok(X1),ok(X2)) -> c_29(x#(X1,X2)) - Weak TRS: active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(plus(N,0())) -> mark(N) active(plus(N,s(M))) -> mark(s(plus(N,M))) active(plus(X1,X2)) -> plus(X1,active(X2)) active(plus(X1,X2)) -> plus(active(X1),X2) active(s(X)) -> s(active(X)) active(x(N,0())) -> mark(0()) active(x(N,s(M))) -> mark(plus(x(N,M),N)) active(x(X1,X2)) -> x(X1,active(X2)) active(x(X1,X2)) -> x(active(X1),X2) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) plus(X1,mark(X2)) -> mark(plus(X1,X2)) plus(mark(X1),X2) -> mark(plus(X1,X2)) plus(ok(X1),ok(X2)) -> ok(plus(X1,X2)) proper(0()) -> ok(0()) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(plus(X1,X2)) -> plus(proper(X1),proper(X2)) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(x(X1,X2)) -> x(proper(X1),proper(X2)) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) x(X1,mark(X2)) -> mark(x(X1,X2)) x(mark(X1),X2) -> mark(x(X1,X2)) x(ok(X1),ok(X2)) -> ok(x(X1,X2)) - Signature: {active/1,and/2,plus/2,proper/1,s/1,top/1,x/2,active#/1,and#/2,plus#/2,proper#/1,s#/1,top#/1,x#/2} / {0/0 ,mark/1,ok/1,tt/0,c_1/2,c_2/0,c_3/0,c_4/2,c_5/2,c_6/2,c_7/2,c_8/0,c_9/2,c_10/2,c_11/2,c_12/1,c_13/1,c_14/1 ,c_15/1,c_16/1,c_17/0,c_18/3,c_19/3,c_20/2,c_21/0,c_22/3,c_23/1,c_24/1,c_25/2,c_26/2,c_27/1,c_28/1,c_29/1} - Obligation: innermost runtime complexity wrt. defined symbols {active#,and#,plus#,proper#,s#,top# ,x#} and constructors {0,mark,ok,tt} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE