pseudo-good-worldp

(defun safe-access-event-tuple-number
  (x)
  (let ((x (safe-remove-local x)))
    (if (consp x)
      (if (integerp (car x))
        (car x)
        (if (consp (car x))
          (if (integerp (caar x))
            (caar x)
            -2)
          -2))
      -2)))

(defun pseudo-event-indexp
  (x w)
  (declare (xargs :guard (plist-worldp w)))
  (cond ((consp x) (and (equal (car x) (- (len (cdr x)) 1))
        (equal (safe-access-event-tuple-number (fgetprop 'event-landmark 'global-value nil w))
          (* (car x) *event-index-interval*))
        (consp (cdr x))
        (equal (cadr x) w)
        (or (consp (fgetprop 'event-index 'global-value nil w))
          (null (fgetprop 'event-index 'global-value nil w)))
        (equal (cddr x)
          (cdr (fgetprop 'event-index 'global-value nil w)))))
    (t (and (null x)
        (null (fgetprop 'event-index 'global-value nil w))))))

(defun safe-access-command-tuple-number
  (x)
  (if (consp x)
    (if (integerp (car x))
      (car x)
      -2)
    -2))

(defun pseudo-command-indexp
  (x w)
  (declare (xargs :guard (plist-worldp w)))
  (cond ((consp x) (and (equal (car x) (- (len (cdr x)) 1))
        (equal (safe-access-command-tuple-number (fgetprop 'command-landmark 'global-value nil w))
          (* (car x) *event-index-interval*))
        (consp (cdr x))
        (equal (cadr x) w)
        (or (consp (fgetprop 'command-index 'global-value nil w))
          (null (fgetprop 'command-index 'global-value nil w)))
        (equal (cddr x)
          (cdr (fgetprop 'command-index 'global-value nil w)))))
    (t (and (null x)
        (null (fgetprop 'command-index 'global-value nil w))))))

(defun pseudo-runep
  (rune)
  (and (consp rune)
    (keywordp (car rune))
    (consp (cdr rune))
    (symbolp (cadr rune))
    (or (null (cddr rune)) (natp (cddr rune)))))

(defun pseudo-function-symbolp
  (fn n)
  (declare (ignore n))
  (symbolp fn))

(defun pseudo-function-symbol-listp
  (lst n)
  (if (atom lst)
    (null lst)
    (and (pseudo-function-symbolp (car lst) n)
      (pseudo-function-symbol-listp (cdr lst) n))))

(defun pseudo-well-founded-relation-alistp
  (val)
  (cond ((atom val) (null val))
    ((and (consp (car val)) (consp (cdr (car val)))) (let ((rel (car (car val))) (m (cadr (car val)))
          (rune (cddr (car val))))
        (and (pseudo-function-symbolp rel 2)
          (pseudo-function-symbolp m 1)
          (pseudo-runep rune)
          (pseudo-well-founded-relation-alistp (cdr val)))))
    (t nil)))

(defun pseudo-numep (n) (natp n))

(defun pseudo-built-in-clause-recordp
  (x)
  (case-match x
    (((nume . all-fnnames) clause . rune) (and (or (null nume) (pseudo-numep nume))
        (pseudo-function-symbol-listp all-fnnames nil)
        (pseudo-term-listp clause)
        (pseudo-runep rune)))
    (& nil)))

(defun pseudo-built-in-clause-record-listp
  (x)
  (if (atom x)
    (null x)
    (and (pseudo-built-in-clause-recordp (car x))
      (pseudo-built-in-clause-record-listp (cdr x)))))

(defun pseudo-built-in-clausesp
  (x)
  (if (atom x)
    (null x)
    (and (consp (car x))
      (pseudo-function-symbolp (car (car x)) nil)
      (pseudo-built-in-clause-record-listp (cdr (car x)))
      (pseudo-built-in-clausesp (cdr x)))))

(defun pseudo-attach-nil-lst
  (lst)
  (pseudo-function-symbol-listp lst nil))

(defun attachment-components-pathp
  (path)
  (cond ((atom path) (null path))
    (t (and (pseudo-function-symbolp (car path) nil)
        (attachment-components-pathp (cdr path))))))

(defun attachment-component-p
  (c)
  (case-match c
    (('attachment-component (ext-anc . ord-anc) . path) (and (pseudo-function-symbol-listp ext-anc nil)
        (pseudo-function-symbol-listp ord-anc nil)
        (attachment-components-pathp path)))))

(defun attachment-components-p
  (components)
  (cond ((atom components) (null components))
    (t (and (attachment-component-p (car components))
        (attachment-components-p (cdr components))))))

(defun pseudo-attachment-recordp
  (x)
  (case-match x
    (('attachment (g . ext-succ) components . pairs) (and (pseudo-function-symbol-listp ext-succ nil)
        (pseudo-function-symbolp g nil)
        (attachment-components-p components)
        (symbol-alistp pairs)
        (r-symbol-alistp pairs)))
    (& nil)))

(defun pseudo-attachment-recordsp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-attachment-recordp (car x))
        (pseudo-attachment-recordsp (cdr x))))))

(defun pseudo-attachments-at-ground-zerop
  (x)
  (cond ((atom x) (null x))
    (t (and (consp (car x))
        (pseudo-function-symbolp (caar x) nil)
        (pseudo-function-symbolp (cdar x) nil)
        (pseudo-attachments-at-ground-zerop (cdr x))))))

(defun pseudo-half-length-built-in-clausesp (n) (natp n))

(defun type-setp
  (n)
  (and (integerp n)
    (<= *min-type-set* n)
    (<= n *max-type-set*)))

(defun pseudo-type-set-inverter-rule-recordp
  (x)
  (case-match x
    (('type-set-inverter-rule (nume . ts) terms . rune) (and (or (null nume) (pseudo-numep nume))
        (type-setp ts)
        (pseudo-term-listp terms)
        (pseudo-runep rune)))
    (& nil)))

(defun pseudo-type-set-inverter-rulesp
  (val)
  (if (atom val)
    (null val)
    (and (pseudo-type-set-inverter-rule-recordp (car val))
      (pseudo-type-set-inverter-rulesp (cdr val)))))

(defun pseudo-rune-array1p
  (a)
  (declare (xargs :guard (alistp a)))
  (cond ((atom a) (null a))
    ((eq (car (car a)) :header) (pseudo-rune-array1p (cdr a)))
    (t (and (pseudo-runep (cdr (car a)))
        (pseudo-rune-array1p (cdr a))))))

(defun pseudo-enabled-structure-recordp
  (val)
  (case-match val
    (((index-of-last-enabling . theory-array) (array-name . array-length)
       array-name-root . array-name-suffix) (and (integerp index-of-last-enabling)
        (<= -1 index-of-last-enabling)
        (symbolp array-name)
        (array1p array-name theory-array)
        (pseudo-rune-array1p theory-array)
        (natp array-length)
        (character-listp array-name-root)
        (natp array-name-suffix)))
    (& nil)))

(defun pseudo-global-arithmetic-enabled-structurep
  (val)
  (pseudo-enabled-structure-recordp val))

