		Search-engine friendly clone of the ACL2 documentation.

Initialization

System-initp

Check if a system state is an initial one.

Signature
(system-initp systate) → yes/no
Arguments: systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

Every correct validator must be in the initial state, and the network must be empty (no messages have been sent yet).

Furthermore, the network is initially empty.

Definitions and Theorems

Function: system-initp

(defun system-initp (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'system-initp))
    (declare (ignorable __function__))
    (and (system-validators-initp systate)
         (emptyp (get-network-state systate)))))

Theorem: booleanp-of-system-initp

(defthm booleanp-of-system-initp
  (b* ((yes/no (system-initp systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: system-initp-of-system-state-fix-systate

(defthm system-initp-of-system-state-fix-systate
  (equal (system-initp (system-state-fix systate))
         (system-initp systate)))

Theorem: system-initp-system-state-equiv-congruence-on-systate

(defthm system-initp-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (system-initp systate)
                  (system-initp systate-equiv)))
  :rule-classes :congruence)