Nested Quantifiers:Is this solution right

Question

I need to express this system specification using quantifiers and predicates.

The email address of every user can be retrieved whenever the archive contains at least one message sent by every user on the system

Here are the predicates i used

$S(m,x)$ = message $m$ is sent by user $x$

$A(a,x)$ = $a$ is the email address of $x$

$C(m)$ = archive contains message $m$

$U(x)$ = user $x$ is on system

$R(a)$ = email address $a$ can be retrieved

Here is my answer

$\forall x [(U(x) \rightarrow \exists m (C(m) \land S(m,x)) \rightarrow \forall a (A(a,x) \rightarrow R(a))]$

Is this solution right?

Answer 1

$$\forall x~[(U(x) \rightarrow \exists m~(C(m) \land S(m,x)) \rightarrow \forall a~(A(a,x) \rightarrow R(a))]$$

This says: The email address of any user can be retrieved whenever the archive contains at least one message sent by that user on the system.

You wanted to say: The email address of every user can be retrieved whenever the archive contains at least one message sent by every user on the system.

That is not quite the same thing.