		Search-engine friendly clone of the ACL2 documentation.

Initialization

System-init-loop1

Signature
(system-init-loop1 correct-vals) → map
Arguments: correct-vals — Guard (address-setp correct-vals).
Returns: map — Type (validators-statep map), given (address-setp correct-vals).

Definitions and Theorems

Function: system-init-loop1

(defun system-init-loop1 (correct-vals)
 (declare (xargs :guard (address-setp correct-vals)))
 (let ((__function__ 'system-init-loop1))
  (declare (ignorable __function__))
  (cond
       ((emptyp correct-vals) nil)
       (t (omap::update (head correct-vals)
                        (validator-init)
                        (system-init-loop1 (tail correct-vals)))))))

Theorem: validators-statep-of-system-init-loop1

(defthm validators-statep-of-system-init-loop1
  (implies (address-setp correct-vals)
           (b* ((map (system-init-loop1 correct-vals)))
             (validators-statep map)))
  :rule-classes :rewrite)