We consider the system 776.

  Alphabet:

    0 : [] --> G 
    app : [ArGG * G] --> G 
    false : [] --> B 
    fix : [G -> G] --> G 
    fix2 : [G -> G -> PrGG] --> PrGG 
    if : [B * G * G] --> G 
    lam : [G -> G] --> ArGG 
    pair : [G * G] --> PrGG 
    true : [] --> B 
    union : [G * G] --> G 

  Rules:

    app(lam(/\x.X(x)), Y) => X(Y) 
    lam(/\x.app(X, x)) => X 
    union(X, 0) => X 
    union(0, X) => X 
    union(union(X, Y), Z) => union(X, union(Y, Z)) 
    union(X, Y) => union(Y, X) 
    fix2(/\x./\y.pair(X(x, y), Y(x, y))) => pair(fix(/\z.X(z, z)), fix(/\u.Y(u, u))) 
    if(true, X, Y) => X 
    if(false, X, Y) => Y 

It is easy to see that this system is non-terminating:

  union(x, 0) 
    => union(0, x) 
    => union(x, 0) 

That is, a term s reduces to a term t which instantiates s.