		Search-engine friendly clone of the ACL2 documentation.

Same-committees

Same-committees-p-when-reachable

The invariant holds in every reachable state.

Definitions and Theorems

Theorem: same-committees-p-when-reachable

(defthm same-committees-p-when-reachable
  (implies (and (system-state-reachablep systate)
                (system-committees-fault-tolerant-p systate))
           (same-committees-p systate)))