(VAR
    l l1 l2 l3 x xs y ys z zs)

(DATATYPES
   a = µX. < cons(b,X), nil >
   b = µX. < tuple#3(X,X,X) >
 )

(SIGNATURES
   group3 :: a -> a
   group3#1 :: a -> a
   group3#2 :: a x b -> a
   group3#3 :: a x b x b -> a
   zip3 :: a x a x a -> a
   zip3#1 :: a x a x a -> a
   zip3#2 :: a x a x b x a -> a
   zip3#3 :: a x b x a x b x a -> a
 )

(RULES
    group3(l) -> group3#1(l)
    group3#1(cons(x,xs)) -> group3#2(xs,x)
    group3#1(nil) -> nil
    group3#2(cons(y,ys),x) -> group3#3(ys,x,y)
    group3#2(nil,x) -> nil
    group3#3(cons(z,zs),x,y) -> cons(tuple#3(x,y,z),group3(zs))
    group3#3(nil,x,y) -> nil
    zip3(l1,l2,l3) -> zip3#1(l1,l2,l3)
    zip3#1(cons(x,xs),l2,l3) -> zip3#2(l2,l3,x,xs)
    zip3#1(nil,l2,l3) -> nil
    zip3#2(cons(y,ys),l3,x,xs) -> zip3#3(l3,x,xs,y,ys)
    zip3#2(nil,l3,x,xs) -> nil
    zip3#3(cons(z,zs),x,xs,y,ys) -> cons(tuple#3(x,y,z),zip3(xs,ys,zs))
    zip3#3(nil,x,xs,y,ys) -> nil)