(defun operating-systemp
  (val)
  (member-eq val '(:unix :apple :mswindows)))

(defun event-number-baselinep (val) (natp val))

(defun command-number-baseline-infop
  (val)
  (case-match val
    (('command-number-baseline-info current
       permament-p . original) (and (natp current) (booleanp permament-p) (natp original)))
    (& nil)))

(defun pseudo-arglistp (x) (symbol-listp x))

(defun pseudo-internal-signaturep
  (insig)
  (case-match insig
    ((fn formals stobjs-in stobjs-out) (and (pseudo-function-symbolp fn nil)
        (pseudo-arglistp formals)
        (symbol-listp stobjs-in)
        (symbol-listp stobjs-out)
        (equal (len formals) (len stobjs-in))))
    (& nil)))

(defun pseudo-internal-signature-listp
  (x)
  (if (atom x)
    (null x)
    (and (pseudo-internal-signaturep (car x))
      (pseudo-internal-signature-listp (cdr x)))))

(defun pseudo-embedded-event-lst-entryp
  (ee-entry)
  (and (consp ee-entry)
    (if (eq (car ee-entry) 'encapsulate)
      (and (consp (cdr ee-entry))
        (pseudo-internal-signature-listp (cadr ee-entry)))
      t)
    (if (eq (car ee-entry) 'include-book)
      (and (consp (cdr ee-entry)) (book-name-p (cadr ee-entry)))
      t)))

(defun pseudo-embedded-event-lstp
  (val)
  (if (atom val)
    (null val)
    (and (pseudo-embedded-event-lst-entryp (car val))
      (pseudo-embedded-event-lstp (cdr val)))))

(defun pseudo-cltl-commandp
  (val)
  (case-match val
    (('defuns defun-mode ignorep . defs) (and (or (null defun-mode)
          (eq defun-mode :program)
          (eq defun-mode :logic))
        (or (eq ignorep 'reclassifying)
          (and (consp ignorep)
            (eq (car ignorep) 'defstobj)
            (pseudo-function-symbolp (cdr ignorep) nil))
          (null ignorep))
        (true-listp defs)))
    (& t)))

(defun pseudo-cltl-command-listp
  (val)
  (cond ((atom val) (null val))
    (t (and (pseudo-cltl-commandp (car val))
        (pseudo-cltl-command-listp (cdr val))))))

(defun pseudo-include-book-alist-entryp
  (entry)
  (case-match entry
    ((full-name user-name
       familiar-name
       cert-annotations . chk-sum) (and (book-name-p full-name)
        (stringp user-name)
        (stringp familiar-name)
        (or (null cert-annotations)
          (cert-annotationsp cert-annotations))
        (case-match chk-sum
          (((':book-length . book-length) (':book-write-date . book-write-date)) (and (natp book-length) (natp book-write-date)))
          (& (or (integerp chk-sum) (eq chk-sum nil))))))
    (& nil)))

(defun pseudo-include-book-alist-entry-listp
  (x local-markers-allowedp)
  (cond ((atom x) (equal x nil))
    ((and local-markers-allowedp
       (consp (car x))
       (eq (car (car x)) 'local)
       (consp (cdr (car x)))
       (equal (cddr (car x)) nil)) (and (pseudo-include-book-alist-entryp (cadr (car x)))
        (pseudo-include-book-alist-entry-listp (cdr x)
          local-markers-allowedp)))
    (t (and (pseudo-include-book-alist-entryp (car x))
        (pseudo-include-book-alist-entry-listp (cdr x)
          local-markers-allowedp)))))

(defun pseudo-include-book-alistp
  (val)
  (pseudo-include-book-alist-entry-listp val t))

(defun pseudo-include-book-alist-allp
  (val)
  (pseudo-include-book-alistp val))

(defun pseudo-pcert-booksp (val) (book-name-listp val))

(defun pseudo-include-book-pathp
  (val)
  (book-name-listp val))

(defun certification-tuplep
  (val)
  (or (null val) (pseudo-include-book-alist-entryp val)))

(defun pseudo-functional-substitution-pairp
  (x)
  (case-match x
    ((fn 'lambda vars body) (and (pseudo-function-symbolp fn nil)
        (pseudo-arglistp vars)
        (pseudo-termp body)))
    ((fn . fn1) (and (pseudo-function-symbolp fn nil)
        (pseudo-function-symbolp fn1 nil)))
    (& nil)))

(defun pseudo-functional-substitutionp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-functional-substitution-pairp (car x))
        (pseudo-functional-substitutionp (cdr x))))))

(defun proved-functional-instances-alist-entryp
  (x)
  (case-match x
    ((name fn-subst . on-behalf) (and (symbolp name)
        (pseudo-functional-substitutionp fn-subst)
        (or (equal on-behalf 0) (symbolp on-behalf))))
    (& nil)))

(defun proved-functional-instances-alistp
  (val)
  (cond ((atom val) (null val))
    (t (and (proved-functional-instances-alist-entryp (car val))
        (proved-functional-instances-alistp (cdr val))))))

(defun nonconstructive-axiom-namesp
  (val)
  (symbol-listp val))

(defun pseudo-theoryp1
  (lst)
  (cond ((atom lst) (null lst))
    (t (and (pseudo-runep (car lst)) (pseudo-theoryp1 (cdr lst))))))

(defun pseudo-standard-theoriesp
  (val)
  (case-match val
    ((r-unv r-fn1 r-fn2 r-fn3) (and (pseudo-theoryp1 r-unv)
        (pseudo-theoryp1 r-fn1)
        (pseudo-theoryp1 r-fn2)
        (pseudo-theoryp1 r-fn3)))
    (& nil)))

(defun pseudo-current-theoryp (val) (pseudo-theoryp1 val))

(defun pseudo-augmented-theoryp
  (lst)
  (cond ((atom lst) (null lst))
    (t (and (consp (car lst))
        (pseudo-numep (car (car lst)))
        (pseudo-runep (cdr (car lst)))
        (pseudo-augmented-theoryp (cdr lst))))))

(defun pseudo-current-theory-augmentedp
  (val)
  (pseudo-augmented-theoryp val))

(defun pseudo-current-theory-indexp
  (val)
  (or (pseudo-numep val) (equal val -1)))

(defun pseudo-generalize-rulep
  (x)
  (case-match x
    (('generalize-rule nume formula . rune) (and (pseudo-numep nume)
        (pseudo-termp formula)
        (pseudo-runep rune)))
    (& nil)))

(defun pseudo-generalize-rulesp
  (val)
  (cond ((atom val) (null val))
    (t (and (pseudo-generalize-rulep (car val))
        (pseudo-generalize-rulesp (cdr val))))))

(defun pseudo-clause-processor-rulesp
  (val)
  (cond ((atom val) (null val))
    (t (and (consp (car val))
        (symbolp (car (car val)))
        (pseudo-termp (cdr (car val)))
        (pseudo-clause-processor-rulesp (cdr val))))))

(defun boot-strap-flgp (val) (booleanp val))

(defun boot-strap-pass-2p (val) (booleanp val))

(defun skip-proofs-seenp
  (val)
  (or (null val)
    (and (true-listp val)
      (equal (len val) 2)
      (eq (car val) :include-book)
      (book-name-p (cadr val)))
    (pseudo-event-formp val)))

(defun redef-seenp
  (val)
  (or (null val)
    (and (true-listp val)
      (equal (len val) 2)
      (eq (car val) :include-book)
      (stringp (cadr val)))
    (pseudo-event-formp val)))

(defun cert-replayp
  (val)
  (or (null val)
    (eq val t)
    (and (consp val) (true-listp (cdr val)) (posp (car val)))))

(defun proof-supporters-alistp
  (val)
  (cond ((atom val) (null val))
    (t (and (consp (car val))
        (or (symbolp (caar val)) (symbol-listp (caar val)))
        (cdar val)
        (symbol-listp (cdar val))
        (proof-supporters-alistp (cdr val))))))

(defun pseudo-free-var-runes-allp
  (val)
  (pseudo-theoryp1 val))

(defun pseudo-free-var-runes-oncep
  (val)
  (pseudo-theoryp1 val))

(defun weak-translate-cert-data-record-listp
  (lst)
  (cond ((atom lst) (null lst))
    (t (and (weak-translate-cert-data-record-p (car lst))
        (weak-translate-cert-data-record-listp (cdr lst))))))

(defun pseudo-translate-cert-datap
  (val)
  (cond ((atom val) (null val))
    (t (and (consp (car val))
        (symbolp (caar val))
        (weak-translate-cert-data-record-listp (cdar val))
        (pseudo-translate-cert-datap (cdr val))))))

(defun chk-new-name-lstp (val) (symbol-listp val))

(defun pseudo-tau-pairp
  (sym val)
  (declare (xargs :guard (symbolp sym)))
  (cond (sym (and (consp val) (natp (car val)) (eq (cdr val) sym)))
    (t (and (consp val) (rationalp (car val)) (symbolp (cdr val))))))

(defun pseudo-tau-pairp-listp
  (lst)
  (cond ((atom lst) (equal lst nil))
    (t (and (consp (car lst))
        (pseudo-tau-pairp nil (car lst))
        (pseudo-tau-pairp-listp (cdr lst))))))

(defun indexed-pairs-ordered-strictly-descendingp
  (lst)
  (declare (xargs :guard (pseudo-tau-pairp-listp lst)))
  (cond ((endp lst) t)
    ((endp (cdr lst)) t)
    ((> (car (car lst)) (car (cadr lst))) (indexed-pairs-ordered-strictly-descendingp (cdr lst)))
    (t nil)))

(defun pseudo-tau-pairsp
  (x)
  (and (pseudo-tau-pairp-listp x)
    (indexed-pairs-ordered-strictly-descendingp x)))

(defun pseudo-evg-singletonp
  (x)
  (and (consp x) (null (cdr x))))

(defun pseudo-evg-singletonsp1
  (lst)
  (cond ((atom lst) (equal lst nil))
    (t (and (pseudo-evg-singletonp (car lst))
        (pseudo-evg-singletonsp1 (cdr lst))))))

(defun lexorder-strict-ascendingp-without-list-nil
  (lst)
  (cond ((atom lst) t)
    ((atom (cdr lst)) t)
    ((lexorder (cadr lst) (car lst)) nil)
    (t (lexorder-strict-ascendingp-without-list-nil (cdr lst)))))

(defun pseudo-evg-singletonsp
  (lst)
  (and (pseudo-evg-singletonsp1 lst)
    (lexorder-strict-ascendingp-without-list-nil (if (equal (car lst) '(nil))
        (cdr lst)
        lst))))

(defun pseudo-tau-intervalp
  (x)
  (cond ((eq x nil) t)
    ((and (consp x)
       (consp (cdr x))
       (consp (car (cdr x)))
       (consp (cdr (cdr x)))) (let ((dom (car x)) (lo-rel (car (cadr x)))
          (lo (cdr (cadr x)))
          (hi-rel (car (cddr x)))
          (hi (cdr (cddr x))))
        (and (or (eq dom 'integerp)
            (eq dom 'rationalp)
            (eq dom 'acl2-numberp)
            (null dom))
          (if (eq dom 'integerp)
            (and (null lo-rel)
              (or (null lo) (integerp lo))
              (null hi-rel)
              (or (null hi) (integerp hi)))
            (and (booleanp lo-rel)
              (or (null lo) (rationalp lo))
              (booleanp hi-rel)
              (or (null hi) (rationalp hi)))))))
    (t nil)))

(defun pseudo-taup
  (x)
  (cond ((atom x) (equal x nil))
    ((atom (car x)) (and (equal (car x) nil)
        (if (consp (cdr x))
          (and (pseudo-tau-intervalp (cadr x))
            (cond ((atom (cddr x)) (equal (cddr x) nil))
              (t (and (pseudo-tau-pairsp (car (cddr x)))
                  (pseudo-tau-pairsp (cdr (cddr x)))))))
          (equal (cdr x) nil))))
    (t (and (and (or (null (car (car x)))
            (pseudo-evg-singletonp (car (car x))))
          (pseudo-evg-singletonsp (cdr (car x))))
        (if (consp (cdr x))
          (and (pseudo-tau-intervalp (cadr x))
            (cond ((atom (cddr x)) (equal (cddr x) nil))
              (t (and (pseudo-tau-pairsp (car (cddr x)))
                  (pseudo-tau-pairsp (cdr (cddr x)))))))
          (equal (cdr x) nil))))))

(defun pseudo-taup-listp
  (x)
  (cond ((atom x) (equal x nil))
    (t (and (pseudo-taup (car x)) (pseudo-taup-listp (cdr x))))))

(defun pseudo-tau-conjunctive-rulesp
  (val)
  (pseudo-taup-listp val))

(defun pseudo-runep-listp
  (val)
  (cond ((atom val) (equal val nil))
    (t (and (pseudo-runep (car val))
        (pseudo-runep-listp (cdr val))))))

(defun ttags-seenp
  (val)
  (cond ((atom val) (null val))
    (t (and (consp (car val))
        (symbolp (car (car val)))
        (true-listp (cdr (car val)))
        (book-name-listp (remove1-eq 'nil (cdr (car val))))
        (ttags-seenp (cdr val))))))

(defun well-formedness-guaranteep
  (x)
  (and (consp x)
    (symbol-listp (car x))
    (or (equal (len (car x)) 3) (equal (len (car x)) 5))
    (arity-alistp (cdr x))))

(defun well-formedness-guarantee-listp
  (lst)
  (if (atom lst)
    (eq lst nil)
    (and (well-formedness-guaranteep (car lst))
      (well-formedness-guarantee-listp (cdr lst)))))

(defun never-untouchable-fnsp
  (val)
  (if (atom val)
    (eq val nil)
    (and (consp (car val))
      (symbolp (car (car val)))
      (well-formedness-guarantee-listp (cdr (car val)))
      (never-untouchable-fnsp (cdr val)))))

(defun untouchable-fnsp (val) (symbol-listp val))

(defun untouchable-varsp (val) (symbol-listp val))

(defun never-irrelevant-fns-alistp
  (val)
  (and (symbol-alistp val)
    (subsetp-eq (strip-cdrs val) '(t nil :both))))

(defun pseudo-defined-hereditarily-constrained-fnsp
  (val)
  (pseudo-function-symbol-listp val nil))

(defun world-globalsp (val) (symbol-listp val))

(defun lambda$-alistp (val) (alistp val))

(defun loop$-alistp (val) (alistp val))

(defun common-lisp-compliant-lambdasp
  (val)
  (true-listp val))

(defun pseudo-loop-stopper-elementp
  (x)
  (case-match x
    ((var1 var2 . fns) (and (symbolp var1)
        (symbolp var2)
        (pseudo-function-symbol-listp fns nil)))
    (& nil)))

(defun pseudo-loop-stopperp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-loop-stopper-elementp (car x))
        (pseudo-loop-stopperp (cdr x))))))

(defun nil-or-nat-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (or (null (car x)) (natp (car x)))
        (nil-or-nat-listp (cdr x))))))

(defun pseudo-match-freep
  (x)
  (or (null x) (eq x :once) (eq x :all)))

(defun pseudo-rewrite-quoted-constant-rulep
  (x)
  (case-match x
    (('rewrite-rule rune
       nume
       hyps
       equiv
       lhs
       rhs
       subclass
       heuristic-info
       backchain-limit-lst
       var-info . match-free) (cond ((eq subclass 'rewrite-quoted-constant) (and (pseudo-runep rune)
            (pseudo-numep nume)
            (pseudo-term-listp hyps)
            (pseudo-function-symbolp equiv 2)
            (pseudo-termp lhs)
            (pseudo-termp rhs)
            (consp heuristic-info)
            (integerp (car heuristic-info))
            (<= 1 (car heuristic-info))
            (<= (car heuristic-info) 3)
            (pseudo-loop-stopperp (cdr heuristic-info))
            (or (null backchain-limit-lst)
              (nil-or-nat-listp backchain-limit-lst))
            (booleanp var-info)
            (pseudo-match-freep match-free)))
        (t nil)))
    (& nil)))

(defun pseudo-rewrite-quoted-constant-rulesp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-rewrite-quoted-constant-rulep (car x))
        (pseudo-rewrite-quoted-constant-rulesp (cdr x))))))

(defun pseudo-evaluator-check-inputs-p
  (val)
  (true-listp val))

(defun absolute-event-numberp
  (sym val)
  (declare (ignore sym))
  (natp val))

(defun absstobj-infop
  (val)
  (and (weak-absstobj-info-p val)
    (symbolp (access absstobj-info val :st$c))
    (let ((absstobj-tuples (access absstobj-info val :absstobj-tuples)))
      (and (symbol-alistp absstobj-tuples)
        (let ((cdrs (strip-cdrs absstobj-tuples)))
          (and (symbol-alistp cdrs)
            (let ((cddrs (strip-cdrs cdrs)))
              (and (symbol-alistp cddrs) (r-symbol-alistp cddrs)))))))))

(defun accessor-namesp (sym val) (array1p sym val))

(defun attachment-propertyp
  (sym val)
  (declare (ignore sym))
  (or (pseudo-function-symbolp val nil)
    (and (consp val)
      (eq (car val) :attachment-disallowed)
      (or (symbolp (cdr val)) (symbol-alistp (cdr val))))
    (symbol-alistp val)))

(defun pseudo-big-switchp
  (sym val)
  (declare (ignore sym))
  (and (true-listp val)
    (equal (len val) 5)
    (eq (car val) 'big-switch-rule)
    (let ((formals (nth 1 val)) (switch-var (nth 2 val))
        (switch-var-pos (nth 3 val))
        (body (nth 4 val)))
      (and (pseudo-arglistp formals)
        (natp switch-var-pos)
        (< switch-var-pos (length formals))
        (equal (nth switch-var-pos formals) switch-var)
        (pseudo-termp body)))))

(defun tau-interval-domainsp
  (x)
  (cond ((atom x) (eq x nil))
    (t (and (member-eq (car x) '(integerp rationalp acl2-numberp nil))
        (tau-interval-domainsp (cdr x))))))

(defun tau-interval-domainsp-listp
  (x)
  (cond ((atom x) (eq x nil))
    (t (and (tau-interval-domainsp (car x))
        (tau-interval-domainsp-listp (cdr x))))))

(defun pseudo-bounder-correctnessp
  (sym x)
  (and (consp x)
    (consp (car x))
    (consp (cdr x))
    (symbolp (car (car x)))
    (tau-interval-domainsp-listp (cdr (car x)))
    (eq sym (car (car x)))
    (symbolp (car (cdr x)))
    (nat-listp (cdr (cdr x)))))

(defun pseudo-tau-boundersp
  (sym val)
  (cond ((atom val) (eq val nil))
    (t (and (pseudo-bounder-correctnessp sym (car val))
        (pseudo-tau-boundersp sym (cdr val))))))

(defun pseudo-tau-boundersp-listp
  (sym val)
  (cond ((atom val) (eq val nil))
    (t (and (pseudo-tau-boundersp sym (car val))
        (pseudo-tau-boundersp-listp sym (cdr val))))))

(defun classesp
  (sym val)
  (declare (ignore sym))
  (keyword-to-keyword-value-list-alistp val))

(defun classicalpp
  (sym val)
  (declare (ignore sym))
  (booleanp val))

(defun clause-processorp
  (sym val)
  (declare (ignore sym))
  (or (booleanp val) (well-formedness-guaranteep val)))

(defun coarseningsp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbol-listp val 2))

(defun concrete-stobjp
  (sym val)
  (declare (ignore sym))
  (symbolp val))

(defun pseudo-congruence-rulep
  (x)
  (case-match x
    ((nume equiv . rune) (and (pseudo-numep nume)
        (pseudo-function-symbolp equiv 2)
        (pseudo-runep rune)))
    (& nil)))

(defun pseudo-congruence-rule-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-congruence-rulep (car x))
        (pseudo-congruence-rule-listp (cdr x))))))

