		Search-engine friendly clone of the ACL2 documentation.

No-self-messages

Message-noselfp

Check that a message is not self-addressed.

Signature
(message-noselfp msg) → yes/no
Arguments: msg — Guard (messagep msg).
Returns: yes/no — Type (booleanp yes/no).

The certificate's author, who is the sender, must differ from the destination, who is the recipient.

Definitions and Theorems

Function: message-noselfp

(defun message-noselfp (msg)
  (declare (xargs :guard (messagep msg)))
  (let ((__function__ 'message-noselfp))
    (declare (ignorable __function__))
    (not (equal (certificate->author (message->certificate msg))
                (message->destination msg)))))

Theorem: booleanp-of-message-noselfp

(defthm booleanp-of-message-noselfp
  (b* ((yes/no (message-noselfp msg)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: message-noselfp-of-message-fix-msg

(defthm message-noselfp-of-message-fix-msg
  (equal (message-noselfp (message-fix msg))
         (message-noselfp msg)))

Theorem: message-noselfp-message-equiv-congruence-on-msg

(defthm message-noselfp-message-equiv-congruence-on-msg
  (implies (message-equiv msg msg-equiv)
           (equal (message-noselfp msg)
                  (message-noselfp msg-equiv)))
  :rule-classes :congruence)