Recognizer for fgl-binder-rule structures.
(fgl-binder-rule-p x) → *
Function:
(defun fgl-binder-rule-p (x) (declare (xargs :guard t)) (let ((__function__ 'fgl-binder-rule-p)) (declare (ignorable __function__)) (and (consp x) (cond ((or (atom x) (eq (car x) :brewrite)) (and (consp (cdr x)) (consp (car (cdr x))) (consp (cdr (car (cdr x)))) (consp (cdr (cdr x))) (consp (car (cdr (cdr x)))) (consp (cdr (cdr (cdr x)))) (b* ((rune (car (car (cdr x)))) (lhs-fn (car (cdr (car (cdr x))))) (lhs-args (cdr (cdr (car (cdr x))))) (hyps (car (car (cdr (cdr x))))) (rhs (cdr (car (cdr (cdr x))))) (equiv (car (cdr (cdr (cdr x))))) (r-equiv (cdr (cdr (cdr (cdr x)))))) (and (fgl-binder-rune-p rune) (pseudo-fnsym-p lhs-fn) (pseudo-term-listp lhs-args) (pseudo-term-listp hyps) (pseudo-termp rhs) (pseudo-fnsym-p equiv) (pseudo-fnsym-p r-equiv))))) (t (and (eq (car x) :bmeta) (and (true-listp (cdr x)) (eql (len (cdr x)) 1)) (b* ((name (std::da-nth 0 (cdr x)))) (pseudo-fnsym-p name))))))))
Theorem:
(defthm consp-when-fgl-binder-rule-p (implies (fgl-binder-rule-p x) (consp x)) :rule-classes :compound-recognizer)