MAYBE

Problem:
 and(tt(),X) -> activate(X)
 plus(N,0()) -> N
 plus(N,s(M)) -> s(plus(N,M))
 x(N,0()) -> 0()
 x(N,s(M)) -> plus(x(N,M),N)
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   and#(tt(),X) -> activate#(X)
   plus#(N,s(M)) -> plus#(N,M)
   x#(N,s(M)) -> x#(N,M)
   x#(N,s(M)) -> plus#(x(N,M),N)
  TRS:
   and(tt(),X) -> activate(X)
   plus(N,0()) -> N
   plus(N,s(M)) -> s(plus(N,M))
   x(N,0()) -> 0()
   x(N,s(M)) -> plus(x(N,M),N)
   activate(X) -> X
  Open