(defun pseudo-congruence-rule-list-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-congruence-rule-listp (car x))
        (pseudo-congruence-rule-list-listp (cdr x))))))

(defun pseudo-congruence-tuplep
  (x)
  (or (null x)
    (and (consp x)
      (pseudo-function-symbolp (car x) 2)
      (pseudo-congruence-rule-list-listp (cdr x)))))

(defun pseudo-congruence-tuple-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-congruence-tuplep (car x))
        (pseudo-congruence-tuple-listp (cdr x))))))

(defun congruencesp
  (sym val)
  (declare (ignore sym))
  (pseudo-congruence-tuple-listp val))

(defun pseudo-pequiv-pattern-p
  (p)
  (or (legal-variablep p)
    (and (weak-pequiv-pattern-p p)
      (symbolp (access pequiv-pattern p :fn))
      (pseudo-term-listp (access pequiv-pattern p :pre-rev))
      (pseudo-term-listp (access pequiv-pattern p :post))
      (eql (access pequiv-pattern p :posn)
        (1+ (length (access pequiv-pattern p :pre-rev))))
      (pseudo-pequiv-pattern-p (access pequiv-pattern p :next)))))

(defun pseudo-pequiv-p
  (x)
  (and (weak-pequiv-p x)
    (pseudo-pequiv-pattern-p (access pequiv x :pattern))
    (alistp (access pequiv x :unify-subst))
    (pseudo-congruence-rulep (access pequiv x :congruence-rule))))

