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