//
// flight rule: lsamRendezvous can only be invoked after lasJettison has been invoked
//
// see Assumption1.txt for details

FlightRule2 = (lasJettison -> Q1),
Q1 = (lasJettison -> Q1
     | lsamRendezvous -> Q1).