(defun pseudo-pequiv-listp
  (lst)
  (cond ((atom lst) (null lst))
    (t (and (pseudo-pequiv-p (car lst))
        (pseudo-pequiv-listp (cdr lst))))))

(defun pseudo-pequiv-alistp
  (alist)
  (cond ((atom alist) (null alist))
    (t (and (consp (car alist))
        (symbolp (caar alist))
        (pseudo-pequiv-listp (cdar alist))
        (pseudo-pequiv-alistp (cdr alist))))))

(defun pequivsp
  (sym val)
  (declare (ignore sym))
  (or (null val)
    (and (weak-pequivs-property-p val)
      (pseudo-pequiv-alistp (access pequivs-property val :deep))
      (pseudo-pequiv-alistp (access pequivs-property val :shallow)))))

(defun congruent-stobj-repp
  (sym val)
  (declare (ignore sym))
  (symbolp val))

(defun const-propertyp
  (sym val)
  (declare (ignore sym val))
  t)

(defun pseudo-constrainedpp
  (sym val)
  (declare (ignore sym))
  (or (booleanp val)
    (eq val *unknown-constraints*)
    (weak-transparent-rec-p val)))

(defun pseudo-controller-alistp
  (alist)
  (cond ((atom alist) (null alist))
    ((and (consp (car alist))
       (pseudo-function-symbolp (caar alist) nil)
       (boolean-listp (cdar alist))) (pseudo-controller-alistp (cdr alist)))
    (t nil)))

(defun pseudo-def-bodyp
  (x)
  (case-match x
    (((nume hyp . concl) equiv
       recursivep
       formals
       rune . controller-alist) (and (pseudo-numep nume)
        (or (null hyp) (pseudo-termp hyp))
        (pseudo-termp concl)
        (and (symbolp equiv) equiv)
        (pseudo-function-symbol-listp recursivep nil)
        (pseudo-arglistp formals)
        (pseudo-runep rune)
        (pseudo-controller-alistp controller-alist)))
    (& nil)))

(defun pseudo-def-body-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-def-bodyp (car x))
        (pseudo-def-body-listp (cdr x))))))

(defun pseudo-def-bodiesp
  (sym val)
  (declare (ignore sym))
  (pseudo-def-body-listp val))

(defun defaxiom-supporterp
  (sym val)
  (declare (ignore sym))
  (symbolp val))

(defun pseudo-defchoose-axiomp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun pseudo-elim-rulep
  (x)
  (case-match x
    (('elim-rule ((nume . crucial-position) destructor-term . destructor-terms)
       (hyps . equiv)
       (lhs . rhs) . rune) (and (pseudo-numep nume)
        (natp crucial-position)
        (pseudo-termp destructor-term)
        (pseudo-term-listp destructor-terms)
        (pseudo-term-listp hyps)
        (pseudo-function-symbolp equiv 2)
        (pseudo-termp lhs)
        (symbolp rhs)
        (pseudo-runep rune)
        (consp destructor-term)
        (< crucial-position (len (cdr destructor-term)))
        (equal rhs (nth crucial-position (cdr destructor-term)))))
    (& nil)))

(defun pseudo-eliminate-destructors-rules
  (sym val)
  (declare (irrelevant sym))
  (cond ((atom val) (null val))
    (t (and (pseudo-elim-rulep (car val))
        (pseudo-eliminate-destructors-rules sym (cdr val))))))

(defun pseudo-formalsp
  (sym val)
  (declare (ignore sym))
  (pseudo-arglistp val))

(defun pseudo-forward-chaining-rulep
  (x)
  (case-match x
    (('forward-chaining-rule (rune . nume)
       trigger
       hyps
       concls . match-free) (and (pseudo-runep rune)
        (pseudo-numep nume)
        (pseudo-termp trigger)
        (pseudo-term-listp hyps)
        (pseudo-term-listp concls)
        (pseudo-match-freep match-free)))
    (& nil)))

(defun pseudo-forward-chaining-rule-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-forward-chaining-rulep (car x))
        (pseudo-forward-chaining-rule-listp (cdr x))))))

