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