YES(O(1), O(n^1)) 215.03/63.20 YES(O(1), O(n^1)) 215.40/63.22 215.40/63.22 215.40/63.22
215.40/63.22 215.40/63.220 CpxTRS215.40/63.22
↳1 CpxTrsMatchBoundsTAProof (⇔)215.40/63.22
↳2 BOUNDS(O(1), O(n^1))215.40/63.22
active(zeros) → mark(cons(0, zeros)) 215.40/63.22
active(U11(tt, L)) → mark(U12(tt, L)) 215.40/63.22
active(U12(tt, L)) → mark(s(length(L))) 215.40/63.22
active(U21(tt, IL, M, N)) → mark(U22(tt, IL, M, N)) 215.40/63.22
active(U22(tt, IL, M, N)) → mark(U23(tt, IL, M, N)) 215.40/63.22
active(U23(tt, IL, M, N)) → mark(cons(N, take(M, IL))) 215.40/63.22
active(length(nil)) → mark(0) 215.40/63.22
active(length(cons(N, L))) → mark(U11(tt, L)) 215.40/63.22
active(take(0, IL)) → mark(nil) 215.40/63.22
active(take(s(M), cons(N, IL))) → mark(U21(tt, IL, M, N)) 215.40/63.22
active(cons(X1, X2)) → cons(active(X1), X2) 215.40/63.22
active(U11(X1, X2)) → U11(active(X1), X2) 215.40/63.22
active(U12(X1, X2)) → U12(active(X1), X2) 215.40/63.22
active(s(X)) → s(active(X)) 215.40/63.22
active(length(X)) → length(active(X)) 215.40/63.22
active(U21(X1, X2, X3, X4)) → U21(active(X1), X2, X3, X4) 215.40/63.22
active(U22(X1, X2, X3, X4)) → U22(active(X1), X2, X3, X4) 215.40/63.22
active(U23(X1, X2, X3, X4)) → U23(active(X1), X2, X3, X4) 215.40/63.22
active(take(X1, X2)) → take(active(X1), X2) 215.40/63.22
active(take(X1, X2)) → take(X1, active(X2)) 215.40/63.22
cons(mark(X1), X2) → mark(cons(X1, X2)) 215.40/63.22
U11(mark(X1), X2) → mark(U11(X1, X2)) 215.40/63.22
U12(mark(X1), X2) → mark(U12(X1, X2)) 215.40/63.22
s(mark(X)) → mark(s(X)) 215.40/63.22
length(mark(X)) → mark(length(X)) 215.40/63.22
U21(mark(X1), X2, X3, X4) → mark(U21(X1, X2, X3, X4)) 215.40/63.22
U22(mark(X1), X2, X3, X4) → mark(U22(X1, X2, X3, X4)) 215.40/63.22
U23(mark(X1), X2, X3, X4) → mark(U23(X1, X2, X3, X4)) 215.40/63.22
take(mark(X1), X2) → mark(take(X1, X2)) 215.40/63.22
take(X1, mark(X2)) → mark(take(X1, X2)) 215.40/63.22
proper(zeros) → ok(zeros) 215.40/63.22
proper(cons(X1, X2)) → cons(proper(X1), proper(X2)) 215.40/63.22
proper(0) → ok(0) 215.40/63.22
proper(U11(X1, X2)) → U11(proper(X1), proper(X2)) 215.40/63.22
proper(tt) → ok(tt) 215.40/63.22
proper(U12(X1, X2)) → U12(proper(X1), proper(X2)) 215.40/63.22
proper(s(X)) → s(proper(X)) 215.40/63.22
proper(length(X)) → length(proper(X)) 215.40/63.22
proper(U21(X1, X2, X3, X4)) → U21(proper(X1), proper(X2), proper(X3), proper(X4)) 215.40/63.22
proper(U22(X1, X2, X3, X4)) → U22(proper(X1), proper(X2), proper(X3), proper(X4)) 215.40/63.22
proper(U23(X1, X2, X3, X4)) → U23(proper(X1), proper(X2), proper(X3), proper(X4)) 215.40/63.22
proper(take(X1, X2)) → take(proper(X1), proper(X2)) 215.40/63.22
proper(nil) → ok(nil) 215.40/63.22
cons(ok(X1), ok(X2)) → ok(cons(X1, X2)) 215.40/63.22
U11(ok(X1), ok(X2)) → ok(U11(X1, X2)) 215.40/63.22
U12(ok(X1), ok(X2)) → ok(U12(X1, X2)) 215.40/63.22
s(ok(X)) → ok(s(X)) 215.40/63.22
length(ok(X)) → ok(length(X)) 215.40/63.22
U21(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U21(X1, X2, X3, X4)) 215.40/63.22
U22(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U22(X1, X2, X3, X4)) 215.40/63.22
U23(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U23(X1, X2, X3, X4)) 215.40/63.22
take(ok(X1), ok(X2)) → ok(take(X1, X2)) 215.40/63.22
top(mark(X)) → top(proper(X)) 215.40/63.22
top(ok(X)) → top(active(X))