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