Recognizer for fgl-generic-rune.
(fgl-generic-rune-p x) → *
Function:
(defun fgl-generic-rune-p (x) (declare (xargs :guard t)) (let ((__function__ 'fgl-generic-rune-p)) (declare (ignorable __function__)) (case (tag x) ((:brewrite :bformula :bmeta) (fgl-binder-rune-p x)) (otherwise (fgl-rune-p x)))))
Theorem:
(defthm consp-when-fgl-generic-rune-p (implies (fgl-generic-rune-p x) (consp x)) :rule-classes :compound-recognizer)
Theorem:
(defthm fgl-generic-rune-p-when-fgl-binder-rune-p (implies (fgl-binder-rune-p x) (fgl-generic-rune-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-generic-rune-p-when-fgl-rune-p (implies (fgl-rune-p x) (fgl-generic-rune-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-binder-rune-p-by-tag-when-fgl-generic-rune-p (implies (and (or (equal (tag x) :brewrite) (equal (tag x) :bformula) (equal (tag x) :bmeta)) (fgl-generic-rune-p x)) (fgl-binder-rune-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-rune-p-by-tag-when-fgl-generic-rune-p (implies (and (or (equal (tag x) :rewrite) (equal (tag x) :definition) (equal (tag x) :formula) (equal (tag x) :primitive) (equal (tag x) :meta)) (fgl-generic-rune-p x)) (fgl-rune-p x)) :rule-classes ((:rewrite :backchain-limit-lst 1)))
Theorem:
(defthm fgl-generic-rune-p-when-invalid-tag (implies (and (not (equal (tag x) :brewrite)) (not (equal (tag x) :bformula)) (not (equal (tag x) :bmeta)) (not (equal (tag x) :rewrite)) (not (equal (tag x) :definition)) (not (equal (tag x) :formula)) (not (equal (tag x) :primitive)) (not (equal (tag x) :meta))) (not (fgl-generic-rune-p x))) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm tag-when-fgl-generic-rune-p-forward (implies (fgl-generic-rune-p x) (or (equal (tag x) :brewrite) (equal (tag x) :bformula) (equal (tag x) :bmeta) (equal (tag x) :rewrite) (equal (tag x) :definition) (equal (tag x) :formula) (equal (tag x) :primitive) (equal (tag x) :meta))) :rule-classes ((:forward-chaining)))