(cst-%x23-7f-nat abnf::cst) → nat
Function:
(defun cst-%x23-7f-nat (abnf::cst) (declare (xargs :guard (abnf::treep abnf::cst))) (declare (xargs :guard (cst-matchp abnf::cst "%x23-7F"))) (let ((__function__ 'cst-%x23-7f-nat)) (declare (ignorable __function__)) (lnfix (nth 0 (abnf::tree-leafterm->get abnf::cst)))))
Theorem:
(defthm natp-of-cst-%x23-7f-nat (b* ((nat (cst-%x23-7f-nat abnf::cst))) (natp nat)) :rule-classes :rewrite)
Theorem:
(defthm cst-%x23-7f-nat-of-tree-fix-cst (equal (cst-%x23-7f-nat (abnf::tree-fix abnf::cst)) (cst-%x23-7f-nat abnf::cst)))
Theorem:
(defthm cst-%x23-7f-nat-tree-equiv-congruence-on-cst (implies (abnf::tree-equiv abnf::cst cst-equiv) (equal (cst-%x23-7f-nat abnf::cst) (cst-%x23-7f-nat cst-equiv))) :rule-classes :congruence)