(defun pseudo-forward-chaining-rulesp
  (sym val)
  (declare (ignore sym))
  (pseudo-forward-chaining-rule-listp val))

(defun stobj-listp
  (x known-stobjs w)
  (declare (xargs :guard (and (plist-worldp w)
        (or (eq known-stobjs t) (true-listp known-stobjs)))))
  (cond ((atom x) (null x))
    (t (and (stobjp (car x) known-stobjs w)
        (stobj-listp (cdr x) known-stobjs w)))))

(defun global-stobjs-p
  (val w)
  (declare (xargs :guard (plist-worldp w)))
  (or (null val)
    (and (consp val)
      (stobj-listp (car val) t w)
      (stobj-listp (cdr val) t w)
      (not (intersectp-eq (car val) (cdr val))))))

(defun pseudo-global-valuep
  (sym val w)
  (declare (xargs :guard (plist-worldp w)))
  (case sym
    (event-landmark (pseudo-event-landmarkp val))
    (command-landmark (pseudo-command-landmarkp val))
    (known-package-alist (known-package-alistp val))
    (well-founded-relation-alist (pseudo-well-founded-relation-alistp val))
    (built-in-clauses (pseudo-built-in-clausesp val))
    (attach-nil-lst (pseudo-attach-nil-lst val))
    (attachment-records (pseudo-attachment-recordsp val))
    (attachments-at-ground-zero (pseudo-attachments-at-ground-zerop val))
    (half-length-built-in-clauses (pseudo-half-length-built-in-clausesp val))
    (type-set-inverter-rules (pseudo-type-set-inverter-rulesp val))
    (global-arithmetic-enabled-structure (pseudo-global-arithmetic-enabled-structurep val))
    (operating-system (operating-systemp val))
    (event-index (pseudo-event-indexp val w))
    (command-index (pseudo-command-indexp val w))
    (event-number-baseline (event-number-baselinep val))
    (command-number-baseline-info (command-number-baseline-infop val))
    (embedded-event-lst (pseudo-embedded-event-lstp val))
    (cltl-command (pseudo-cltl-commandp val))
    (top-level-cltl-command-stack (pseudo-cltl-command-listp val))
    (include-book-alist (pseudo-include-book-alistp val))
    (include-book-alist-all (pseudo-include-book-alist-allp val))
    (pcert-books (pseudo-pcert-booksp val))
    (include-book-path (pseudo-include-book-pathp val))
    (certification-tuple (certification-tuplep val))
    (proved-functional-instances-alist (proved-functional-instances-alistp val))
    (nonconstructive-axiom-names (nonconstructive-axiom-namesp val))
    (standard-theories (pseudo-standard-theoriesp val))
    (current-theory (pseudo-current-theoryp val))
    (current-theory-length (natp val))
    (current-theory-augmented (pseudo-current-theory-augmentedp val))
    (current-theory-index (pseudo-current-theory-indexp val))
    (generalize-rules (pseudo-generalize-rulesp val))
    (clause-processor-rules (pseudo-clause-processor-rulesp val))
    (boot-strap-flg (boot-strap-flgp val))
    (boot-strap-pass-2 (boot-strap-pass-2p val))
    (skip-proofs-seen (skip-proofs-seenp val))
    (redef-seen (redef-seenp val))
    (cert-replay (cert-replayp val))
    (proof-supporters-alist (proof-supporters-alistp val))
    (free-var-runes-all (pseudo-free-var-runes-allp val))
    (free-var-runes-once (pseudo-free-var-runes-oncep val))
    (translate-cert-data (pseudo-translate-cert-datap val))
    (chk-new-name-lst (chk-new-name-lstp val))
    (tau-conjunctive-rules (pseudo-tau-conjunctive-rulesp val))
    (tau-next-index (natp val))
    (tau-runes (pseudo-runep-listp val))
    (tau-mv-nth-synonyms (pseudo-function-symbol-listp val nil))
    (tau-lost-runes (pseudo-runep-listp val))
    (ttags-seen (ttags-seenp val))
    (never-untouchable-fns (never-untouchable-fnsp val))
    (untouchable-fns (untouchable-fnsp val))
    (untouchable-vars (untouchable-varsp val))
    (defined-hereditarily-constrained-fns (pseudo-defined-hereditarily-constrained-fnsp val))
    (world-globals (world-globalsp val))
    (lambda$-alist (lambda$-alistp val))
    (loop$-alist (loop$-alistp val))
    (common-lisp-compliant-lambdas (common-lisp-compliant-lambdasp val))
    (never-irrelevant-fns-alist (never-irrelevant-fns-alistp val))
    (rewrite-quoted-constant-rules (pseudo-rewrite-quoted-constant-rulesp val))
    (project-dir-alist (and (alistp val)
        (keyword-listp (strip-cars val))
        (string-listp (strip-cdrs val))))
    (projects/apply/base-includedp (booleanp val))
    (evaluator-check-inputs (pseudo-evaluator-check-inputs-p val))
    (ext-gens (symbol-listp val))
    (ext-gen-barriers (pseudo-function-symbol-listp val nil))
    (otherwise nil)))

(defun pseudo-guardp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun pseudo-hereditarily-constrained-fnnamesp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbol-listp val nil))

(defun pseudo-induction-machinep
  (sym val)
  (declare (ignore sym))
  (pseudo-tests-and-calls-listp val))

(defun pseudo-induction-rulep
  (x)
  (case-match x
    (('induction-rule nume (pattern . condition) scheme . rune) (and (pseudo-numep nume)
        (pseudo-termp pattern)
        (pseudo-term-listp condition)
        (pseudo-termp scheme)
        (pseudo-runep rune)))
    (& nil)))

(defun pseudo-induction-rule-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-induction-rulep (car x))
        (pseudo-induction-rule-listp (cdr x))))))

(defun pseudo-induction-rulesp
  (sym val)
  (declare (ignore sym))
  (pseudo-induction-rule-listp val))

(defun pseudo-ruler-extendersp
  (x)
  (or (eq x :all) (pseudo-function-symbol-listp x nil)))

(defun pseudo-justificationp
  (sym val)
  (declare (ignore sym))
  (case-match val
    (('justification subset
       (subversive-p mp . rel)
       (measure . ruler-extenders)) (and (pseudo-arglistp subset)
        (booleanp subversive-p)
        (pseudo-function-symbolp mp 1)
        (pseudo-function-symbolp rel 2)
        (pseudo-termp measure)
        (pseudo-ruler-extendersp ruler-extenders)))
    (& nil)))

(defun labelp
  (sym val)
  (declare (ignore sym))
  (symbolp val))

(defun pseudo-rewrite-rulep
  (x)
  (case-match x
    (('rewrite-rule rune
       nume
       hyps
       equiv
       lhs
       rhs
       subclass
       heuristic-info
       backchain-limit-lst
       var-info . match-free) (case subclass
        (backchain (and (pseudo-runep rune)
            (pseudo-numep nume)
            (pseudo-term-listp hyps)
            (pseudo-function-symbolp equiv 2)
            (pseudo-termp lhs)
            (pseudo-termp rhs)
            (pseudo-loop-stopperp heuristic-info)
            (or (null backchain-limit-lst)
              (nil-or-nat-listp backchain-limit-lst))
            (booleanp var-info)
            (pseudo-match-freep match-free)))
        (abbreviation (and (pseudo-runep rune)
            (pseudo-numep nume)
            (null hyps)
            (pseudo-function-symbolp equiv 2)
            (pseudo-termp lhs)
            (pseudo-termp rhs)
            (null heuristic-info)
            (null backchain-limit-lst)
            (booleanp var-info)
            (null match-free)))
        (meta (and (pseudo-runep rune)
            (pseudo-numep nume)
            (or (null hyps) (pseudo-function-symbolp hyps 1))
            (pseudo-function-symbolp equiv 2)
            (pseudo-function-symbolp lhs 1)
            (or (null rhs) (eq rhs 'extended))
            (or (null heuristic-info)
              (well-formedness-guaranteep heuristic-info))
            (or (null backchain-limit-lst) (natp backchain-limit-lst))
            (null match-free)))
        (definition (and (pseudo-runep rune)
            (pseudo-numep nume)
            (pseudo-term-listp hyps)
            (pseudo-function-symbolp equiv 2)
            (pseudo-termp lhs)
            (pseudo-termp rhs)
            (and (consp heuristic-info)
              (pseudo-function-symbol-listp (car heuristic-info) nil)
              (pseudo-controller-alistp (cdr heuristic-info)))
            (null backchain-limit-lst)
            (integer-listp var-info)
            (null match-free)))
        (otherwise nil)))
    (& nil)))

(defun pseudo-rewrite-rule-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-rewrite-rulep (car x))
        (pseudo-rewrite-rule-listp (cdr x))))))

