sublis-var

(local (defun sublis-var1-flg
    (flg alist x)
    (cond (flg (cond ((endp x) (mv nil x))
          (t (mv-let (changedp1 term)
              (sublis-var1-flg nil alist (car x))
              (mv-let (changedp2 lst)
                (sublis-var1-flg t alist (cdr x))
                (cond ((or changedp1 changedp2) (mv t (cons term lst)))
                  (t (mv nil x))))))))
      (t (cond ((variablep x) (let ((a (assoc-eq x alist)))
              (cond (a (mv (not (eq x (cdr a))) (cdr a))) (t (mv nil x)))))
          ((fquotep x) (mv nil x))
          (t (mv-let (changedp lst)
              (sublis-var1-flg t alist (fargs x))
              (let ((fn (ffn-symb x)))
                (cond (changedp (mv t (cons-term fn lst)))
                  ((and (symbolp fn) (quote-listp lst)) (cons-term1-mv2 fn lst x))
                  (t (mv nil x)))))))))))

(local (defthmd sublis-var1-flg-property
    (equal (sublis-var1-flg flg alist x)
      (if flg
        (sublis-var1-lst alist x)
        (sublis-var1 alist x)))))

(local (defthm sublis-var1-flg-preserves-len
    (implies flg
      (equal (len (mv-nth 1 (sublis-var1-flg flg alist x)))
        (len x)))))

(local (defthm pseudo-termp-sublis-var1-flg
    (implies (and (symbol-alistp alist)
        (pseudo-term-listp (strip-cdrs alist))
        (if flg
          (pseudo-term-listp x)
          (pseudo-termp x)))
      (if flg
        (pseudo-term-listp (mv-nth 1 (sublis-var1-flg flg alist x)))
        (pseudo-termp (mv-nth 1 (sublis-var1-flg flg alist x)))))
    :rule-classes nil))

(local (defthm pseudo-termp-implies-pseudo-term-listp-cdr
    (implies (and (pseudo-termp x)
        (consp x)
        (not (equal (car x) 'quote)))
      (pseudo-term-listp (cdr x)))))

(local (defthm pseudo-term-listp-implies-true-listp
    (implies (pseudo-term-listp x) (true-listp x))))