		Search-engine friendly clone of the ACL2 documentation.

Poseidon-main-definition

Param->size

Size of the state vector, i.e. r + c.

Signature
(param->size param) → r+c
Arguments: param — Guard (paramp param).
Returns: r+c — Type (posp r+c).

Definitions and Theorems

Function: param->size

(defun param->size (param)
  (declare (xargs :guard (paramp param)))
  (let ((__function__ 'param->size))
    (declare (ignorable __function__))
    (+ (param->rate param)
       (param->capacity param))))

Theorem: posp-of-param->size

(defthm posp-of-param->size
  (b* ((r+c (param->size param)))
    (posp r+c))
  :rule-classes :rewrite)

Theorem: param->size-of-param-fix-param

(defthm param->size-of-param-fix-param
  (equal (param->size (param-fix param))
         (param->size param)))

Theorem: param->size-param-equiv-congruence-on-param

(defthm param->size-param-equiv-congruence-on-param
  (implies (param-equiv param param-equiv)
           (equal (param->size param)
                  (param->size param-equiv)))
  :rule-classes :congruence)