Measure for recurring over path structures.

**Function: **

(defun path-count (x) (declare (xargs :guard (path-p x))) (let ((__function__ 'path-count)) (declare (ignorable __function__)) (case (path-kind x) (:wire 1) (:scope (+ 3 (path-count (path-scope->subpath x)))))))

**Theorem: **

(defthm natp-of-path-count (b* ((count (path-count x))) (natp count)) :rule-classes :type-prescription)

**Theorem: **

(defthm path-count-of-path-fix-x (equal (path-count (path-fix x)) (path-count x)))

**Theorem: **

(defthm path-count-path-equiv-congruence-on-x (implies (path-equiv x x-equiv) (equal (path-count x) (path-count x-equiv))) :rule-classes :congruence)

**Theorem: **

(defthm path-count-of-path-scope (implies t (< (+ (path-count subpath)) (path-count (path-scope subpath namespace)))) :rule-classes :linear)

**Theorem: **

(defthm path-count-of-path-scope->subpath (implies (equal (path-kind x) :scope) (< (path-count (path-scope->subpath x)) (path-count x))) :rule-classes :linear)