		Search-engine friendly clone of the ACL2 documentation.

No-self-endorsed

No-self-endorsed-p-of-events-next

Preservation of the invariant by multiple transitions.

Definitions and Theorems

Theorem: no-self-endorsed-p-of-events-next

(defthm no-self-endorsed-p-of-events-next
  (implies (and (events-possiblep events systate)
                (no-self-endorsed-p systate))
           (no-self-endorsed-p (events-next events systate))))