We consider the system 729.

  Alphabet:

    abs : [term -> term] --> term 
    car : [stream] --> term 
    cdr : [stream] --> stream 
    cons : [term * stream] --> stream 
    mu : [stream -> term] --> term 
    sapp : [term * stream] --> term 
    tapp : [term * term] --> term 

  Rules:

    tapp(mu(/\x.X(x)), Y) => mu(/\y.X(cons(Y, y))) 
    sapp(mu(/\x.X(x)), Y) => X(Y) 
    abs(/\x.X(x)) => mu(/\y.sapp(X(car(y)), cdr(y))) 
    sapp(X, cons(Y, Z)) => sapp(tapp(X, Y), Z) 
    car(cons(X, Y)) => X 
    cdr(cons(X, Y)) => Y 
    mu(/\x.sapp(X, x)) => X 
    cons(car(X), cdr(X)) => X 
    sapp(tapp(X, car(Y)), cdr(Y)) => sapp(X, Y) 
    tapp(abs(/\x.X(x)), Y) => X(Y) 
    abs(/\x.tapp(X, x)) => X 

This system is non-terminating, as demonstrated by the following reduction:

  tapp(abs(/\x.tapp(x, x)), abs(/\y.tapp(y, y))) 
    => (/\x.tapp(x, x)) abs(/\y.tapp(y, y)) 
    =>_beta tapp(abs(/\x.tapp(x, x)), abs(/\y.tapp(y, y))) 

That is, a term reduces to itself.