TYPE
  lts = tr-set;
  tr  :: O:INT-list
         L:STR-list
         D:INT-list;
ENDTYPE

FUNC dh(l)
RETURNS hd(tl(l));

FUNC cart(A,B)
RETURNS {a ^ b | a <- A, b <- B};

FUNC total (p:lts, q:lts) : lts
RETURNS  let
         ( o1 = {O(t) | t <- p},
           d1 = {D(t) | t <- p},
           l1 = {L(t) | t <- p} U {<"*">},
           o2 = {O(t) | t <- q},
           d2 = {D(t) | t <- q},
           l2 = {L(t) | t <- q} U {<"*">},
           s  = cart(o1 U d1,o2 U d2),
           l  = cart(l1,l2)   )
          in {tr(x,y,z) | x <- s, y <- l, z <- s};




FUNC prod (p:lts, q:lts) : lts
RETURNS   {t | t <- total(p,q) : f(t,Y(p)) /\ g(t,Y(q))};


Y(p) = p U {tr(O(t),<"*">,O(t)) | t <- p} U {tr(D(t),<"*">,D(t)) | t <- p};
f(t,p) = tr(<hd(O(t))>,<hd(L(t))>,<hd(D(t))>) in p;
g(t,p) = tr(<dh(O(t))>,<dh(L(t))>,<dh(D(t))>) in p;

CR(p,q) = let (x = prod(p,q) )
          in {t | t <- x : hd(L(t)) == dh(L(t))};




; test
J <- {tr(<1>,<"a">,<2>)};
K <- {tr(<10>,<"b">,<20>)};

C <- {tr(<1>,<"a">,<2>)};
A <- {tr(<11>,<"a">,<22>)};
C1 <- {tr(<10>,<"x">,<20>), tr(<20>,<"y">,<20>)};
A1 <- {tr(<100>,<"x">,<200>)};

crAC <- CR(A,C);
crA1C1 <- CR(A1,C1);
pcrACcrA1C1 <- prod(crAC,crA1C1);
pAA1 <- prod(A,A1);
pCC1 <- prod(C,C1);
crpAA1CC1 <- CR(pAA1,pCC1);
card(pcrACcrA1C1) == card(crpAA1CC1);