Function:
(defun vl-simple-id-tail-string-p (x i len) (declare (xargs :guard (and (stringp x) (natp i) (eql len (length x))))) (declare (xargs :guard (<= i len))) (let ((__function__ 'vl-simple-id-tail-string-p)) (declare (ignorable __function__)) (if (mbe :logic (zp (- (nfix len) (nfix i))) :exec (eql i len)) t (and (vl-simple-id-tail-p (char x i)) (vl-simple-id-tail-string-p x (+ 1 (lnfix i)) len)))))
Theorem:
(defthm vl-simple-id-tail-string-p-of-str-fix-x (equal (vl-simple-id-tail-string-p (str-fix x) i len) (vl-simple-id-tail-string-p x i len)))
Theorem:
(defthm vl-simple-id-tail-string-p-streqv-congruence-on-x (implies (streqv x x-equiv) (equal (vl-simple-id-tail-string-p x i len) (vl-simple-id-tail-string-p x-equiv i len))) :rule-classes :congruence)
Theorem:
(defthm vl-simple-id-tail-string-p-of-nfix-i (equal (vl-simple-id-tail-string-p x (nfix i) len) (vl-simple-id-tail-string-p x i len)))
Theorem:
(defthm vl-simple-id-tail-string-p-nat-equiv-congruence-on-i (implies (acl2::nat-equiv i i-equiv) (equal (vl-simple-id-tail-string-p x i len) (vl-simple-id-tail-string-p x i-equiv len))) :rule-classes :congruence)