		Search-engine friendly clone of the ACL2 documentation.

Initialization

System-init-loop2

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

Definitions and Theorems

Function: system-init-loop2

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

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

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