The invariant holds in every reachable state.
Theorem: nonforking-anchors-p-when-reachable
(defthm nonforking-anchors-p-when-reachable (implies (and (system-state-reachablep systate) (system-committees-fault-tolerant-p systate)) (nonforking-anchors-p systate)))