(defun pseudo-lemmasp
  (sym val)
  (declare (ignore sym))
  (pseudo-rewrite-rule-listp val))

(defun level-nop
  (sym val)
  (declare (ignore sym))
  (natp val))

(defun pseudo-linear-lemmap
  (x)
  (case-match x
    (('linear-lemma (nume . hyps)
       max-term
       concl
       backchain-limit-lst
       rune . match-free) (and (pseudo-numep nume)
        (pseudo-term-listp hyps)
        (pseudo-termp max-term)
        (pseudo-termp concl)
        (or (null backchain-limit-lst)
          (nil-or-nat-listp backchain-limit-lst))
        (pseudo-runep rune)
        (pseudo-match-freep match-free)))
    (& nil)))

(defun pseudo-linear-lemma-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-linear-lemmap (car x))
        (pseudo-linear-lemma-listp (cdr x))))))

(defun pseudo-linear-lemmasp
  (sym val)
  (declare (ignore sym))
  (pseudo-linear-lemma-listp val))

(defun loop$-recursionp
  (sym val)
  (declare (ignore sym))
  (booleanp val))

(defun hint-for-macro-arglist-keysp
  (args passed1 passed2)
  (declare (xargs :verify-guards nil))
  (cond ((endp args) (list passed1 passed2))
    (t (cons (hint-for-macro-arglist-keysp (cdr args)
          (cons (intern (symbol-name (car args)) "KEYWORD") passed1)
          (cons (intern (symbol-name (car args)) "KEYWORD") passed2))
        (hint-for-macro-arglist-keysp (cdr args)
          (cons (cond ((symbolp (caar args)) (intern (symbol-name (caar args)) "KEYWORD"))
              (t (car (caar args))))
            passed1)
          (cons (cond ((symbolp (caar args)) (intern (symbol-name (caar args)) "KEYWORD"))
              (t (car (caar args))))
            passed2))))))

(defun pseudo-macro-arglist-msgp
  (args)
  (and (macro-args-structurep args)
    (pseudo-arglistp (macro-vars args))))

(defun pseudo-macro-argsp
  (sym val)
  (declare (ignore sym))
  (pseudo-macro-arglist-msgp val))

(defun pseudo-macro-bodyp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun pseudo-neg-implicantsp
  (sym val)
  (declare (ignore sym))
  (pseudo-taup val))

(defun non-executablepp
  (sym val)
  (declare (ignore sym))
  (or (eq val :program) (booleanp val)))

(defun non-memoizablep
  (sym val)
  (declare (ignore sym))
  (booleanp val))

(defun pseudo-pos-implicantsp
  (sym val)
  (declare (ignore sym))
  (pseudo-taup val))

(defun predefinedp
  (sym val)
  (declare (ignore sym))
  (booleanp val))

(defun primitive-recursive-defunpp
  (sym val)
  (declare (ignore sym))
  (booleanp val))

(defun pseudo-quick-block-info-listp
  (lst)
  (cond ((atom lst) (null lst))
    (t (and (member-eq (car lst)
          '(questionable unchanging self-reflexive))
        (pseudo-quick-block-info-listp (cdr lst))))))

(defun pseudo-quick-block-infop
  (sym val)
  (declare (ignore sym))
  (pseudo-quick-block-info-listp val))

(defun pseudo-recognizer-tuplep
  (fn x)
  (case-match x
    ((!fn (nume . true-ts) (false-ts . strongp) . rune) (and (pseudo-function-symbolp fn 1)
        (or (null nume) (pseudo-numep nume))
        (type-setp true-ts)
        (type-setp false-ts)
        (booleanp strongp)
        (pseudo-runep rune)))
    (& nil)))

(defun pseudo-recognizer-alistp
  (fn x)
  (if (atom x)
    (null x)
    (and (pseudo-recognizer-tuplep fn (car x))
      (pseudo-recognizer-alistp fn (cdr x)))))

(defun pseudo-recursivepp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbol-listp val nil))

