(VAR E K S u u2 v v2 )

(DATATYPES a = µX. < tt, ff, nil, dd(X,X) >
 )

(SIGNATURES
   ite :: a x a x a -> a
   find :: a x a x a -> a
   complete :: a x a x a -> a
   clique :: a x a -> a
   choice :: a x a x a -> a
 )


(RULES
  ite(tt, u, v) -> u
  ite(ff, u, v) -> v
  find(u, v, nil) -> ff
  find(u, v, dd(dd(u, v), E)) -> tt
  find(u, v, dd(dd(u2, v2), E)) -> find(u, v, E)
  complete(u, nil, E) -> tt
  complete(u, dd(v, S), E) -> ite(find(u, v, E), complete(u, S, E), ff)
  clique(nil, E) -> tt
  clique(dd(u, K), E) -> ite(complete(u, K, E), clique(K, E), ff)
  choice(nil, K, E) -> ite(clique(K, E), K, nil)
  choice(dd(u, S), K, E) -> choice(S, dd(u, K), E)
  choice(dd(u, S), K, E) -> choice(S, K, E)
)