pseudo-termp-lemmas

(in-package "ACL2")

(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))))

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

(defthm pseudo-termp-lambda-lemma
  (implies (and (pseudo-termp x) (consp x) (not (symbolp (car x))))
    (and (true-listp (car x))
      (equal (length (car x)) 3)
      (eq (car (car x)) 'lambda)
      (symbol-listp (cadr (car x)))
      (pseudo-termp (caddr (car x)))
      (equal (length (cadr (car x))) (length (cdr x))))))