(defun redefinedp
  (sym val)
  (declare (ignore sym))
  (case-match val
    ((renewal-mode . insig) (and (member-eq renewal-mode
          '(:erase :overwrite :reclassifying-overwrite))
        (or (null insig) (pseudo-internal-signaturep insig))))
    (& nil)))

(defun pseudo-integer-boundp
  (x)
  (or (integerp x)
    (eq x '*)
    (and (consp x) (integerp (car x)) (null (cdr x)))))

(defun pseudo-rational-boundp
  (x)
  (or (integerp x)
    (eq x '*)
    (and (consp x) (rationalp (car x)) (null (cdr x)))))

(defun pseudo-type-specp
  (x)
  (cond ((or (eq x 'integer) (eq x 'signed-byte)) t)
    ((and (consp x)
       (eq (car x) 'integer)
       (true-listp x)
       (equal (length x) 3)) (and (pseudo-integer-boundp (cadr x))
        (pseudo-integer-boundp (caddr x))))
    ((eq x 'rational) t)
    ((eq x 'real) t)
    ((eq x 'complex) t)
    ((and (consp x)
       (or (eq (car x) 'rational) (eq (car x) 'real))
       (true-listp x)
       (equal (length x) 3)) (and (pseudo-rational-boundp (cadr x))
        (pseudo-rational-boundp (caddr x))))
    ((eq x 'bit) t)
    ((and (consp x)
       (eq (car x) 'mod)
       (true-listp x)
       (equal (length x) 2)
       (integerp (cadr x))) t)
    ((and (consp x)
       (eq (car x) 'signed-byte)
       (true-listp x)
       (equal (length x) 2)
       (integerp (cadr x))
       (> (cadr x) 0)) t)
    ((eq x 'unsigned-byte) t)
    ((and (consp x)
       (eq (car x) 'unsigned-byte)
       (true-listp x)
       (equal (length x) 2)
       (integerp (cadr x))
       (> (cadr x) 0)) t)
    ((eq x 'atom) t)
    ((eq x 'character) t)
    ((eq x 'cons) t)
    ((eq x 'list) t)
    ((eq x 'nil) t)
    ((eq x 'null) t)
    ((eq x 'ratio) t)
    ((eq x 'standard-char) t)
    ((eq x 'string) t)
    ((and (consp x)
       (eq (car x) 'string)
       (true-listp x)
       (equal (length x) 2)
       (integerp (cadr x))
       (>= (cadr x) 0)) t)
    ((eq x 'symbol) t)
    ((eq x 't) t)
    ((weak-satisfies-type-spec-p x) t)
    ((and (consp x) (eq (car x) 'member) (eqlable-listp (cdr x))) t)
    (t nil)))

(defun pseudo-array1-type-specp
  (x)
  (case-match x
    (('array type-spec (max)) (and (pseudo-type-specp type-spec) (natp max)))
    (& nil)))

(defun pseudo-stobj-field-descriptor-keyword-pairp
  (key val)
  (cond ((eq key :type) (or (pseudo-type-specp val) (pseudo-array1-type-specp val)))
    ((eq key :initially) t)
    ((eq key :resizable) (booleanp val))
    (t nil)))

(defun pseudo-stobj-field-descriptor-keyword-alistp
  (x)
  (cond ((atom x) t)
    ((atom (cdr x)) nil)
    (t (and (pseudo-stobj-field-descriptor-keyword-pairp (car x)
          (cadr x))
        (pseudo-stobj-field-descriptor-keyword-alistp (cddr x))))))

(defun pseudo-stobj-field-descriptorp
  (x)
  (or (pseudo-function-symbolp x nil)
    (and (true-listp x)
      (consp x)
      (pseudo-function-symbolp (car x) nil)
      (pseudo-stobj-field-descriptor-keyword-alistp (cdr x)))))

(defun pseudo-stobj-field-descriptor-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-stobj-field-descriptorp (car x))
        (pseudo-stobj-field-descriptor-listp (cdr x))))))

(defun pseudo-doublet-style-renaming-alistp
  (x)
  (cond ((atom x) (null x))
    (t (and (consp (car x))
        (symbolp (car (car x)))
        (consp (cdr (car x)))
        (symbolp (cadr (car x)))
        (null (cddr (car x)))
        (pseudo-doublet-style-renaming-alistp (cdr x))))))

(defun pseudo-redundancy-bundlep
  (sym val)
  (declare (ignore sym))
  (case-match val
    ((field-descriptors . renaming-alist) (and (pseudo-stobj-field-descriptor-listp field-descriptors)
        (pseudo-doublet-style-renaming-alistp renaming-alist)))
    (& nil)))

(defun pseudo-runic-mapping-pairs-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (consp (car x))
        (pseudo-numep (car (car x)))
        (pseudo-runep (cdr (car x)))
        (pseudo-runic-mapping-pairs-listp (cdr x))))))

(defun pseudo-runic-mapping-pairsp
  (sym val)
  (declare (ignore sym))
  (pseudo-runic-mapping-pairs-listp val))

(defun siblings-propertyp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbol-listp val nil))

(defun pseudo-signaturep
  (x)
  (and (true-listp x)
    (equal (len x) 4)
    (let ((inputs-tau-list (nth 0 x)) (vars-and-dependent-hyps (nth 1 x))
        (output-sign (nth 2 x))
        (output-recog (nth 3 x)))
      (and (pseudo-taup-listp inputs-tau-list)
        (consp vars-and-dependent-hyps)
        (symbol-listp (car vars-and-dependent-hyps))
        (no-duplicatesp-eq (car vars-and-dependent-hyps))
        (pseudo-term-listp (cdr vars-and-dependent-hyps))
        (booleanp output-sign)
        (or (pseudo-tau-pairp nil output-recog)
          (pseudo-evg-singletonp output-recog))))))

(defun pseudo-signaturep-listp
  (x)
  (cond ((atom x) (equal x nil))
    (t (and (pseudo-signaturep (car x))
        (pseudo-signaturep-listp (cdr x))))))

(defun pseudo-signature-rules-form-1p
  (sym val)
  (declare (ignore sym))
  (pseudo-signaturep-listp val))

(defun pseudo-signaturep-listp-listp
  (x)
  (cond ((atom x) (equal x nil))
    (t (and (pseudo-signaturep-listp (car x))
        (pseudo-signaturep-listp-listp (cdr x))))))

(defun pseudo-signature-rules-form-2p
  (sym val)
  (declare (ignore sym))
  (pseudo-signaturep-listp-listp val))

(defun pseudo-split-types-termp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun pseudo-invariant-riskp
  (sym val)
  (declare (ignore sym val))
  t)

(defun pseudo-stobjp
  (sym val)
  (if (eq sym 'state)
    (equal val '(*the-live-state*))
    (or (null val) (weak-stobj-property-p val))))

(defun pseudo-stobj-constantp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbolp val nil))

(defun pseudo-stobj-functionp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbolp val nil))

(defun pseudo-stobj-live-varp
  (sym val)
  (declare (ignore sym))
  (pseudo-function-symbolp val nil))

(defun pseudo-stobjs-inp
  (sym val)
  (declare (ignore sym))
  (symbol-listp val))

(defun pseudo-stobjs-outp
  (sym val)
  (declare (ignore sym))
  (symbol-listp val))

(defun symbol-classp
  (sym val)
  (declare (ignore sym))
  (member-eq val '(:program :ideal :common-lisp-compliant)))

(defun table-alistp
  (sym val)
  (declare (ignore sym))
  (alistp val))

(defun pseudo-table-guardp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun pseudo-theoremp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun pseudo-theoryp
  (sym lst)
  (declare (ignore sym))
  (pseudo-theoryp1 lst))

(defun pseudo-type-prescriptionp
  (x)
  (case-match x
    ((basic-ts (nume . term)
       (hyps . backchain-limit-lst)
       (vars . rune) . corollary) (and (type-setp basic-ts)
        (or (null nume) (pseudo-numep nume))
        (pseudo-termp term)
        (pseudo-term-listp hyps)
        (or (null backchain-limit-lst)
          (and (backchain-limit-listp backchain-limit-lst)
            (equal (length backchain-limit-lst) (length hyps))))
        (symbol-listp vars)
        (pseudo-runep rune)
        (pseudo-termp corollary)))
    (& nil)))

(defun pseudo-type-prescription-listp
  (x)
  (cond ((atom x) (null x))
    (t (and (pseudo-type-prescriptionp (car x))
        (pseudo-type-prescription-listp (cdr x))))))

(defun pseudo-type-prescriptionsp
  (sym val)
  (declare (ignore sym))
  (pseudo-type-prescription-listp val))

(defun pseudo-unevalable-but-knownp
  (sym val)
  (declare (ignore sym))
  (cond ((atom val) (equal val nil))
    (t (and (consp (car val))
        (booleanp (cdr (car val)))
        (pseudo-unevalable-but-knownp nil (cdr val))))))

(defun unnormalized-bodyp
  (sym val)
  (declare (ignore sym))
  (pseudo-termp val))

(defun untranslated-theoremp
  (sym val)
  (declare (ignore sym))
  (or (atom val) (true-listp val)))

(defun pseudo-good-world-triplep
  (trip w redefp)
  (declare (xargs :guard (plist-worldp w)))
  (cond ((and (consp trip)
       (symbolp (car trip))
       (consp (cdr trip))
       (symbolp (cadr trip))) (let ((sym (car trip)) (prop (cadr trip)) (val (cddr trip)))
        (cond ((and redefp (eq val *acl2-property-unbound*)) t)
          (t (case prop
              (absolute-event-number (or (eq val *acl2-property-unbound*)
                  (absolute-event-numberp sym val)))
              (absstobj-info (absstobj-infop val))
              (accessor-names (accessor-namesp sym val))
              (attachment (attachment-propertyp sym val))
              (big-switch (pseudo-big-switchp sym val))
              (tau-bounders-form-1 (pseudo-tau-boundersp sym val))
              (tau-bounders-form-2 (pseudo-tau-boundersp-listp sym val))
              (classes (classesp sym val))
              (classicalp (or (eq val *acl2-property-unbound*) (classicalpp sym val)))
              (clause-processor (clause-processorp sym val))
              (coarsenings (coarseningsp sym val))
              (concrete-stobj (concrete-stobjp sym val))
              (congruences (congruencesp sym val))
              (congruent-stobj-rep (congruent-stobj-repp sym val))
              (const (const-propertyp sym val))
              (constrainedp (pseudo-constrainedpp sym val))
              (constraint-lst-etc (constraint-lst-etc-p val))
              (def-bodies (or (eq val *acl2-property-unbound*)
                  (pseudo-def-bodiesp sym val)))
              (defaxiom-supporter (defaxiom-supporterp sym val))
              (defchoose-axiom (pseudo-defchoose-axiomp sym val))
              (eliminate-destructors-rules (pseudo-eliminate-destructors-rules sym val))
              (formals (or (eq val *acl2-property-unbound*)
                  (pseudo-formalsp sym val)))
              (forward-chaining-rules (pseudo-forward-chaining-rulesp sym val))
              (global-stobjs (or (eq val *acl2-property-unbound*)
                  (global-stobjs-p val w)))
              (global-value (and (not (eq val *acl2-property-unbound*))
                  (pseudo-global-valuep sym val w)))
              (guard (or (eq val *acl2-property-unbound*)
                  (pseudo-guardp sym val)))
              (hereditarily-constrained-fnnames (pseudo-hereditarily-constrained-fnnamesp sym val))
              (induction-machine (pseudo-induction-machinep sym val))
              (induction-rules (pseudo-induction-rulesp sym val))
              (invariant-risk (or (eq val *acl2-property-unbound*)
                  (pseudo-invariant-riskp sym val)))
              (justification (pseudo-justificationp sym val))
              (label (labelp sym val))
              (lemmas (pseudo-lemmasp sym val))
              (level-no (level-nop sym val))
              (linear-lemmas (pseudo-linear-lemmasp sym val))
              (loop$-recursion (loop$-recursionp sym val))
              (macro-args (pseudo-macro-argsp sym val))
              (macro-body (pseudo-macro-bodyp sym val))
              (neg-implicants (pseudo-neg-implicantsp sym val))
              (non-executablep (or (eq val *acl2-property-unbound*)
                  (non-executablepp sym val)))
              (non-memoizable (non-memoizablep sym val))
              (pequivs (pequivsp sym val))
              (pos-implicants (pseudo-pos-implicantsp sym val))
              (predefined (or (eq val *acl2-property-unbound*) (predefinedp sym val)))
              (primitive-recursive-defunp (primitive-recursive-defunpp sym val))
              (quick-block-info (pseudo-quick-block-infop sym val))
              (recognizer-alist (pseudo-recognizer-alistp sym val))
              (recursivep (pseudo-recursivepp sym val))
              (redefined (redefinedp sym val))
              (runic-mapping-pairs (pseudo-runic-mapping-pairsp sym val))
              (siblings (siblings-propertyp sym val))
              (signature-rules-form-1 (pseudo-signature-rules-form-1p sym val))
              (signature-rules-form-2 (pseudo-signature-rules-form-2p sym val))
              (split-types-term (or (eq val *acl2-property-unbound*)
                  (pseudo-split-types-termp sym val)))
              (stobj (pseudo-stobjp sym val))
              (stobj-constant (pseudo-stobj-constantp sym val))
              (stobj-function (pseudo-stobj-functionp sym val))
              (stobj-live-var (pseudo-stobj-live-varp sym val))
              (stobjs-in (or (eq val *acl2-property-unbound*)
                  (pseudo-stobjs-inp sym val)))
              (stobjs-out (or (eq val *acl2-property-unbound*)
                  (pseudo-stobjs-outp sym val)))
              (symbol-class (or (eq val *acl2-property-unbound*)
                  (symbol-classp sym val)))
              (table-alist (table-alistp sym val))
              (table-guard (pseudo-table-guardp sym val))
              (tau-pair (pseudo-tau-pairp sym val))
              (tau-pair-saved (pseudo-tau-pairp sym val))
              (theorem (pseudo-theoremp sym val))
              (theory (pseudo-theoryp sym val))
              (type-prescriptions (or (eq val *acl2-property-unbound*)
                  (pseudo-type-prescriptionsp sym val)))
              (unevalable-but-known (pseudo-unevalable-but-knownp sym val))
              (unnormalized-body (or (eq val *acl2-property-unbound*)
                  (unnormalized-bodyp sym val)))
              (untranslated-theorem (untranslated-theoremp sym val))
              (otherwise nil))))))
    (t nil)))

(defun pseudo-good-worldp2
  (pos w redefp)
  (declare (xargs :guard (and (natp pos) (plist-worldp w))))
  (cond ((atom w) (null w))
    ((pseudo-good-world-triplep (car w) (cdr w) redefp) (pseudo-good-worldp2 (+ 1 pos) (cdr w) redefp))
    (t (bad-world! 'pseudo-good-worldp2
        "(nth ~x0 ...) is an illegal triple."
        pos))))

(defun pseudo-good-worldp1
  (w redefp)
  (declare (xargs :guard (plist-worldp w)))
  (cond ((atom w) (null w))
    ((pseudo-good-world-triplep (car w) (cdr w) redefp) (pseudo-good-worldp1 (cdr w) redefp))
    (t nil)))

(defun good-command-blocksp1
  (pos just-entered-command-blockp no-event-landmark-yetp w)
  (declare (xargs :guard (and (natp pos) (plist-worldp w))))
  (cond ((atom w) t)
    (t (let ((sym (car (car w))) (prop (cadr (car w)))
          (val (cddr (car w))))
        (cond ((and (eq sym 'command-landmark) (eq prop 'global-value)) (cond (no-event-landmark-yetp (bad-world! 'good-command-blocksp1
                  "Violation of the command blocks invariant, ~
                                   specifically that every block contain at ~
                                   least one EVENT-LANDMARK, was detected at ~
                                   triple ~x0.  The preceding ~
                                   command-landmark, (with no event-landmark ~
                                   found between that one and the one at ~
                                   position ~x0) is:~|~x1"
                  pos
                  no-event-landmark-yetp))
              (t (good-command-blocksp1 (+ 1 pos) t (car w) (cdr w)))))
          ((and (eq sym 'command-index) (eq prop 'global-value)) (cond ((or just-entered-command-blockp (null val)) (good-command-blocksp1 (+ 1 pos)
                  nil
                  no-event-landmark-yetp
                  (cdr w)))
              (t (bad-world! 'good-command-blocksp1
                  "Violation of the command blocks ~
                                     invariant, specifically that every ~
                                     COMMAND-INDEX (except the initializing ~
                                     one) appear immediately after a ~
                                     COMMAND-LANDMARK, was detected at triple ~
                                     ~x0."
                  pos))))
          ((and (eq sym 'event-landmark) (eq prop 'global-value)) (good-command-blocksp1 (+ 1 pos) nil nil (cdr w)))
          (t (good-command-blocksp1 (+ 1 pos)
              nil
              no-event-landmark-yetp
              (cdr w))))))))

(defun good-command-blocksp
  (w)
  (declare (xargs :guard (plist-worldp w)))
  (good-command-blocksp1 0 nil nil w))

(defun sequential-event-landmarksp1
  (pos n w)
  (declare (xargs :guard (and (natp pos) (plist-worldp w))))
  (cond ((atom w) (if (equal n -2)
        (eq w nil)
        (bad-world! 'sequential-event-landmarksp1
          "When we reached the end of the world, n was ~x0 ~
                          instead of -2."
          n)))
    ((and (eq (car (car w)) 'event-landmark)
       (eq (cadr (car w)) 'global-value)) (if (equal n (safe-access-event-tuple-number (cddr (car w))))
        (sequential-event-landmarksp1 (+ 1 pos) (- n 1) (cdr w))
        (bad-world! 'sequential-event-landmarksp
          "Item ~x0 was supposed to be EVENT-LANDMARK ~x1 but ~
                          actually has number ~x2."
          pos
          n
          (safe-access-event-tuple-number (cddr (car w))))))
    (t (sequential-event-landmarksp1 (+ 1 pos) n (cdr w)))))

(defun sequential-event-landmarksp
  (w)
  (declare (xargs :guard (plist-worldp w)))
  (sequential-event-landmarksp1 0
    (safe-access-event-tuple-number (fgetprop 'event-landmark 'global-value nil w))
    w))

(defun sequential-command-landmarksp1
  (pos n w)
  (declare (xargs :guard (and (natp pos) (plist-worldp w))))
  (cond ((atom w) (if (equal n -2)
        (eq w nil)
        (bad-world! 'sequential-command-landmarksp1
          "When we reached the end of the world, n was ~x0 ~
                          instead of -2."
          n)))
    ((and (eq (car (car w)) 'command-landmark)
       (eq (cadr (car w)) 'global-value)) (if (equal n (safe-access-command-tuple-number (cddr (car w))))
        (sequential-command-landmarksp1 (+ 1 pos) (- n 1) (cdr w))
        (bad-world! 'sequential-command-landmarksp1
          "Item ~x0 was supposed to be COMMAND-LANDMARK ~x1 ~
                          but actually has number ~x2."
          pos
          n
          (safe-access-command-tuple-number (cddr (car w))))))
    (t (sequential-command-landmarksp1 (+ 1 pos) n (cdr w)))))

(defun sequential-command-landmarksp
  (w)
  (declare (xargs :guard (plist-worldp w)))
  (sequential-command-landmarksp1 0
    (safe-access-command-tuple-number (fgetprop 'command-landmark 'global-value nil w))
    w))

(defun pseudo-good-worldp
  (w redefp)
  (and (plist-worldp w)
    (pseudo-good-worldp2 0 w redefp)
    (sequential-event-landmarksp w)
    (sequential-command-landmarksp w)
    (good-command-blocksp w)))