MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: U11(mark(X1),X2) -> mark(U11(X1,X2)) U11(ok(X1),ok(X2)) -> ok(U11(X1,X2)) active(U11(X1,X2)) -> U11(active(X1),X2) active(U11(tt(),L)) -> mark(s(length(L))) active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(cons(X1,X2)) -> cons(active(X1),X2) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatIList(zeros())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(isNatList(nil())) -> mark(tt()) active(length(X)) -> length(active(X)) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) active(length(nil())) -> mark(0()) active(s(X)) -> s(active(X)) active(zeros()) -> mark(cons(0(),zeros())) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) isNat(ok(X)) -> ok(isNat(X)) isNatIList(ok(X)) -> ok(isNatIList(X)) isNatList(ok(X)) -> ok(isNatList(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(U11(X1,X2)) -> U11(proper(X1),proper(X2)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(isNat(X)) -> isNat(proper(X)) proper(isNatIList(X)) -> isNatIList(proper(X)) proper(isNatList(X)) -> isNatList(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(zeros()) -> ok(zeros()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1} / {0/0,mark/1 ,nil/0,ok/1,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {U11,active,and,cons,isNat,isNatIList,isNatList,length ,proper,s,top} and constructors {0,mark,nil,ok,tt,zeros} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_6() active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) active#(isNat(0())) -> c_8() active#(isNat(length(V1))) -> c_9(isNatList#(V1)) active#(isNat(s(V1))) -> c_10(isNat#(V1)) active#(isNatIList(V)) -> c_11(isNatList#(V)) active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) active#(isNatIList(zeros())) -> c_13() active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) active#(isNatList(nil())) -> c_15() active#(length(X)) -> c_16(length#(active(X)),active#(X)) active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) active#(length(nil())) -> c_18() active#(s(X)) -> c_19(s#(active(X)),active#(X)) active#(zeros()) -> c_20(cons#(0(),zeros())) and#(mark(X1),X2) -> c_21(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) isNat#(ok(X)) -> c_25(isNat#(X)) isNatIList#(ok(X)) -> c_26(isNatIList#(X)) isNatList#(ok(X)) -> c_27(isNatList#(X)) length#(mark(X)) -> c_28(length#(X)) length#(ok(X)) -> c_29(length#(X)) proper#(0()) -> c_30() proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) proper#(nil()) -> c_38() proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) proper#(tt()) -> c_40() proper#(zeros()) -> c_41() s#(mark(X)) -> c_42(s#(X)) s#(ok(X)) -> c_43(s#(X)) top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_45(top#(active(X)),active#(X)) Weak DPs and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_6() active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) active#(isNat(0())) -> c_8() active#(isNat(length(V1))) -> c_9(isNatList#(V1)) active#(isNat(s(V1))) -> c_10(isNat#(V1)) active#(isNatIList(V)) -> c_11(isNatList#(V)) active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) active#(isNatIList(zeros())) -> c_13() active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) active#(isNatList(nil())) -> c_15() active#(length(X)) -> c_16(length#(active(X)),active#(X)) active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) active#(length(nil())) -> c_18() active#(s(X)) -> c_19(s#(active(X)),active#(X)) active#(zeros()) -> c_20(cons#(0(),zeros())) and#(mark(X1),X2) -> c_21(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) isNat#(ok(X)) -> c_25(isNat#(X)) isNatIList#(ok(X)) -> c_26(isNatIList#(X)) isNatList#(ok(X)) -> c_27(isNatList#(X)) length#(mark(X)) -> c_28(length#(X)) length#(ok(X)) -> c_29(length#(X)) proper#(0()) -> c_30() proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) proper#(nil()) -> c_38() proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) proper#(tt()) -> c_40() proper#(zeros()) -> c_41() s#(mark(X)) -> c_42(s#(X)) s#(ok(X)) -> c_43(s#(X)) top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_45(top#(active(X)),active#(X)) - Weak TRS: U11(mark(X1),X2) -> mark(U11(X1,X2)) U11(ok(X1),ok(X2)) -> ok(U11(X1,X2)) active(U11(X1,X2)) -> U11(active(X1),X2) active(U11(tt(),L)) -> mark(s(length(L))) active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(cons(X1,X2)) -> cons(active(X1),X2) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatIList(zeros())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(isNatList(nil())) -> mark(tt()) active(length(X)) -> length(active(X)) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) active(length(nil())) -> mark(0()) active(s(X)) -> s(active(X)) active(zeros()) -> mark(cons(0(),zeros())) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) isNat(ok(X)) -> ok(isNat(X)) isNatIList(ok(X)) -> ok(isNatIList(X)) isNatList(ok(X)) -> ok(isNatList(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(U11(X1,X2)) -> U11(proper(X1),proper(X2)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(isNat(X)) -> isNat(proper(X)) proper(isNatIList(X)) -> isNatIList(proper(X)) proper(isNatList(X)) -> isNatList(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(zeros()) -> ok(zeros()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) top(mark(X)) -> top(proper(X)) top(ok(X)) -> top(active(X)) - Signature: {U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1,U11#/2,active#/1 ,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,proper#/1,s#/1,top#/1} / {0/0,mark/1,nil/0 ,ok/1,tt/0,zeros/0,c_1/1,c_2/1,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2,c_8/0,c_9/1,c_10/1,c_11/1,c_12/3,c_13/0,c_14/3 ,c_15/0,c_16/2,c_17/4,c_18/0,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1 ,c_30/0,c_31/3,c_32/3,c_33/3,c_34/2,c_35/2,c_36/2,c_37/2,c_38/0,c_39/2,c_40/0,c_41/0,c_42/1,c_43/1,c_44/2 ,c_45/2} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,active#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,proper#,s#,top#} and constructors {0,mark,nil,ok,tt,zeros} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: U11(mark(X1),X2) -> mark(U11(X1,X2)) U11(ok(X1),ok(X2)) -> ok(U11(X1,X2)) active(U11(X1,X2)) -> U11(active(X1),X2) active(U11(tt(),L)) -> mark(s(length(L))) active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(cons(X1,X2)) -> cons(active(X1),X2) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatIList(zeros())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(isNatList(nil())) -> mark(tt()) active(length(X)) -> length(active(X)) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) active(length(nil())) -> mark(0()) active(s(X)) -> s(active(X)) active(zeros()) -> mark(cons(0(),zeros())) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) isNat(ok(X)) -> ok(isNat(X)) isNatIList(ok(X)) -> ok(isNatIList(X)) isNatList(ok(X)) -> ok(isNatList(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(U11(X1,X2)) -> U11(proper(X1),proper(X2)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(isNat(X)) -> isNat(proper(X)) proper(isNatIList(X)) -> isNatIList(proper(X)) proper(isNatList(X)) -> isNatList(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(zeros()) -> ok(zeros()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_6() active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) active#(isNat(0())) -> c_8() active#(isNat(length(V1))) -> c_9(isNatList#(V1)) active#(isNat(s(V1))) -> c_10(isNat#(V1)) active#(isNatIList(V)) -> c_11(isNatList#(V)) active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) active#(isNatIList(zeros())) -> c_13() active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) active#(isNatList(nil())) -> c_15() active#(length(X)) -> c_16(length#(active(X)),active#(X)) active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) active#(length(nil())) -> c_18() active#(s(X)) -> c_19(s#(active(X)),active#(X)) active#(zeros()) -> c_20(cons#(0(),zeros())) and#(mark(X1),X2) -> c_21(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) isNat#(ok(X)) -> c_25(isNat#(X)) isNatIList#(ok(X)) -> c_26(isNatIList#(X)) isNatList#(ok(X)) -> c_27(isNatList#(X)) length#(mark(X)) -> c_28(length#(X)) length#(ok(X)) -> c_29(length#(X)) proper#(0()) -> c_30() proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) proper#(nil()) -> c_38() proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) proper#(tt()) -> c_40() proper#(zeros()) -> c_41() s#(mark(X)) -> c_42(s#(X)) s#(ok(X)) -> c_43(s#(X)) top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_45(top#(active(X)),active#(X)) * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) active#(and(tt(),X)) -> c_6() active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) active#(isNat(0())) -> c_8() active#(isNat(length(V1))) -> c_9(isNatList#(V1)) active#(isNat(s(V1))) -> c_10(isNat#(V1)) active#(isNatIList(V)) -> c_11(isNatList#(V)) active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) active#(isNatIList(zeros())) -> c_13() active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) active#(isNatList(nil())) -> c_15() active#(length(X)) -> c_16(length#(active(X)),active#(X)) active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) active#(length(nil())) -> c_18() active#(s(X)) -> c_19(s#(active(X)),active#(X)) active#(zeros()) -> c_20(cons#(0(),zeros())) and#(mark(X1),X2) -> c_21(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) isNat#(ok(X)) -> c_25(isNat#(X)) isNatIList#(ok(X)) -> c_26(isNatIList#(X)) isNatList#(ok(X)) -> c_27(isNatList#(X)) length#(mark(X)) -> c_28(length#(X)) length#(ok(X)) -> c_29(length#(X)) proper#(0()) -> c_30() proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) proper#(nil()) -> c_38() proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) proper#(tt()) -> c_40() proper#(zeros()) -> c_41() s#(mark(X)) -> c_42(s#(X)) s#(ok(X)) -> c_43(s#(X)) top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_45(top#(active(X)),active#(X)) - Weak TRS: U11(mark(X1),X2) -> mark(U11(X1,X2)) U11(ok(X1),ok(X2)) -> ok(U11(X1,X2)) active(U11(X1,X2)) -> U11(active(X1),X2) active(U11(tt(),L)) -> mark(s(length(L))) active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(cons(X1,X2)) -> cons(active(X1),X2) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatIList(zeros())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(isNatList(nil())) -> mark(tt()) active(length(X)) -> length(active(X)) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) active(length(nil())) -> mark(0()) active(s(X)) -> s(active(X)) active(zeros()) -> mark(cons(0(),zeros())) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) isNat(ok(X)) -> ok(isNat(X)) isNatIList(ok(X)) -> ok(isNatIList(X)) isNatList(ok(X)) -> ok(isNatList(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(U11(X1,X2)) -> U11(proper(X1),proper(X2)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(isNat(X)) -> isNat(proper(X)) proper(isNatIList(X)) -> isNatIList(proper(X)) proper(isNatList(X)) -> isNatList(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(zeros()) -> ok(zeros()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1,U11#/2,active#/1 ,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,proper#/1,s#/1,top#/1} / {0/0,mark/1,nil/0 ,ok/1,tt/0,zeros/0,c_1/1,c_2/1,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2,c_8/0,c_9/1,c_10/1,c_11/1,c_12/3,c_13/0,c_14/3 ,c_15/0,c_16/2,c_17/4,c_18/0,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1 ,c_30/0,c_31/3,c_32/3,c_33/3,c_34/2,c_35/2,c_36/2,c_37/2,c_38/0,c_39/2,c_40/0,c_41/0,c_42/1,c_43/1,c_44/2 ,c_45/2} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,active#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,proper#,s#,top#} and constructors {0,mark,nil,ok,tt,zeros} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {6,8,13,15,18,20,30,38,40,41} by application of Pre({6,8,13,15,18,20,30,38,40,41}) = {3,5,7,16,19,31,32,33,34,35,36,37,39,44,45}. Here rules are labelled as follows: 1: U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) 2: U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) 3: active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) 4: active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) 5: active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) 6: active#(and(tt(),X)) -> c_6() 7: active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) 8: active#(isNat(0())) -> c_8() 9: active#(isNat(length(V1))) -> c_9(isNatList#(V1)) 10: active#(isNat(s(V1))) -> c_10(isNat#(V1)) 11: active#(isNatIList(V)) -> c_11(isNatList#(V)) 12: active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) 13: active#(isNatIList(zeros())) -> c_13() 14: active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) 15: active#(isNatList(nil())) -> c_15() 16: active#(length(X)) -> c_16(length#(active(X)),active#(X)) 17: active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) 18: active#(length(nil())) -> c_18() 19: active#(s(X)) -> c_19(s#(active(X)),active#(X)) 20: active#(zeros()) -> c_20(cons#(0(),zeros())) 21: and#(mark(X1),X2) -> c_21(and#(X1,X2)) 22: and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) 23: cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) 24: cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) 25: isNat#(ok(X)) -> c_25(isNat#(X)) 26: isNatIList#(ok(X)) -> c_26(isNatIList#(X)) 27: isNatList#(ok(X)) -> c_27(isNatList#(X)) 28: length#(mark(X)) -> c_28(length#(X)) 29: length#(ok(X)) -> c_29(length#(X)) 30: proper#(0()) -> c_30() 31: proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 32: proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 33: proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) 34: proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) 35: proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) 36: proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) 37: proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) 38: proper#(nil()) -> c_38() 39: proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) 40: proper#(tt()) -> c_40() 41: proper#(zeros()) -> c_41() 42: s#(mark(X)) -> c_42(s#(X)) 43: s#(ok(X)) -> c_43(s#(X)) 44: top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) 45: top#(ok(X)) -> c_45(top#(active(X)),active#(X)) * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) active#(isNat(length(V1))) -> c_9(isNatList#(V1)) active#(isNat(s(V1))) -> c_10(isNat#(V1)) active#(isNatIList(V)) -> c_11(isNatList#(V)) active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) active#(length(X)) -> c_16(length#(active(X)),active#(X)) active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) active#(s(X)) -> c_19(s#(active(X)),active#(X)) and#(mark(X1),X2) -> c_21(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) isNat#(ok(X)) -> c_25(isNat#(X)) isNatIList#(ok(X)) -> c_26(isNatIList#(X)) isNatList#(ok(X)) -> c_27(isNatList#(X)) length#(mark(X)) -> c_28(length#(X)) length#(ok(X)) -> c_29(length#(X)) proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_42(s#(X)) s#(ok(X)) -> c_43(s#(X)) top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_45(top#(active(X)),active#(X)) - Weak DPs: active#(and(tt(),X)) -> c_6() active#(isNat(0())) -> c_8() active#(isNatIList(zeros())) -> c_13() active#(isNatList(nil())) -> c_15() active#(length(nil())) -> c_18() active#(zeros()) -> c_20(cons#(0(),zeros())) proper#(0()) -> c_30() proper#(nil()) -> c_38() proper#(tt()) -> c_40() proper#(zeros()) -> c_41() - Weak TRS: U11(mark(X1),X2) -> mark(U11(X1,X2)) U11(ok(X1),ok(X2)) -> ok(U11(X1,X2)) active(U11(X1,X2)) -> U11(active(X1),X2) active(U11(tt(),L)) -> mark(s(length(L))) active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(cons(X1,X2)) -> cons(active(X1),X2) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatIList(zeros())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(isNatList(nil())) -> mark(tt()) active(length(X)) -> length(active(X)) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) active(length(nil())) -> mark(0()) active(s(X)) -> s(active(X)) active(zeros()) -> mark(cons(0(),zeros())) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) isNat(ok(X)) -> ok(isNat(X)) isNatIList(ok(X)) -> ok(isNatIList(X)) isNatList(ok(X)) -> ok(isNatList(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(U11(X1,X2)) -> U11(proper(X1),proper(X2)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(isNat(X)) -> isNat(proper(X)) proper(isNatIList(X)) -> isNatIList(proper(X)) proper(isNatList(X)) -> isNatList(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(zeros()) -> ok(zeros()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1,U11#/2,active#/1 ,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,proper#/1,s#/1,top#/1} / {0/0,mark/1,nil/0 ,ok/1,tt/0,zeros/0,c_1/1,c_2/1,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2,c_8/0,c_9/1,c_10/1,c_11/1,c_12/3,c_13/0,c_14/3 ,c_15/0,c_16/2,c_17/4,c_18/0,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1 ,c_30/0,c_31/3,c_32/3,c_33/3,c_34/2,c_35/2,c_36/2,c_37/2,c_38/0,c_39/2,c_40/0,c_41/0,c_42/1,c_43/1,c_44/2 ,c_45/2} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,active#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,proper#,s#,top#} and constructors {0,mark,nil,ok,tt,zeros} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) -->_1 U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)):2 -->_1 U11#(mark(X1),X2) -> c_1(U11#(X1,X2)):1 2:S:U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) -->_1 U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)):2 -->_1 U11#(mark(X1),X2) -> c_1(U11#(X1,X2)):1 3:S:active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) -->_2 active#(s(X)) -> c_19(s#(active(X)),active#(X)):14 -->_2 active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)):13 -->_2 active#(length(X)) -> c_16(length#(active(X)),active#(X)):12 -->_2 active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)):11 -->_2 active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)) ,isNat#(V1) ,isNatIList#(V2)):10 -->_2 active#(isNatIList(V)) -> c_11(isNatList#(V)):9 -->_2 active#(isNat(s(V1))) -> c_10(isNat#(V1)):8 -->_2 active#(isNat(length(V1))) -> c_9(isNatList#(V1)):7 -->_2 active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)):6 -->_2 active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)):5 -->_2 active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)):4 -->_2 active#(zeros()) -> c_20(cons#(0(),zeros())):41 -->_2 active#(length(nil())) -> c_18():40 -->_2 active#(isNatList(nil())) -> c_15():39 -->_2 active#(isNatIList(zeros())) -> c_13():38 -->_2 active#(isNat(0())) -> c_8():37 -->_2 active#(and(tt(),X)) -> c_6():36 -->_2 active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)):3 -->_1 U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)):2 -->_1 U11#(mark(X1),X2) -> c_1(U11#(X1,X2)):1 4:S:active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) -->_1 s#(ok(X)) -> c_43(s#(X)):33 -->_1 s#(mark(X)) -> c_42(s#(X)):32 -->_2 length#(ok(X)) -> c_29(length#(X)):23 -->_2 length#(mark(X)) -> c_28(length#(X)):22 5:S:active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) -->_1 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_1 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 -->_2 active#(s(X)) -> c_19(s#(active(X)),active#(X)):14 -->_2 active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)):13 -->_2 active#(length(X)) -> c_16(length#(active(X)),active#(X)):12 -->_2 active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)):11 -->_2 active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)) ,isNat#(V1) ,isNatIList#(V2)):10 -->_2 active#(isNatIList(V)) -> c_11(isNatList#(V)):9 -->_2 active#(isNat(s(V1))) -> c_10(isNat#(V1)):8 -->_2 active#(isNat(length(V1))) -> c_9(isNatList#(V1)):7 -->_2 active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)):6 -->_2 active#(zeros()) -> c_20(cons#(0(),zeros())):41 -->_2 active#(length(nil())) -> c_18():40 -->_2 active#(isNatList(nil())) -> c_15():39 -->_2 active#(isNatIList(zeros())) -> c_13():38 -->_2 active#(isNat(0())) -> c_8():37 -->_2 active#(and(tt(),X)) -> c_6():36 -->_2 active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)):5 -->_2 active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)):4 -->_2 active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)):3 6:S:active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) -->_1 cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)):18 -->_1 cons#(mark(X1),X2) -> c_23(cons#(X1,X2)):17 -->_2 active#(s(X)) -> c_19(s#(active(X)),active#(X)):14 -->_2 active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)):13 -->_2 active#(length(X)) -> c_16(length#(active(X)),active#(X)):12 -->_2 active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)):11 -->_2 active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)) ,isNat#(V1) ,isNatIList#(V2)):10 -->_2 active#(isNatIList(V)) -> c_11(isNatList#(V)):9 -->_2 active#(isNat(s(V1))) -> c_10(isNat#(V1)):8 -->_2 active#(isNat(length(V1))) -> c_9(isNatList#(V1)):7 -->_2 active#(zeros()) -> c_20(cons#(0(),zeros())):41 -->_2 active#(length(nil())) -> c_18():40 -->_2 active#(isNatList(nil())) -> c_15():39 -->_2 active#(isNatIList(zeros())) -> c_13():38 -->_2 active#(isNat(0())) -> c_8():37 -->_2 active#(and(tt(),X)) -> c_6():36 -->_2 active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)):6 -->_2 active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)):5 -->_2 active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)):4 -->_2 active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)):3 7:S:active#(isNat(length(V1))) -> c_9(isNatList#(V1)) -->_1 isNatList#(ok(X)) -> c_27(isNatList#(X)):21 8:S:active#(isNat(s(V1))) -> c_10(isNat#(V1)) -->_1 isNat#(ok(X)) -> c_25(isNat#(X)):19 9:S:active#(isNatIList(V)) -> c_11(isNatList#(V)) -->_1 isNatList#(ok(X)) -> c_27(isNatList#(X)):21 10:S:active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) -->_3 isNatIList#(ok(X)) -> c_26(isNatIList#(X)):20 -->_2 isNat#(ok(X)) -> c_25(isNat#(X)):19 -->_1 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_1 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 11:S:active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) -->_3 isNatList#(ok(X)) -> c_27(isNatList#(X)):21 -->_2 isNat#(ok(X)) -> c_25(isNat#(X)):19 -->_1 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_1 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 12:S:active#(length(X)) -> c_16(length#(active(X)),active#(X)) -->_1 length#(ok(X)) -> c_29(length#(X)):23 -->_1 length#(mark(X)) -> c_28(length#(X)):22 -->_2 active#(s(X)) -> c_19(s#(active(X)),active#(X)):14 -->_2 active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)):13 -->_2 active#(zeros()) -> c_20(cons#(0(),zeros())):41 -->_2 active#(length(nil())) -> c_18():40 -->_2 active#(isNatList(nil())) -> c_15():39 -->_2 active#(isNatIList(zeros())) -> c_13():38 -->_2 active#(isNat(0())) -> c_8():37 -->_2 active#(and(tt(),X)) -> c_6():36 -->_2 active#(length(X)) -> c_16(length#(active(X)),active#(X)):12 -->_2 active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)):11 -->_2 active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)) ,isNat#(V1) ,isNatIList#(V2)):10 -->_2 active#(isNatIList(V)) -> c_11(isNatList#(V)):9 -->_2 active#(isNat(s(V1))) -> c_10(isNat#(V1)):8 -->_2 active#(isNat(length(V1))) -> c_9(isNatList#(V1)):7 -->_2 active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)):6 -->_2 active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)):5 -->_2 active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)):4 -->_2 active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)):3 13:S:active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) -->_3 isNatList#(ok(X)) -> c_27(isNatList#(X)):21 -->_4 isNat#(ok(X)) -> c_25(isNat#(X)):19 -->_2 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_2 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 -->_1 U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)):2 -->_1 U11#(mark(X1),X2) -> c_1(U11#(X1,X2)):1 14:S:active#(s(X)) -> c_19(s#(active(X)),active#(X)) -->_1 s#(ok(X)) -> c_43(s#(X)):33 -->_1 s#(mark(X)) -> c_42(s#(X)):32 -->_2 active#(zeros()) -> c_20(cons#(0(),zeros())):41 -->_2 active#(length(nil())) -> c_18():40 -->_2 active#(isNatList(nil())) -> c_15():39 -->_2 active#(isNatIList(zeros())) -> c_13():38 -->_2 active#(isNat(0())) -> c_8():37 -->_2 active#(and(tt(),X)) -> c_6():36 -->_2 active#(s(X)) -> c_19(s#(active(X)),active#(X)):14 -->_2 active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)):13 -->_2 active#(length(X)) -> c_16(length#(active(X)),active#(X)):12 -->_2 active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)):11 -->_2 active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)) ,isNat#(V1) ,isNatIList#(V2)):10 -->_2 active#(isNatIList(V)) -> c_11(isNatList#(V)):9 -->_2 active#(isNat(s(V1))) -> c_10(isNat#(V1)):8 -->_2 active#(isNat(length(V1))) -> c_9(isNatList#(V1)):7 -->_2 active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)):6 -->_2 active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)):5 -->_2 active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)):4 -->_2 active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)):3 15:S:and#(mark(X1),X2) -> c_21(and#(X1,X2)) -->_1 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_1 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 16:S:and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) -->_1 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_1 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 17:S:cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)):18 -->_1 cons#(mark(X1),X2) -> c_23(cons#(X1,X2)):17 18:S:cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) -->_1 cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)):18 -->_1 cons#(mark(X1),X2) -> c_23(cons#(X1,X2)):17 19:S:isNat#(ok(X)) -> c_25(isNat#(X)) -->_1 isNat#(ok(X)) -> c_25(isNat#(X)):19 20:S:isNatIList#(ok(X)) -> c_26(isNatIList#(X)) -->_1 isNatIList#(ok(X)) -> c_26(isNatIList#(X)):20 21:S:isNatList#(ok(X)) -> c_27(isNatList#(X)) -->_1 isNatList#(ok(X)) -> c_27(isNatList#(X)):21 22:S:length#(mark(X)) -> c_28(length#(X)) -->_1 length#(ok(X)) -> c_29(length#(X)):23 -->_1 length#(mark(X)) -> c_28(length#(X)):22 23:S:length#(ok(X)) -> c_29(length#(X)) -->_1 length#(ok(X)) -> c_29(length#(X)):23 -->_1 length#(mark(X)) -> c_28(length#(X)):22 24:S:proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_3 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_3 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_3 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_3 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_3 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_3 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_3 proper#(zeros()) -> c_41():45 -->_2 proper#(zeros()) -> c_41():45 -->_3 proper#(tt()) -> c_40():44 -->_2 proper#(tt()) -> c_40():44 -->_3 proper#(nil()) -> c_38():43 -->_2 proper#(nil()) -> c_38():43 -->_3 proper#(0()) -> c_30():42 -->_2 proper#(0()) -> c_30():42 -->_3 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)):2 -->_1 U11#(mark(X1),X2) -> c_1(U11#(X1,X2)):1 25:S:proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_3 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_3 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_3 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_3 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_3 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_3 proper#(zeros()) -> c_41():45 -->_2 proper#(zeros()) -> c_41():45 -->_3 proper#(tt()) -> c_40():44 -->_2 proper#(tt()) -> c_40():44 -->_3 proper#(nil()) -> c_38():43 -->_2 proper#(nil()) -> c_38():43 -->_3 proper#(0()) -> c_30():42 -->_2 proper#(0()) -> c_30():42 -->_3 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_3 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)):16 -->_1 and#(mark(X1),X2) -> c_21(and#(X1,X2)):15 26:S:proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) -->_3 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_3 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_3 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_3 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_3 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_3 proper#(zeros()) -> c_41():45 -->_2 proper#(zeros()) -> c_41():45 -->_3 proper#(tt()) -> c_40():44 -->_2 proper#(tt()) -> c_40():44 -->_3 proper#(nil()) -> c_38():43 -->_2 proper#(nil()) -> c_38():43 -->_3 proper#(0()) -> c_30():42 -->_2 proper#(0()) -> c_30():42 -->_3 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_3 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_3 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)):18 -->_1 cons#(mark(X1),X2) -> c_23(cons#(X1,X2)):17 27:S:proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(zeros()) -> c_41():45 -->_2 proper#(tt()) -> c_40():44 -->_2 proper#(nil()) -> c_38():43 -->_2 proper#(0()) -> c_30():42 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 isNat#(ok(X)) -> c_25(isNat#(X)):19 28:S:proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(zeros()) -> c_41():45 -->_2 proper#(tt()) -> c_40():44 -->_2 proper#(nil()) -> c_38():43 -->_2 proper#(0()) -> c_30():42 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 isNatIList#(ok(X)) -> c_26(isNatIList#(X)):20 29:S:proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(zeros()) -> c_41():45 -->_2 proper#(tt()) -> c_40():44 -->_2 proper#(nil()) -> c_38():43 -->_2 proper#(0()) -> c_30():42 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 isNatList#(ok(X)) -> c_27(isNatList#(X)):21 30:S:proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(zeros()) -> c_41():45 -->_2 proper#(tt()) -> c_40():44 -->_2 proper#(nil()) -> c_38():43 -->_2 proper#(0()) -> c_30():42 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 -->_1 length#(ok(X)) -> c_29(length#(X)):23 -->_1 length#(mark(X)) -> c_28(length#(X)):22 31:S:proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) -->_1 s#(ok(X)) -> c_43(s#(X)):33 -->_1 s#(mark(X)) -> c_42(s#(X)):32 -->_2 proper#(zeros()) -> c_41():45 -->_2 proper#(tt()) -> c_40():44 -->_2 proper#(nil()) -> c_38():43 -->_2 proper#(0()) -> c_30():42 -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 32:S:s#(mark(X)) -> c_42(s#(X)) -->_1 s#(ok(X)) -> c_43(s#(X)):33 -->_1 s#(mark(X)) -> c_42(s#(X)):32 33:S:s#(ok(X)) -> c_43(s#(X)) -->_1 s#(ok(X)) -> c_43(s#(X)):33 -->_1 s#(mark(X)) -> c_42(s#(X)):32 34:S:top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) -->_1 top#(ok(X)) -> c_45(top#(active(X)),active#(X)):35 -->_2 proper#(zeros()) -> c_41():45 -->_2 proper#(tt()) -> c_40():44 -->_2 proper#(nil()) -> c_38():43 -->_2 proper#(0()) -> c_30():42 -->_1 top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)):34 -->_2 proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)):31 -->_2 proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)):30 -->_2 proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)):29 -->_2 proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)):28 -->_2 proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)):27 -->_2 proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):26 -->_2 proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):25 -->_2 proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)):24 35:S:top#(ok(X)) -> c_45(top#(active(X)),active#(X)) -->_2 active#(zeros()) -> c_20(cons#(0(),zeros())):41 -->_2 active#(length(nil())) -> c_18():40 -->_2 active#(isNatList(nil())) -> c_15():39 -->_2 active#(isNatIList(zeros())) -> c_13():38 -->_2 active#(isNat(0())) -> c_8():37 -->_2 active#(and(tt(),X)) -> c_6():36 -->_1 top#(ok(X)) -> c_45(top#(active(X)),active#(X)):35 -->_1 top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)):34 -->_2 active#(s(X)) -> c_19(s#(active(X)),active#(X)):14 -->_2 active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)):13 -->_2 active#(length(X)) -> c_16(length#(active(X)),active#(X)):12 -->_2 active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)):11 -->_2 active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)) ,isNat#(V1) ,isNatIList#(V2)):10 -->_2 active#(isNatIList(V)) -> c_11(isNatList#(V)):9 -->_2 active#(isNat(s(V1))) -> c_10(isNat#(V1)):8 -->_2 active#(isNat(length(V1))) -> c_9(isNatList#(V1)):7 -->_2 active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)):6 -->_2 active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)):5 -->_2 active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)):4 -->_2 active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)):3 36:W:active#(and(tt(),X)) -> c_6() 37:W:active#(isNat(0())) -> c_8() 38:W:active#(isNatIList(zeros())) -> c_13() 39:W:active#(isNatList(nil())) -> c_15() 40:W:active#(length(nil())) -> c_18() 41:W:active#(zeros()) -> c_20(cons#(0(),zeros())) 42:W:proper#(0()) -> c_30() 43:W:proper#(nil()) -> c_38() 44:W:proper#(tt()) -> c_40() 45:W:proper#(zeros()) -> c_41() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 42: proper#(0()) -> c_30() 43: proper#(nil()) -> c_38() 44: proper#(tt()) -> c_40() 45: proper#(zeros()) -> c_41() 36: active#(and(tt(),X)) -> c_6() 37: active#(isNat(0())) -> c_8() 38: active#(isNatIList(zeros())) -> c_13() 39: active#(isNatList(nil())) -> c_15() 40: active#(length(nil())) -> c_18() 41: active#(zeros()) -> c_20(cons#(0(),zeros())) * Step 5: Failure MAYBE + Considered Problem: - Strict DPs: U11#(mark(X1),X2) -> c_1(U11#(X1,X2)) U11#(ok(X1),ok(X2)) -> c_2(U11#(X1,X2)) active#(U11(X1,X2)) -> c_3(U11#(active(X1),X2),active#(X1)) active#(U11(tt(),L)) -> c_4(s#(length(L)),length#(L)) active#(and(X1,X2)) -> c_5(and#(active(X1),X2),active#(X1)) active#(cons(X1,X2)) -> c_7(cons#(active(X1),X2),active#(X1)) active#(isNat(length(V1))) -> c_9(isNatList#(V1)) active#(isNat(s(V1))) -> c_10(isNat#(V1)) active#(isNatIList(V)) -> c_11(isNatList#(V)) active#(isNatIList(cons(V1,V2))) -> c_12(and#(isNat(V1),isNatIList(V2)),isNat#(V1),isNatIList#(V2)) active#(isNatList(cons(V1,V2))) -> c_14(and#(isNat(V1),isNatList(V2)),isNat#(V1),isNatList#(V2)) active#(length(X)) -> c_16(length#(active(X)),active#(X)) active#(length(cons(N,L))) -> c_17(U11#(and(isNatList(L),isNat(N)),L) ,and#(isNatList(L),isNat(N)) ,isNatList#(L) ,isNat#(N)) active#(s(X)) -> c_19(s#(active(X)),active#(X)) and#(mark(X1),X2) -> c_21(and#(X1,X2)) and#(ok(X1),ok(X2)) -> c_22(and#(X1,X2)) cons#(mark(X1),X2) -> c_23(cons#(X1,X2)) cons#(ok(X1),ok(X2)) -> c_24(cons#(X1,X2)) isNat#(ok(X)) -> c_25(isNat#(X)) isNatIList#(ok(X)) -> c_26(isNatIList#(X)) isNatList#(ok(X)) -> c_27(isNatList#(X)) length#(mark(X)) -> c_28(length#(X)) length#(ok(X)) -> c_29(length#(X)) proper#(U11(X1,X2)) -> c_31(U11#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(and(X1,X2)) -> c_32(and#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(cons(X1,X2)) -> c_33(cons#(proper(X1),proper(X2)),proper#(X1),proper#(X2)) proper#(isNat(X)) -> c_34(isNat#(proper(X)),proper#(X)) proper#(isNatIList(X)) -> c_35(isNatIList#(proper(X)),proper#(X)) proper#(isNatList(X)) -> c_36(isNatList#(proper(X)),proper#(X)) proper#(length(X)) -> c_37(length#(proper(X)),proper#(X)) proper#(s(X)) -> c_39(s#(proper(X)),proper#(X)) s#(mark(X)) -> c_42(s#(X)) s#(ok(X)) -> c_43(s#(X)) top#(mark(X)) -> c_44(top#(proper(X)),proper#(X)) top#(ok(X)) -> c_45(top#(active(X)),active#(X)) - Weak TRS: U11(mark(X1),X2) -> mark(U11(X1,X2)) U11(ok(X1),ok(X2)) -> ok(U11(X1,X2)) active(U11(X1,X2)) -> U11(active(X1),X2) active(U11(tt(),L)) -> mark(s(length(L))) active(and(X1,X2)) -> and(active(X1),X2) active(and(tt(),X)) -> mark(X) active(cons(X1,X2)) -> cons(active(X1),X2) active(isNat(0())) -> mark(tt()) active(isNat(length(V1))) -> mark(isNatList(V1)) active(isNat(s(V1))) -> mark(isNat(V1)) active(isNatIList(V)) -> mark(isNatList(V)) active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2))) active(isNatIList(zeros())) -> mark(tt()) active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2))) active(isNatList(nil())) -> mark(tt()) active(length(X)) -> length(active(X)) active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L)) active(length(nil())) -> mark(0()) active(s(X)) -> s(active(X)) active(zeros()) -> mark(cons(0(),zeros())) and(mark(X1),X2) -> mark(and(X1,X2)) and(ok(X1),ok(X2)) -> ok(and(X1,X2)) cons(mark(X1),X2) -> mark(cons(X1,X2)) cons(ok(X1),ok(X2)) -> ok(cons(X1,X2)) isNat(ok(X)) -> ok(isNat(X)) isNatIList(ok(X)) -> ok(isNatIList(X)) isNatList(ok(X)) -> ok(isNatList(X)) length(mark(X)) -> mark(length(X)) length(ok(X)) -> ok(length(X)) proper(0()) -> ok(0()) proper(U11(X1,X2)) -> U11(proper(X1),proper(X2)) proper(and(X1,X2)) -> and(proper(X1),proper(X2)) proper(cons(X1,X2)) -> cons(proper(X1),proper(X2)) proper(isNat(X)) -> isNat(proper(X)) proper(isNatIList(X)) -> isNatIList(proper(X)) proper(isNatList(X)) -> isNatList(proper(X)) proper(length(X)) -> length(proper(X)) proper(nil()) -> ok(nil()) proper(s(X)) -> s(proper(X)) proper(tt()) -> ok(tt()) proper(zeros()) -> ok(zeros()) s(mark(X)) -> mark(s(X)) s(ok(X)) -> ok(s(X)) - Signature: {U11/2,active/1,and/2,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,proper/1,s/1,top/1,U11#/2,active#/1 ,and#/2,cons#/2,isNat#/1,isNatIList#/1,isNatList#/1,length#/1,proper#/1,s#/1,top#/1} / {0/0,mark/1,nil/0 ,ok/1,tt/0,zeros/0,c_1/1,c_2/1,c_3/2,c_4/2,c_5/2,c_6/0,c_7/2,c_8/0,c_9/1,c_10/1,c_11/1,c_12/3,c_13/0,c_14/3 ,c_15/0,c_16/2,c_17/4,c_18/0,c_19/2,c_20/1,c_21/1,c_22/1,c_23/1,c_24/1,c_25/1,c_26/1,c_27/1,c_28/1,c_29/1 ,c_30/0,c_31/3,c_32/3,c_33/3,c_34/2,c_35/2,c_36/2,c_37/2,c_38/0,c_39/2,c_40/0,c_41/0,c_42/1,c_43/1,c_44/2 ,c_45/2} - Obligation: innermost runtime complexity wrt. defined symbols {U11#,active#,and#,cons#,isNat#,isNatIList#,isNatList# ,length#,proper#,s#,top#} and constructors {0,mark,nil,ok,tt,zeros} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE