provif中==>是什么意思？

Question

我在provif手册中找到了以下一行代码。

 ⋮ 
query event(evCocks) ==> event(evRSA).
 ⋮ 

==>

是什么意思？

EDIT: I have answered my own question below.

Answer 1

Correspondence properties:
  P and Q are predicates.

    P(x) ==> Q(x, y)

      for all x where P(x) is true, then there exists a y 
      such that Q(x, y) is true

query event(e1) ==> event(e2).

  the query above can be translated to the following question:
    Is it true that;
         for all executions of event e1 (in the protocol) it is true that 
         e2 has executed?

在provif手册中指出

query event(evCocks) ==> event(evRSA)

is true if and only if, for all executions of the protocol, if the event 
evCocks has been executed, then
event evRSA has also [already] been executed

链接到证明手册