This is the Lisp implementation of Algorithms 1 and 2 of the paper 
<I>Towards Automating the Discovery of Decreasing Measures</I> by
R.S. Boyer, W.J. Legato and V.W. Marek

;;; We represent each of the sets S(j,i) as an integer bit vector
;;;                       k
;;; s(j,i) =   sum       2
;;;          x in S(j,i)
;;;           k
;;; Let s = ((s(1,1) s(1,2) ... s(1.n))
;;;          (s(2,1) s(2,2) ... s(2,n))
;;;                 ...
;;;          (s(m,1) s(m,2) ... s(m,n)))

;;; Algorithm 1

(defun measure-ok (s)
  (do       ; loop until the prefix p is stable
   ((p 1)   ; initially p is empty
    (pp 0)) ; the old value of p
   ((equal p pp) ; when p is stable, return true iff all xi
    (equal (1+ (length (car s))) (logcount p))) ; are assigned
   (setq pp p)
   (do     ; intersect the "ready" sets over all j
    ((sj s (cdr sj))
     (pmask -1)) ; prepare to intersect ready vars over all j
    ((null sj) (setq p (logior p pmask))) ; extend prefix
    (do    ; compute the "ready" set for the jth substitution
     ((i 2 (+ i i)) ; advance i over powers of 2
      (ready 0)
      (si (car sj) (cdr si))) ; si = (S(j,1) S(j,2), ... S(j,n))
     ((null si)
      (setq pmask (logand pmask ready))) ; must be ready for j
     (and (zerop (logand p i)) ; if xi is not assigned and S(j,i)
          (or (zerop (logand p (car si))) ; holds an assigned var
              (setq ready (logior i ready)))))))) ; xi is ready

;;; Generate the s(j,i), where the kth element of the list sub
;;; represents whether variable xk went up, down or remained the
;;; same under the jth substitution.

(defun predecessor (sub)
  (let ((down
         (do ; generate the set Gj of the paper
          ((i 2 (+ i i))
           (pmask 0)
           (sub sub (cdr sub)))
          ((null sub) pmask)
          (and (equal (car sub) 'down)
               (setq pmask (logior pmask i))))))
    (do
     ((sub sub (cdr sub))
      (s nil)) ; generate sj
     ((null sub) (reverse s))
     (push (case (car sub)
                 ('equal (if (zerop down) 0 1)) ; unconstrained
                 ('down 1) ; unconstrained
                 ('up down); must follow a decreasing variable
                 (t t))  ; this should never happen
           s))))

;;; Create the list of sj's.

(defun s-gen (subs)
  (mapcar #'predecessor subs))

;;; Generate the mask of positions within sub with value key.

(defun gen-mask (sub key)
  (do ((sub sub (cdr sub))
       (i 2 (+ i i))
       (d 1))
      ((null sub) d)
      (and (equal (car sub) key)
           (setq d (+ d i)))))


;;; Algorithm 2

;;; D(j,i) = 1 if substitution j provably goes down on variable i
;;; U(j,i) = 1 if substitution j possibly goes up on variable i
;;; Variables are indexed starting with 1.  D(j,0) = U(j,0) = 1
;;;
;;; D(j) = sum D(j,i)*2^i, ds = (D(1) D(2) ... D(m))
;;;         i
;;;
;;; U(j) = sum U(j,i)*2^i, us = (U(1) U(2) ... U(m))
;;;         i
;;;

;;; due is destructive on the lists ds and us.
;;; Use (due (copy-list ds) (copy-list us))
;;; to preserve original values.

(defun due (ds us)
  (let (d u m)
    (loop
     (setq d (reduce #'logior ds)
           u (reduce #'logior us)
           m (logand d (lognot u)))
     (or (not (zerop m))
         (return (if (zerop (logior d u))
                     t
                   nil)))
     (do ((ds ds (cdr ds))
          (us us (cdr us)))
         ((null ds))
         (or (zerop (logand m (car ds)))
             (setf (car ds) 0
                   (car us) 0))))))

;;; Compare algorithms 1 and 2 on ntries randomly generated
;;; tests of nvars variables and nsubs substitutions.

(defun tess (nvars nsubs ntries)
  (let ((flg t))
    (dotimes (k ntries flg)
      (let* ((test
              (do ((j 0 (1+ j))
                   (subs nil (cons
                              (do ((i 0 (1+ i))
                                   (sub nil (cons 
                                             (case (random 3)
                                                   (0 'up)
                                                   (1 'down)
                                                   (2 'equal))
                                             sub)))
                                  ((<= nvars i) sub))
                              subs)))
                  ((<= nsubs j) subs)))
             (masks (s-gen test))
             (ds (mapcar #'(lambda (x) (gen-mask x 'down)) test))
             (us (mapcar #'(lambda (x) (gen-mask x 'up)) test))
             (t1 (measure-ok masks))
             (t2 (due ds us)))
        (format t "test=~A due=~A~%" test t2)
        (format t "Algorithms agree? = ~A~%" (equal t1 t2))
        (setq flg (and flg (equal t1 t2)))))))