Phi is a defined symbol. It is defined to equal the temporal formula

  Init  /\  [][AX \/ AY]        /\  WF      (AX)
                        <x, y>        <x, y>

               Click here for Explanation Mode       You are in Definition Mode