MAYBE

Problem:
 active(zeros()) -> mark(cons(0(),zeros()))
 active(U11(tt(),L)) -> mark(s(length(L)))
 active(and(tt(),X)) -> mark(X)
 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(zeros())) -> mark(tt())
 active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
 active(isNatList(nil())) -> mark(tt())
 active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
 active(length(nil())) -> mark(0())
 active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
 active(cons(X1,X2)) -> cons(active(X1),X2)
 active(U11(X1,X2)) -> U11(active(X1),X2)
 active(s(X)) -> s(active(X))
 active(length(X)) -> length(active(X))
 active(and(X1,X2)) -> and(active(X1),X2)
 cons(mark(X1),X2) -> mark(cons(X1,X2))
 U11(mark(X1),X2) -> mark(U11(X1,X2))
 s(mark(X)) -> mark(s(X))
 length(mark(X)) -> mark(length(X))
 and(mark(X1),X2) -> mark(and(X1,X2))
 proper(zeros()) -> ok(zeros())
 proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
 proper(0()) -> ok(0())
 proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
 proper(tt()) -> ok(tt())
 proper(s(X)) -> s(proper(X))
 proper(length(X)) -> length(proper(X))
 proper(and(X1,X2)) -> and(proper(X1),proper(X2))
 proper(isNat(X)) -> isNat(proper(X))
 proper(isNatList(X)) -> isNatList(proper(X))
 proper(isNatIList(X)) -> isNatIList(proper(X))
 proper(nil()) -> ok(nil())
 cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
 U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
 s(ok(X)) -> ok(s(X))
 length(ok(X)) -> ok(length(X))
 and(ok(X1),ok(X2)) -> ok(and(X1,X2))
 isNat(ok(X)) -> ok(isNat(X))
 isNatList(ok(X)) -> ok(isNatList(X))
 isNatIList(ok(X)) -> ok(isNatIList(X))
 top(mark(X)) -> top(proper(X))
 top(ok(X)) -> top(active(X))

