Problem: zeros() -> cons(0(),n__zeros()) and(tt(),X) -> activate(X) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(X1,X2) activate(X) -> X Proof: Matrix Interpretation Processor: dim=1 interpretation: [n__take](x0, x1) = x0 + x1, [take](x0, x1) = x0 + x1, [s](x0) = x0, [length](x0) = x0, [nil] = 0, [activate](x0) = x0, [and](x0, x1) = 7x0 + x1, [tt] = 3, [cons](x0, x1) = 6x0 + x1, [n__zeros] = 0, [0] = 0, [zeros] = 0 orientation: zeros() = 0 >= 0 = cons(0(),n__zeros()) and(tt(),X) = X + 21 >= X = activate(X) length(nil()) = 0 >= 0 = 0() length(cons(N,L)) = L + 6N >= L = s(length(activate(L))) take(0(),IL) = IL >= 0 = nil() take(s(M),cons(N,IL)) = IL + M + 6N >= IL + M + 6N = cons(N,n__take(M,activate(IL))) zeros() = 0 >= 0 = n__zeros() take(X1,X2) = X1 + X2 >= X1 + X2 = n__take(X1,X2) activate(n__zeros()) = 0 >= 0 = zeros() activate(n__take(X1,X2)) = X1 + X2 >= X1 + X2 = take(X1,X2) activate(X) = X >= X = X problem: zeros() -> cons(0(),n__zeros()) length(nil()) -> 0() length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(X1,X2) activate(X) -> X Matrix Interpretation Processor: dim=1 interpretation: [n__take](x0, x1) = 5x0 + 2x1, [take](x0, x1) = 5x0 + 2x1, [s](x0) = x0, [length](x0) = 2x0 + 1, [nil] = 0, [activate](x0) = x0, [cons](x0, x1) = 4x0 + x1, [n__zeros] = 0, [0] = 0, [zeros] = 0 orientation: zeros() = 0 >= 0 = cons(0(),n__zeros()) length(nil()) = 1 >= 0 = 0() length(cons(N,L)) = 2L + 8N + 1 >= 2L + 1 = s(length(activate(L))) take(0(),IL) = 2IL >= 0 = nil() take(s(M),cons(N,IL)) = 2IL + 5M + 8N >= 2IL + 5M + 4N = cons(N,n__take(M,activate(IL))) zeros() = 0 >= 0 = n__zeros() take(X1,X2) = 5X1 + 2X2 >= 5X1 + 2X2 = n__take(X1,X2) activate(n__zeros()) = 0 >= 0 = zeros() activate(n__take(X1,X2)) = 5X1 + 2X2 >= 5X1 + 2X2 = take(X1,X2) activate(X) = X >= X = X problem: zeros() -> cons(0(),n__zeros()) length(cons(N,L)) -> s(length(activate(L))) take(0(),IL) -> nil() take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() take(X1,X2) -> n__take(X1,X2) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(X1,X2) activate(X) -> X Matrix Interpretation Processor: dim=1 interpretation: [n__take](x0, x1) = x0 + x1 + 1, [take](x0, x1) = 2x0 + 2x1 + 2, [s](x0) = x0, [length](x0) = 4x0, [nil] = 0, [activate](x0) = 2x0, [cons](x0, x1) = 4x0 + 2x1, [n__zeros] = 0, [0] = 0, [zeros] = 0 orientation: zeros() = 0 >= 0 = cons(0(),n__zeros()) length(cons(N,L)) = 8L + 16N >= 8L = s(length(activate(L))) take(0(),IL) = 2IL + 2 >= 0 = nil() take(s(M),cons(N,IL)) = 4IL + 2M + 8N + 2 >= 4IL + 2M + 4N + 2 = cons(N,n__take(M,activate(IL))) zeros() = 0 >= 0 = n__zeros() take(X1,X2) = 2X1 + 2X2 + 2 >= X1 + X2 + 1 = n__take(X1,X2) activate(n__zeros()) = 0 >= 0 = zeros() activate(n__take(X1,X2)) = 2X1 + 2X2 + 2 >= 2X1 + 2X2 + 2 = take(X1,X2) activate(X) = 2X >= X = X problem: zeros() -> cons(0(),n__zeros()) length(cons(N,L)) -> s(length(activate(L))) take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) zeros() -> n__zeros() activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(X1,X2) activate(X) -> X Matrix Interpretation Processor: dim=1 interpretation: [n__take](x0, x1) = x0 + x1, [take](x0, x1) = 4x0 + 4x1 + 3, [s](x0) = x0, [length](x0) = 4x0 + 4, [activate](x0) = 4x0 + 3, [cons](x0, x1) = 3x0 + 4x1 + 3, [n__zeros] = 1, [0] = 0, [zeros] = 7 orientation: zeros() = 7 >= 7 = cons(0(),n__zeros()) length(cons(N,L)) = 16L + 12N + 16 >= 16L + 16 = s(length(activate(L))) take(s(M),cons(N,IL)) = 16IL + 4M + 12N + 15 >= 16IL + 4M + 3N + 15 = cons(N,n__take(M,activate(IL))) zeros() = 7 >= 1 = n__zeros() activate(n__zeros()) = 7 >= 7 = zeros() activate(n__take(X1,X2)) = 4X1 + 4X2 + 3 >= 4X1 + 4X2 + 3 = take(X1,X2) activate(X) = 4X + 3 >= X = X problem: zeros() -> cons(0(),n__zeros()) length(cons(N,L)) -> s(length(activate(L))) take(s(M),cons(N,IL)) -> cons(N,n__take(M,activate(IL))) activate(n__zeros()) -> zeros() activate(n__take(X1,X2)) -> take(X1,X2) Unfolding Processor: loop length: 3 terms: length(cons(N,n__zeros())) s(length(activate(n__zeros()))) s(length(zeros())) context: s([]) substitution: N -> 0() Qed