Problem 1.

   rules:   dx, strict op.	\dE-

	    s := {}		E':= {}

	    s with:= y		E'(f(y)) +:= 1
						
	    s less:= y		E'(f(y)) -:= 1

	    f :={}		E':= {}

	    f(y):=om		if y in s then
				  E'(f(y)) -:=1

	    f(y):=z		if y in s then
				  E'(z) +:= 1

   Note that, same as in rule M2 in paper, we assume that any use of
   E'(z) for which z is outside the domain of E' has the value 0 and
   that any assignment of 0 to E(z) removes z from the domain of E.

   Otherwise, we just need to add the corresponding code, in particular,
   for s with:=y, we have if E'(f(y))=om then E'(f(y))=1 else E'(f(y)) +:= 1.
   for s less:=y, we have if E'(f(y))=1 then E'(f(y))=om else E'(f(y)) -:= 1.

Problem 2.

   No.  Either way we get \dE2,E1 = \dE2<\dE1> \dE2<\dE1>

Problem 3.

   Change the expression [[U,X],W] to [[U,W],X].

Problem 4.

   It is easy to see how this cycle test problem is similar to the
   tree center problem and the topological sort problem.

given:
    program cycle1;
      ...
      s := domain e;
      while exists x in s| e{x} * s = {} loop
        s less:= u;
      end loop;
      ...
    end;

canonical forms:
  s*t --> {x in s| x in t}
  s={} --> #s = 0
  exists x in s --> exists x in {x in s}

  B: while exists x in {x in s| #{y in e{x}| y in s} = 0}
        s less:= x;

expensive computations:
  E1 = {y in e{x}| y in s} nodes in s that are successors of x based on e
  E2 = #E1 number of above
  E3 = {x in s| E2=0} nodes in s that have no successors

auxiliary expressions:
  E1 is needed for any x in s
  E2 too
  E4 = {[y,x]:[x,y] in e}

maintain:
  for E1: succ = {[x,y] in e| y in s} so succ{x} = E1
  for E2: nsucc= {[x,#succ{x}]: x in domain succ} so nsucc(x) = E2
  for E3: tail = {x in s|nsucc(x)=0}
  for E4: pred = {[y,x]:[x,y] in e}

FD:
  \d succ, nsucc, tail, pred<B>
 =\d nsucc, tail, pred<\d succ<B>> -- chain rule
		1. insert \d-succ<s less:=x> before s less:=x
			  = for u in domain e| [u,x] in e -- rule D2
			      succ{u} less:= x;
			  = for u in pred{x} -- can be viewed \d pred
			      succ{u} less:= x;
		2. replace {y in e{x}| y in s} by succ{x}
  B1: while exists x in {x in s | #succ{x} = 0}
	for u in pred{x}
	  succ{u} less:= x;
        s less:= x;

 =\d nsucc, tail<B1>
 =\d tail<\d nsucc<B1>> -- chain rule
	  1. insert \d-nsucc<succ{u} less:=x> before succ{u} less:=x
		    = nsucc(u) -:= 1 -- rule M2
	  2. replace #succ{x} by nsucc(x)
  B2: while exists x in {x in s| nsucc(x) = 0}
	for u in pred{x}
	  nsucc(u) -:= 1;
	  succ{u} less:= x;
        s less:= x;

 =\d tail<B2>
  1. insert \d-tail<nsucc(u) -:= 1> before nsucc(u) -:= 1
	    = if nsucc(u)=1 then
		tail with:= u;
     insert \d-tail<s less:= x> before s less:= x
	    = if nsucc(x)=0 then
		tail less:= x;
  2. replace {x in s| nsucc(x) = 0} by tail
  B3: while exists x in tail
	for u in pred{x}
	  if nsucc(u)=1 then
	    tail with:= u;
	  nsucc(u) -:= 1;
	  succ{u} less:= x; -- stmt and succ not needed (see later)
	if nsucc(x)=0 then -- cond always true, since x in tail
	  tail less:= x;
        s less:= x;