Proof:
 DP Processor:
  DPs:
   active#(zeros()) -> cons#(0(),zeros())
   active#(U11(tt(),L)) -> length#(L)
   active#(U11(tt(),L)) -> s#(length(L))
   active#(isNat(length(V1))) -> isNatList#(V1)
   active#(isNat(s(V1))) -> isNat#(V1)
   active#(isNatIList(V)) -> isNatList#(V)
   active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
   active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
   active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
   active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
   active#(isNatList(cons(V1,V2))) -> isNat#(V1)
   active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
   active#(length(cons(N,L))) -> isNat#(N)
   active#(length(cons(N,L))) -> isNatList#(L)
   active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
   active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
   active#(cons(X1,X2)) -> active#(X1)
   active#(cons(X1,X2)) -> cons#(active(X1),X2)
   active#(U11(X1,X2)) -> active#(X1)
   active#(U11(X1,X2)) -> U11#(active(X1),X2)
   active#(s(X)) -> active#(X)
   active#(s(X)) -> s#(active(X))
   active#(length(X)) -> active#(X)
   active#(length(X)) -> length#(active(X))
   active#(and(X1,X2)) -> active#(X1)
   active#(and(X1,X2)) -> and#(active(X1),X2)
   cons#(mark(X1),X2) -> cons#(X1,X2)
   U11#(mark(X1),X2) -> U11#(X1,X2)
   s#(mark(X)) -> s#(X)
   length#(mark(X)) -> length#(X)
   and#(mark(X1),X2) -> and#(X1,X2)
   proper#(cons(X1,X2)) -> proper#(X2)
   proper#(cons(X1,X2)) -> proper#(X1)
   proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
   proper#(U11(X1,X2)) -> proper#(X2)
   proper#(U11(X1,X2)) -> proper#(X1)
   proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
   proper#(s(X)) -> proper#(X)
   proper#(s(X)) -> s#(proper(X))
   proper#(length(X)) -> proper#(X)
   proper#(length(X)) -> length#(proper(X))
   proper#(and(X1,X2)) -> proper#(X2)
   proper#(and(X1,X2)) -> proper#(X1)
   proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
   proper#(isNat(X)) -> proper#(X)
   proper#(isNat(X)) -> isNat#(proper(X))
   proper#(isNatList(X)) -> proper#(X)
   proper#(isNatList(X)) -> isNatList#(proper(X))
   proper#(isNatIList(X)) -> proper#(X)
   proper#(isNatIList(X)) -> isNatIList#(proper(X))
   cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
   U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
   s#(ok(X)) -> s#(X)
   length#(ok(X)) -> length#(X)
   and#(ok(X1),ok(X2)) -> and#(X1,X2)
   isNat#(ok(X)) -> isNat#(X)
   isNatList#(ok(X)) -> isNatList#(X)
   isNatIList#(ok(X)) -> isNatIList#(X)
   top#(mark(X)) -> proper#(X)
   top#(mark(X)) -> top#(proper(X))
   top#(ok(X)) -> active#(X)
   top#(ok(X)) -> top#(active(X))
  TRS:
   active(zeros()) -> mark(cons(0(),zeros()))
   active(U11(tt(),L)) -> mark(s(length(L)))
   active(and(tt(),X)) -> mark(X)
   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(zeros())) -> mark(tt())
   active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
   active(isNatList(nil())) -> mark(tt())
   active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
   active(length(nil())) -> mark(0())
   active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
   active(cons(X1,X2)) -> cons(active(X1),X2)
   active(U11(X1,X2)) -> U11(active(X1),X2)
   active(s(X)) -> s(active(X))
   active(length(X)) -> length(active(X))
   active(and(X1,X2)) -> and(active(X1),X2)
   cons(mark(X1),X2) -> mark(cons(X1,X2))
   U11(mark(X1),X2) -> mark(U11(X1,X2))
   s(mark(X)) -> mark(s(X))
   length(mark(X)) -> mark(length(X))
   and(mark(X1),X2) -> mark(and(X1,X2))
   proper(zeros()) -> ok(zeros())
   proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
   proper(0()) -> ok(0())
   proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
   proper(tt()) -> ok(tt())
   proper(s(X)) -> s(proper(X))
   proper(length(X)) -> length(proper(X))
   proper(and(X1,X2)) -> and(proper(X1),proper(X2))
   proper(isNat(X)) -> isNat(proper(X))
   proper(isNatList(X)) -> isNatList(proper(X))
   proper(isNatIList(X)) -> isNatIList(proper(X))
   proper(nil()) -> ok(nil())
   cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
   U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
   s(ok(X)) -> ok(s(X))
   length(ok(X)) -> ok(length(X))
   and(ok(X1),ok(X2)) -> ok(and(X1,X2))
   isNat(ok(X)) -> ok(isNat(X))
   isNatList(ok(X)) -> ok(isNatList(X))
   isNatIList(ok(X)) -> ok(isNatIList(X))
   top(mark(X)) -> top(proper(X))
   top(ok(X)) -> top(active(X))
  TDG Processor:
   DPs:
    active#(zeros()) -> cons#(0(),zeros())
    active#(U11(tt(),L)) -> length#(L)
    active#(U11(tt(),L)) -> s#(length(L))
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(isNatIList(V)) -> isNatList#(V)
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(length(cons(N,L))) -> isNat#(N)
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(U11(X1,X2)) -> active#(X1)
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    active#(s(X)) -> active#(X)
    active#(s(X)) -> s#(active(X))
    active#(length(X)) -> active#(X)
    active#(length(X)) -> length#(active(X))
    active#(and(X1,X2)) -> active#(X1)
    active#(and(X1,X2)) -> and#(active(X1),X2)
    cons#(mark(X1),X2) -> cons#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2)
    s#(mark(X)) -> s#(X)
    length#(mark(X)) -> length#(X)
    and#(mark(X1),X2) -> and#(X1,X2)
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> s#(proper(X))
    proper#(length(X)) -> proper#(X)
    proper#(length(X)) -> length#(proper(X))
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(isNat(X)) -> proper#(X)
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(isNatList(X)) -> proper#(X)
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(isNatIList(X)) -> proper#(X)
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
    s#(ok(X)) -> s#(X)
    length#(ok(X)) -> length#(X)
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    isNat#(ok(X)) -> isNat#(X)
    isNatList#(ok(X)) -> isNatList#(X)
    isNatIList#(ok(X)) -> isNatIList#(X)
    top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X))
   TRS:
    active(zeros()) -> mark(cons(0(),zeros()))
    active(U11(tt(),L)) -> mark(s(length(L)))
    active(and(tt(),X)) -> mark(X)
    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(zeros())) -> mark(tt())
    active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
    active(isNatList(nil())) -> mark(tt())
    active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
    active(length(nil())) -> mark(0())
    active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
    active(cons(X1,X2)) -> cons(active(X1),X2)
    active(U11(X1,X2)) -> U11(active(X1),X2)
    active(s(X)) -> s(active(X))
    active(length(X)) -> length(active(X))
    active(and(X1,X2)) -> and(active(X1),X2)
    cons(mark(X1),X2) -> mark(cons(X1,X2))
    U11(mark(X1),X2) -> mark(U11(X1,X2))
    s(mark(X)) -> mark(s(X))
    length(mark(X)) -> mark(length(X))
    and(mark(X1),X2) -> mark(and(X1,X2))
    proper(zeros()) -> ok(zeros())
    proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
    proper(0()) -> ok(0())
    proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
    proper(tt()) -> ok(tt())
    proper(s(X)) -> s(proper(X))
    proper(length(X)) -> length(proper(X))
    proper(and(X1,X2)) -> and(proper(X1),proper(X2))
    proper(isNat(X)) -> isNat(proper(X))
    proper(isNatList(X)) -> isNatList(proper(X))
    proper(isNatIList(X)) -> isNatIList(proper(X))
    proper(nil()) -> ok(nil())
    cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
    U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
    s(ok(X)) -> ok(s(X))
    length(ok(X)) -> ok(length(X))
    and(ok(X1),ok(X2)) -> ok(and(X1,X2))
    isNat(ok(X)) -> ok(isNat(X))
    isNatList(ok(X)) -> ok(isNatList(X))
    isNatIList(ok(X)) -> ok(isNatIList(X))
    top(mark(X)) -> top(proper(X))
    top(ok(X)) -> top(active(X))
   graph:
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
    top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
    top#(ok(X)) -> top#(active(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
    top#(ok(X)) -> active#(X) ->
    active#(and(X1,X2)) -> and#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(and(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) -> active#(length(X)) -> length#(active(X))
    top#(ok(X)) -> active#(X) -> active#(length(X)) -> active#(X)
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    top#(ok(X)) -> active#(X) ->
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(U11(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
    top#(ok(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    top#(ok(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    top#(ok(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    top#(ok(X)) -> active#(X) -> active#(length(cons(N,L))) -> isNat#(N)
    top#(ok(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    top#(ok(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    top#(ok(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    top#(ok(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    top#(ok(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    top#(ok(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    top#(ok(X)) -> active#(X) -> active#(isNatIList(V)) -> isNatList#(V)
    top#(ok(X)) -> active#(X) -> active#(isNat(s(V1))) -> isNat#(V1)
    top#(ok(X)) -> active#(X) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    top#(ok(X)) -> active#(X) -> active#(U11(tt(),L)) -> s#(length(L))
    top#(ok(X)) -> active#(X) -> active#(U11(tt(),L)) -> length#(L)
    top#(ok(X)) -> active#(X) ->
    active#(zeros()) -> cons#(0(),zeros())
    top#(mark(X)) -> top#(proper(X)) ->
    top#(ok(X)) -> top#(active(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
    top#(mark(X)) -> top#(proper(X)) ->
    top#(mark(X)) -> top#(proper(X))
    top#(mark(X)) -> top#(proper(X)) -> top#(mark(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(isNatIList(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(isNatList(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(isNat(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    top#(mark(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X2)
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
    top#(mark(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(length(X)) -> proper#(X)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(s(X)) -> proper#(X)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(isNatIList(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(isNatIList(X)) -> isNatIList#(proper(X)) ->
    isNatIList#(ok(X)) -> isNatIList#(X)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(length(X)) -> proper#(X)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(s(X)) -> proper#(X)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(isNatList(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(isNatList(X)) -> isNatList#(proper(X)) ->
    isNatList#(ok(X)) -> isNatList#(X)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(length(X)) -> proper#(X)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(isNat(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(isNat(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(isNat(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(isNat(X)) -> isNat#(proper(X)) ->
    isNat#(ok(X)) -> isNat#(X)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(and(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(isNatIList(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(isNatList(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(isNat(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
    proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(s(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
    proper#(s(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
    proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(length(X)) -> proper#(X) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(length(X)) -> proper#(X) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(length(X)) -> proper#(X) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(length(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(length(X)) -> proper#(X) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(length(X)) -> proper#(X) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(length(X)) -> proper#(X) ->
    proper#(length(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(length(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
    proper#(length(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(length(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(length(X)) -> proper#(X) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(length(X)) -> proper#(X) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(length(X)) -> length#(proper(X)) ->
    length#(ok(X)) -> length#(X)
    proper#(length(X)) -> length#(proper(X)) ->
    length#(mark(X)) -> length#(X)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(U11(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2)) ->
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2)) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(length(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X2) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(isNatIList(X)) -> isNatIList#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(isNatIList(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(isNatList(X)) -> isNatList#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(isNatList(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(isNat(X)) -> isNat#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(isNat(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(and(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> length#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(length(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> s#(proper(X))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(s(X)) -> proper#(X)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(U11(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X1)
    proper#(cons(X1,X2)) -> proper#(X1) ->
    proper#(cons(X1,X2)) -> proper#(X2)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2) ->
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
    U11#(mark(X1),X2) -> U11#(X1,X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    and#(ok(X1),ok(X2)) -> and#(X1,X2) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    and#(ok(X1),ok(X2)) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    and#(mark(X1),X2) -> and#(X1,X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    isNatIList#(ok(X)) -> isNatIList#(X) ->
    isNatIList#(ok(X)) -> isNatIList#(X)
    isNat#(ok(X)) -> isNat#(X) -> isNat#(ok(X)) -> isNat#(X)
    isNatList#(ok(X)) -> isNatList#(X) -> isNatList#(ok(X)) -> isNatList#(X)
    s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
    s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
    length#(ok(X)) -> length#(X) -> length#(ok(X)) -> length#(X)
    length#(ok(X)) -> length#(X) -> length#(mark(X)) -> length#(X)
    length#(mark(X)) -> length#(X) -> length#(ok(X)) -> length#(X)
    length#(mark(X)) -> length#(X) ->
    length#(mark(X)) -> length#(X)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    cons#(mark(X1),X2) -> cons#(X1,X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) ->
    isNatIList#(ok(X)) -> isNatIList#(X)
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1) ->
    isNat#(ok(X)) -> isNat#(X)
    active#(isNatIList(V)) -> isNatList#(V) ->
    isNatList#(ok(X)) -> isNatList#(X)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(isNatList(cons(V1,V2))) -> isNat#(V1) ->
    isNat#(ok(X)) -> isNat#(X)
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2) ->
    isNatList#(ok(X)) -> isNatList#(X)
    active#(isNat(s(V1))) -> isNat#(V1) ->
    isNat#(ok(X)) -> isNat#(X)
    active#(isNat(length(V1))) -> isNatList#(V1) ->
    isNatList#(ok(X)) -> isNatList#(X)
    active#(and(X1,X2)) -> and#(active(X1),X2) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    active#(and(X1,X2)) -> and#(active(X1),X2) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(and(X1,X2)) -> and#(active(X1),X2)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(and(X1,X2)) -> active#(X1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> length#(active(X))
    active#(and(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> active#(X)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(and(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(U11(X1,X2)) -> active#(X1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(and(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> isNat#(N)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNatIList(V)) -> isNatList#(V)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(U11(tt(),L)) -> s#(length(L))
    active#(and(X1,X2)) -> active#(X1) ->
    active#(U11(tt(),L)) -> length#(L)
    active#(and(X1,X2)) -> active#(X1) ->
    active#(zeros()) -> cons#(0(),zeros())
    active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
    active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
    active#(s(X)) -> active#(X) ->
    active#(and(X1,X2)) -> and#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(and(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(length(X)) -> length#(active(X))
    active#(s(X)) -> active#(X) -> active#(length(X)) -> active#(X)
    active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
    active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(s(X)) -> active#(X) ->
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(U11(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
    active#(s(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(s(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(s(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(s(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> isNat#(N)
    active#(s(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(s(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(s(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(s(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(s(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(s(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(s(X)) -> active#(X) ->
    active#(isNatIList(V)) -> isNatList#(V)
    active#(s(X)) -> active#(X) -> active#(isNat(s(V1))) -> isNat#(V1)
    active#(s(X)) -> active#(X) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(s(X)) -> active#(X) -> active#(U11(tt(),L)) -> s#(length(L))
    active#(s(X)) -> active#(X) -> active#(U11(tt(),L)) -> length#(L)
    active#(s(X)) -> active#(X) ->
    active#(zeros()) -> cons#(0(),zeros())
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
    and#(ok(X1),ok(X2)) -> and#(X1,X2)
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
    and#(mark(X1),X2) -> and#(X1,X2)
    active#(length(cons(N,L))) -> isNat#(N) ->
    isNat#(ok(X)) -> isNat#(X)
    active#(length(cons(N,L))) -> isNatList#(L) ->
    isNatList#(ok(X)) -> isNatList#(X)
    active#(length(X)) -> length#(active(X)) ->
    length#(ok(X)) -> length#(X)
    active#(length(X)) -> length#(active(X)) ->
    length#(mark(X)) -> length#(X)
    active#(length(X)) -> active#(X) ->
    active#(and(X1,X2)) -> and#(active(X1),X2)
    active#(length(X)) -> active#(X) ->
    active#(and(X1,X2)) -> active#(X1)
    active#(length(X)) -> active#(X) ->
    active#(length(X)) -> length#(active(X))
    active#(length(X)) -> active#(X) ->
    active#(length(X)) -> active#(X)
    active#(length(X)) -> active#(X) ->
    active#(s(X)) -> s#(active(X))
    active#(length(X)) -> active#(X) -> active#(s(X)) -> active#(X)
    active#(length(X)) -> active#(X) ->
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    active#(length(X)) -> active#(X) ->
    active#(U11(X1,X2)) -> active#(X1)
    active#(length(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(length(X)) -> active#(X) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(length(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(length(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(length(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(length(X)) -> active#(X) ->
    active#(length(cons(N,L))) -> isNat#(N)
    active#(length(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(length(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(length(X)) -> active#(X) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(length(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(length(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(length(X)) -> active#(X) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(length(X)) -> active#(X) ->
    active#(isNatIList(V)) -> isNatList#(V)
    active#(length(X)) -> active#(X) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(length(X)) -> active#(X) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(length(X)) -> active#(X) ->
    active#(U11(tt(),L)) -> s#(length(L))
    active#(length(X)) -> active#(X) ->
    active#(U11(tt(),L)) -> length#(L)
    active#(length(X)) -> active#(X) ->
    active#(zeros()) -> cons#(0(),zeros())
    active#(U11(tt(),L)) -> s#(length(L)) ->
    s#(ok(X)) -> s#(X)
    active#(U11(tt(),L)) -> s#(length(L)) -> s#(mark(X)) -> s#(X)
    active#(U11(tt(),L)) -> length#(L) ->
    length#(ok(X)) -> length#(X)
    active#(U11(tt(),L)) -> length#(L) ->
    length#(mark(X)) -> length#(X)
    active#(U11(X1,X2)) -> U11#(active(X1),X2) ->
    U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
    active#(U11(X1,X2)) -> U11#(active(X1),X2) ->
    U11#(mark(X1),X2) -> U11#(X1,X2)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(and(X1,X2)) -> and#(active(X1),X2)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(and(X1,X2)) -> active#(X1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> length#(active(X))
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> active#(X)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(U11(X1,X2)) -> active#(X1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> isNat#(N)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNatIList(V)) -> isNatList#(V)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(U11(tt(),L)) -> s#(length(L))
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(U11(tt(),L)) -> length#(L)
    active#(U11(X1,X2)) -> active#(X1) ->
    active#(zeros()) -> cons#(0(),zeros())
    active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
    cons#(mark(X1),X2) -> cons#(X1,X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(and(X1,X2)) -> and#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(and(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> length#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(length(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> s#(active(X))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(s(X)) -> active#(X)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(U11(X1,X2)) -> U11#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(U11(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> cons#(active(X1),X2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(cons(X1,X2)) -> active#(X1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> isNatList#(L)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(length(cons(N,L))) -> isNat#(N)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> isNat#(V1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNatIList(V)) -> isNatList#(V)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNat(s(V1))) -> isNat#(V1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(isNat(length(V1))) -> isNatList#(V1)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(U11(tt(),L)) -> s#(length(L))
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(U11(tt(),L)) -> length#(L)
    active#(cons(X1,X2)) -> active#(X1) ->
    active#(zeros()) -> cons#(0(),zeros())
    active#(zeros()) -> cons#(0(),zeros()) ->
    cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
    active#(zeros()) -> cons#(0(),zeros()) -> cons#(mark(X1),X2) -> cons#(X1,X2)
   EDG Processor:
    DPs:
     active#(zeros()) -> cons#(0(),zeros())
     active#(U11(tt(),L)) -> length#(L)
     active#(U11(tt(),L)) -> s#(length(L))
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(isNatIList(V)) -> isNatList#(V)
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(length(cons(N,L))) -> isNat#(N)
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(cons(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(U11(X1,X2)) -> active#(X1)
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     active#(s(X)) -> active#(X)
     active#(s(X)) -> s#(active(X))
     active#(length(X)) -> active#(X)
     active#(length(X)) -> length#(active(X))
     active#(and(X1,X2)) -> active#(X1)
     active#(and(X1,X2)) -> and#(active(X1),X2)
     cons#(mark(X1),X2) -> cons#(X1,X2)
     U11#(mark(X1),X2) -> U11#(X1,X2)
     s#(mark(X)) -> s#(X)
     length#(mark(X)) -> length#(X)
     and#(mark(X1),X2) -> and#(X1,X2)
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(s(X)) -> proper#(X)
     proper#(s(X)) -> s#(proper(X))
     proper#(length(X)) -> proper#(X)
     proper#(length(X)) -> length#(proper(X))
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(isNat(X)) -> proper#(X)
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(isNatList(X)) -> proper#(X)
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(isNatIList(X)) -> proper#(X)
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
     s#(ok(X)) -> s#(X)
     length#(ok(X)) -> length#(X)
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     isNat#(ok(X)) -> isNat#(X)
     isNatList#(ok(X)) -> isNatList#(X)
     isNatIList#(ok(X)) -> isNatIList#(X)
     top#(mark(X)) -> proper#(X)
     top#(mark(X)) -> top#(proper(X))
     top#(ok(X)) -> active#(X)
     top#(ok(X)) -> top#(active(X))
    TRS:
     active(zeros()) -> mark(cons(0(),zeros()))
     active(U11(tt(),L)) -> mark(s(length(L)))
     active(and(tt(),X)) -> mark(X)
     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(zeros())) -> mark(tt())
     active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
     active(isNatList(nil())) -> mark(tt())
     active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
     active(length(nil())) -> mark(0())
     active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
     active(cons(X1,X2)) -> cons(active(X1),X2)
     active(U11(X1,X2)) -> U11(active(X1),X2)
     active(s(X)) -> s(active(X))
     active(length(X)) -> length(active(X))
     active(and(X1,X2)) -> and(active(X1),X2)
     cons(mark(X1),X2) -> mark(cons(X1,X2))
     U11(mark(X1),X2) -> mark(U11(X1,X2))
     s(mark(X)) -> mark(s(X))
     length(mark(X)) -> mark(length(X))
     and(mark(X1),X2) -> mark(and(X1,X2))
     proper(zeros()) -> ok(zeros())
     proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
     proper(0()) -> ok(0())
     proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
     proper(tt()) -> ok(tt())
     proper(s(X)) -> s(proper(X))
     proper(length(X)) -> length(proper(X))
     proper(and(X1,X2)) -> and(proper(X1),proper(X2))
     proper(isNat(X)) -> isNat(proper(X))
     proper(isNatList(X)) -> isNatList(proper(X))
     proper(isNatIList(X)) -> isNatIList(proper(X))
     proper(nil()) -> ok(nil())
     cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
     U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
     s(ok(X)) -> ok(s(X))
     length(ok(X)) -> ok(length(X))
     and(ok(X1),ok(X2)) -> ok(and(X1,X2))
     isNat(ok(X)) -> ok(isNat(X))
     isNatList(ok(X)) -> ok(isNatList(X))
     isNatIList(ok(X)) -> ok(isNatIList(X))
     top(mark(X)) -> top(proper(X))
     top(ok(X)) -> top(active(X))
    graph:
     top#(ok(X)) -> top#(active(X)) -> top#(mark(X)) -> proper#(X)
     top#(ok(X)) -> top#(active(X)) ->
     top#(mark(X)) -> top#(proper(X))
     top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> active#(X)
     top#(ok(X)) -> top#(active(X)) -> top#(ok(X)) -> top#(active(X))
     top#(ok(X)) -> active#(X) -> active#(zeros()) -> cons#(0(),zeros())
     top#(ok(X)) -> active#(X) -> active#(U11(tt(),L)) -> length#(L)
     top#(ok(X)) -> active#(X) -> active#(U11(tt(),L)) -> s#(length(L))
     top#(ok(X)) -> active#(X) ->
     active#(isNat(length(V1))) -> isNatList#(V1)
     top#(ok(X)) -> active#(X) -> active#(isNat(s(V1))) -> isNat#(V1)
     top#(ok(X)) -> active#(X) -> active#(isNatIList(V)) -> isNatList#(V)
     top#(ok(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     top#(ok(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     top#(ok(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     top#(ok(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     top#(ok(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     top#(ok(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     top#(ok(X)) -> active#(X) -> active#(length(cons(N,L))) -> isNat#(N)
     top#(ok(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> isNatList#(L)
     top#(ok(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     top#(ok(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     top#(ok(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
     top#(ok(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     top#(ok(X)) -> active#(X) -> active#(U11(X1,X2)) -> active#(X1)
     top#(ok(X)) -> active#(X) ->
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     top#(ok(X)) -> active#(X) -> active#(s(X)) -> active#(X)
     top#(ok(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
     top#(ok(X)) -> active#(X) -> active#(length(X)) -> active#(X)
     top#(ok(X)) -> active#(X) -> active#(length(X)) -> length#(active(X))
     top#(ok(X)) -> active#(X) -> active#(and(X1,X2)) -> active#(X1)
     top#(ok(X)) -> active#(X) ->
     active#(and(X1,X2)) -> and#(active(X1),X2)
     top#(mark(X)) -> top#(proper(X)) ->
     top#(mark(X)) -> proper#(X)
     top#(mark(X)) -> top#(proper(X)) ->
     top#(mark(X)) -> top#(proper(X))
     top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> active#(X)
     top#(mark(X)) -> top#(proper(X)) -> top#(ok(X)) -> top#(active(X))
     top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
     top#(mark(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
     top#(mark(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     top#(mark(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X2)
     top#(mark(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X1)
     top#(mark(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
     top#(mark(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) ->
     proper#(length(X)) -> length#(proper(X))
     top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X2)
     top#(mark(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X1)
     top#(mark(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     top#(mark(X)) -> proper#(X) -> proper#(isNat(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     top#(mark(X)) -> proper#(X) -> proper#(isNatList(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     top#(mark(X)) -> proper#(X) -> proper#(isNatIList(X)) -> proper#(X)
     top#(mark(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(s(X)) -> proper#(X)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(length(X)) -> proper#(X)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(isNatIList(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(isNatIList(X)) -> isNatIList#(proper(X)) ->
     isNatIList#(ok(X)) -> isNatIList#(X)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(s(X)) -> proper#(X)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(length(X)) -> proper#(X)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(isNatList(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(isNatList(X)) -> isNatList#(proper(X)) ->
     isNatList#(ok(X)) -> isNatList#(X)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(isNat(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(isNat(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(isNat(X)) -> proper#(X) ->
     proper#(length(X)) -> proper#(X)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(isNat(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(isNat(X)) -> proper#(X) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(isNat(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(isNat(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(isNat(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(isNat(X)) -> isNat#(proper(X)) ->
     isNat#(ok(X)) -> isNat#(X)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(s(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(length(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X2) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(s(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(length(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(and(X1,X2)) -> proper#(X1) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2)) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X2)
     proper#(s(X)) -> proper#(X) -> proper#(cons(X1,X2)) -> proper#(X1)
     proper#(s(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(s(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X2)
     proper#(s(X)) -> proper#(X) -> proper#(U11(X1,X2)) -> proper#(X1)
     proper#(s(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X) -> proper#(s(X)) -> s#(proper(X))
     proper#(s(X)) -> proper#(X) -> proper#(length(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X2)
     proper#(s(X)) -> proper#(X) -> proper#(and(X1,X2)) -> proper#(X1)
     proper#(s(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(s(X)) -> proper#(X) -> proper#(isNat(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(s(X)) -> proper#(X) -> proper#(isNatList(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(s(X)) -> proper#(X) -> proper#(isNatIList(X)) -> proper#(X)
     proper#(s(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(s(X)) -> s#(proper(X)) -> s#(mark(X)) -> s#(X)
     proper#(s(X)) -> s#(proper(X)) -> s#(ok(X)) -> s#(X)
     proper#(length(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(length(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(length(X)) -> proper#(X) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(length(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(length(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(length(X)) -> proper#(X) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(length(X)) -> proper#(X) ->
     proper#(s(X)) -> proper#(X)
     proper#(length(X)) -> proper#(X) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(length(X)) -> proper#(X) ->
     proper#(length(X)) -> proper#(X)
     proper#(length(X)) -> proper#(X) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(length(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(length(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(length(X)) -> proper#(X) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(length(X)) -> proper#(X) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(length(X)) -> proper#(X) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(length(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(length(X)) -> proper#(X) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(length(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(length(X)) -> proper#(X) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(length(X)) -> length#(proper(X)) ->
     length#(mark(X)) -> length#(X)
     proper#(length(X)) -> length#(proper(X)) ->
     length#(ok(X)) -> length#(X)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(s(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(length(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X2) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(s(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(length(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(U11(X1,X2)) -> proper#(X1) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2)) ->
     U11#(mark(X1),X2) -> U11#(X1,X2)
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2)) ->
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(s(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(length(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X2) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(U11(X1,X2)) -> U11#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(s(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(s(X)) -> s#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(length(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(length(X)) -> length#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> proper#(X2)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> proper#(X1)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(and(X1,X2)) -> and#(proper(X1),proper(X2))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(isNat(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(isNat(X)) -> isNat#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(isNatList(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(isNatList(X)) -> isNatList#(proper(X))
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(isNatIList(X)) -> proper#(X)
     proper#(cons(X1,X2)) -> proper#(X1) ->
     proper#(isNatIList(X)) -> isNatIList#(proper(X))
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     proper#(cons(X1,X2)) -> cons#(proper(X1),proper(X2)) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2) ->
     U11#(mark(X1),X2) -> U11#(X1,X2)
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2) ->
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
     U11#(mark(X1),X2) -> U11#(X1,X2) ->
     U11#(mark(X1),X2) -> U11#(X1,X2)
     U11#(mark(X1),X2) -> U11#(X1,X2) ->
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
     and#(ok(X1),ok(X2)) -> and#(X1,X2) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     and#(ok(X1),ok(X2)) -> and#(X1,X2) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     and#(mark(X1),X2) -> and#(X1,X2) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     and#(mark(X1),X2) -> and#(X1,X2) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     isNatIList#(ok(X)) -> isNatIList#(X) ->
     isNatIList#(ok(X)) -> isNatIList#(X)
     isNat#(ok(X)) -> isNat#(X) -> isNat#(ok(X)) -> isNat#(X)
     isNatList#(ok(X)) -> isNatList#(X) -> isNatList#(ok(X)) -> isNatList#(X)
     s#(ok(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
     s#(ok(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
     s#(mark(X)) -> s#(X) -> s#(mark(X)) -> s#(X)
     s#(mark(X)) -> s#(X) -> s#(ok(X)) -> s#(X)
     length#(ok(X)) -> length#(X) -> length#(mark(X)) -> length#(X)
     length#(ok(X)) -> length#(X) -> length#(ok(X)) -> length#(X)
     length#(mark(X)) -> length#(X) -> length#(mark(X)) -> length#(X)
     length#(mark(X)) -> length#(X) ->
     length#(ok(X)) -> length#(X)
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     cons#(mark(X1),X2) -> cons#(X1,X2) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2)) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2) ->
     isNatIList#(ok(X)) -> isNatIList#(X)
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1) ->
     isNat#(ok(X)) -> isNat#(X)
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2)) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     active#(isNatList(cons(V1,V2))) -> isNat#(V1) ->
     isNat#(ok(X)) -> isNat#(X)
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2) ->
     isNatList#(ok(X)) -> isNatList#(X)
     active#(and(X1,X2)) -> and#(active(X1),X2) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     active#(and(X1,X2)) -> and#(active(X1),X2) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(and(X1,X2)) -> active#(X1) ->
     active#(U11(tt(),L)) -> length#(L)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(U11(tt(),L)) -> s#(length(L))
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatIList(V)) -> isNatList#(V)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(and(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> isNat#(N)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(and(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> active#(X1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(U11(X1,X2)) -> active#(X1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(s(X)) -> active#(X)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(s(X)) -> s#(active(X))
     active#(and(X1,X2)) -> active#(X1) ->
     active#(length(X)) -> active#(X)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(length(X)) -> length#(active(X))
     active#(and(X1,X2)) -> active#(X1) ->
     active#(and(X1,X2)) -> active#(X1)
     active#(and(X1,X2)) -> active#(X1) ->
     active#(and(X1,X2)) -> and#(active(X1),X2)
     active#(s(X)) -> s#(active(X)) -> s#(mark(X)) -> s#(X)
     active#(s(X)) -> s#(active(X)) -> s#(ok(X)) -> s#(X)
     active#(s(X)) -> active#(X) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(s(X)) -> active#(X) -> active#(U11(tt(),L)) -> length#(L)
     active#(s(X)) -> active#(X) ->
     active#(U11(tt(),L)) -> s#(length(L))
     active#(s(X)) -> active#(X) ->
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(s(X)) -> active#(X) -> active#(isNat(s(V1))) -> isNat#(V1)
     active#(s(X)) -> active#(X) ->
     active#(isNatIList(V)) -> isNatList#(V)
     active#(s(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(s(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(s(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(s(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(s(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(s(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(s(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> isNat#(N)
     active#(s(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(s(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(s(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(s(X)) -> active#(X) -> active#(cons(X1,X2)) -> active#(X1)
     active#(s(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(s(X)) -> active#(X) -> active#(U11(X1,X2)) -> active#(X1)
     active#(s(X)) -> active#(X) ->
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     active#(s(X)) -> active#(X) -> active#(s(X)) -> active#(X)
     active#(s(X)) -> active#(X) -> active#(s(X)) -> s#(active(X))
     active#(s(X)) -> active#(X) -> active#(length(X)) -> active#(X)
     active#(s(X)) -> active#(X) ->
     active#(length(X)) -> length#(active(X))
     active#(s(X)) -> active#(X) -> active#(and(X1,X2)) -> active#(X1)
     active#(s(X)) -> active#(X) ->
     active#(and(X1,X2)) -> and#(active(X1),X2)
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
     U11#(mark(X1),X2) -> U11#(X1,X2)
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L) ->
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
     and#(mark(X1),X2) -> and#(X1,X2)
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N)) ->
     and#(ok(X1),ok(X2)) -> and#(X1,X2)
     active#(length(cons(N,L))) -> isNat#(N) ->
     isNat#(ok(X)) -> isNat#(X)
     active#(length(cons(N,L))) -> isNatList#(L) ->
     isNatList#(ok(X)) -> isNatList#(X)
     active#(length(X)) -> length#(active(X)) ->
     length#(mark(X)) -> length#(X)
     active#(length(X)) -> length#(active(X)) ->
     length#(ok(X)) -> length#(X)
     active#(length(X)) -> active#(X) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(length(X)) -> active#(X) ->
     active#(U11(tt(),L)) -> length#(L)
     active#(length(X)) -> active#(X) ->
     active#(U11(tt(),L)) -> s#(length(L))
     active#(length(X)) -> active#(X) ->
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(length(X)) -> active#(X) ->
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(length(X)) -> active#(X) ->
     active#(isNatIList(V)) -> isNatList#(V)
     active#(length(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(length(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(length(X)) -> active#(X) ->
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(length(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(length(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(length(X)) -> active#(X) ->
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(length(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> isNat#(N)
     active#(length(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(length(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(length(X)) -> active#(X) ->
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(length(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> active#(X1)
     active#(length(X)) -> active#(X) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(length(X)) -> active#(X) ->
     active#(U11(X1,X2)) -> active#(X1)
     active#(length(X)) -> active#(X) ->
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     active#(length(X)) -> active#(X) ->
     active#(s(X)) -> active#(X)
     active#(length(X)) -> active#(X) ->
     active#(s(X)) -> s#(active(X))
     active#(length(X)) -> active#(X) ->
     active#(length(X)) -> active#(X)
     active#(length(X)) -> active#(X) ->
     active#(length(X)) -> length#(active(X))
     active#(length(X)) -> active#(X) ->
     active#(and(X1,X2)) -> active#(X1)
     active#(length(X)) -> active#(X) ->
     active#(and(X1,X2)) -> and#(active(X1),X2)
     active#(U11(tt(),L)) -> s#(length(L)) ->
     s#(mark(X)) -> s#(X)
     active#(U11(tt(),L)) -> s#(length(L)) -> s#(ok(X)) -> s#(X)
     active#(U11(tt(),L)) -> length#(L) ->
     length#(mark(X)) -> length#(X)
     active#(U11(tt(),L)) -> length#(L) ->
     length#(ok(X)) -> length#(X)
     active#(U11(X1,X2)) -> U11#(active(X1),X2) ->
     U11#(mark(X1),X2) -> U11#(X1,X2)
     active#(U11(X1,X2)) -> U11#(active(X1),X2) ->
     U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(U11(tt(),L)) -> length#(L)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(U11(tt(),L)) -> s#(length(L))
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatIList(V)) -> isNatList#(V)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> isNat#(N)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> active#(X1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(U11(X1,X2)) -> active#(X1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(s(X)) -> active#(X)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(s(X)) -> s#(active(X))
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(length(X)) -> active#(X)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(length(X)) -> length#(active(X))
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(and(X1,X2)) -> active#(X1)
     active#(U11(X1,X2)) -> active#(X1) ->
     active#(and(X1,X2)) -> and#(active(X1),X2)
     active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
     cons#(mark(X1),X2) -> cons#(X1,X2)
     active#(cons(X1,X2)) -> cons#(active(X1),X2) ->
     cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(zeros()) -> cons#(0(),zeros())
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(U11(tt(),L)) -> length#(L)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(U11(tt(),L)) -> s#(length(L))
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNat(length(V1))) -> isNatList#(V1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNat(s(V1))) -> isNat#(V1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatIList(V)) -> isNatList#(V)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> isNatIList#(V2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> isNat#(V1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatIList(cons(V1,V2))) -> and#(isNat(V1),isNatIList(V2))
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> isNatList#(V2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> isNat#(V1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(isNatList(cons(V1,V2))) -> and#(isNat(V1),isNatList(V2))
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> isNat#(N)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> isNatList#(L)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> and#(isNatList(L),isNat(N))
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(length(cons(N,L))) -> U11#(and(isNatList(L),isNat(N)),L)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(cons(X1,X2)) -> cons#(active(X1),X2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(U11(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(U11(X1,X2)) -> U11#(active(X1),X2)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(s(X)) -> active#(X)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(s(X)) -> s#(active(X))
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(length(X)) -> active#(X)
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(length(X)) -> length#(active(X))
     active#(cons(X1,X2)) -> active#(X1) ->
     active#(and(X1,X2)) -> active#(X1)
     active#(cons(X1,X2)) -> active#(X1) -> active#(and(X1,X2)) -> and#(active(X1),X2)
    SCC Processor:
     #sccs: 11
     #rules: 31
     #arcs: 456/3844
     DPs:
      top#(ok(X)) -> top#(active(X))
      top#(mark(X)) -> top#(proper(X))
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      proper#(isNatIList(X)) -> proper#(X)
      proper#(isNatList(X)) -> proper#(X)
      proper#(isNat(X)) -> proper#(X)
      proper#(and(X1,X2)) -> proper#(X1)
      proper#(and(X1,X2)) -> proper#(X2)
      proper#(length(X)) -> proper#(X)
      proper#(s(X)) -> proper#(X)
      proper#(U11(X1,X2)) -> proper#(X1)
      proper#(U11(X1,X2)) -> proper#(X2)
      proper#(cons(X1,X2)) -> proper#(X1)
      proper#(cons(X1,X2)) -> proper#(X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      active#(and(X1,X2)) -> active#(X1)
      active#(length(X)) -> active#(X)
      active#(s(X)) -> active#(X)
      active#(U11(X1,X2)) -> active#(X1)
      active#(cons(X1,X2)) -> active#(X1)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      isNatIList#(ok(X)) -> isNatIList#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      isNat#(ok(X)) -> isNat#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      isNatList#(ok(X)) -> isNatList#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      cons#(ok(X1),ok(X2)) -> cons#(X1,X2)
      cons#(mark(X1),X2) -> cons#(X1,X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      U11#(ok(X1),ok(X2)) -> U11#(X1,X2)
      U11#(mark(X1),X2) -> U11#(X1,X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      s#(ok(X)) -> s#(X)
      s#(mark(X)) -> s#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      length#(ok(X)) -> length#(X)
      length#(mark(X)) -> length#(X)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open
     
     DPs:
      and#(ok(X1),ok(X2)) -> and#(X1,X2)
      and#(mark(X1),X2) -> and#(X1,X2)
     TRS:
      active(zeros()) -> mark(cons(0(),zeros()))
      active(U11(tt(),L)) -> mark(s(length(L)))
      active(and(tt(),X)) -> mark(X)
      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(zeros())) -> mark(tt())
      active(isNatIList(cons(V1,V2))) -> mark(and(isNat(V1),isNatIList(V2)))
      active(isNatList(nil())) -> mark(tt())
      active(isNatList(cons(V1,V2))) -> mark(and(isNat(V1),isNatList(V2)))
      active(length(nil())) -> mark(0())
      active(length(cons(N,L))) -> mark(U11(and(isNatList(L),isNat(N)),L))
      active(cons(X1,X2)) -> cons(active(X1),X2)
      active(U11(X1,X2)) -> U11(active(X1),X2)
      active(s(X)) -> s(active(X))
      active(length(X)) -> length(active(X))
      active(and(X1,X2)) -> and(active(X1),X2)
      cons(mark(X1),X2) -> mark(cons(X1,X2))
      U11(mark(X1),X2) -> mark(U11(X1,X2))
      s(mark(X)) -> mark(s(X))
      length(mark(X)) -> mark(length(X))
      and(mark(X1),X2) -> mark(and(X1,X2))
      proper(zeros()) -> ok(zeros())
      proper(cons(X1,X2)) -> cons(proper(X1),proper(X2))
      proper(0()) -> ok(0())
      proper(U11(X1,X2)) -> U11(proper(X1),proper(X2))
      proper(tt()) -> ok(tt())
      proper(s(X)) -> s(proper(X))
      proper(length(X)) -> length(proper(X))
      proper(and(X1,X2)) -> and(proper(X1),proper(X2))
      proper(isNat(X)) -> isNat(proper(X))
      proper(isNatList(X)) -> isNatList(proper(X))
      proper(isNatIList(X)) -> isNatIList(proper(X))
      proper(nil()) -> ok(nil())
      cons(ok(X1),ok(X2)) -> ok(cons(X1,X2))
      U11(ok(X1),ok(X2)) -> ok(U11(X1,X2))
      s(ok(X)) -> ok(s(X))
      length(ok(X)) -> ok(length(X))
      and(ok(X1),ok(X2)) -> ok(and(X1,X2))
      isNat(ok(X)) -> ok(isNat(X))
      isNatList(ok(X)) -> ok(isNatList(X))
      isNatIList(ok(X)) -> ok(isNatIList(X))
      top(mark(X)) -> top(proper(X))
      top(ok(X)) -> top(active(X))
     Open