MAYBE
MAYBE
TRS:
 {
  a(lambda(x), y) -> lambda(a(x, p(1(), a(y, t())))),
    a(a(x, y), z) -> a(x, a(y, z)),
    a(p(x, y), z) -> p(a(x, z), a(y, z)),
  a(1(), p(x, y)) -> x,
     a(1(), id()) -> 1(),
  a(t(), p(x, y)) -> y,
     a(t(), id()) -> t(),
       a(id(), x) -> x
 }
 DUP: We consider a duplicating system.
  Trs:
   {
    a(lambda(x), y) -> lambda(a(x, p(1(), a(y, t())))),
      a(a(x, y), z) -> a(x, a(y, z)),
      a(p(x, y), z) -> p(a(x, z), a(y, z)),
    a(1(), p(x, y)) -> x,
       a(1(), id()) -> 1(),
    a(t(), p(x, y)) -> y,
       a(t(), id()) -> t(),
         a(id(), x) -> x
   }
  Fail