Lines Matching refs:g1
144 /\ (ACTLSTAR_PATH (g1 \/ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)
145 /\ (ACTLSTAR_PATH (g1 /\ g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)
149 /\ (ACTLSTAR_PATH (g1 U g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)
150 /\ (ACTLSTAR_PATH (g1 R g2) = ACTLSTAR_PATH g1 /\ ACTLSTAR_PATH g2)`;
252 /\ (STATESAT (M,s) (E g1) = ?PI. (PI IS_FAIR_PATH_IN M) /\
253 (PI STATE_NO 0 = s) /\ PATHSAT(M,PI) g1)
254 /\ (STATESAT (M,s) (A g1) = !PI. (PI IS_FAIR_PATH_IN M) /\
255 (PI STATE_NO 0 = s) ==> PATHSAT(M,PI) g1)
258 /\ (PATHSAT (M,PI) (g1 FAILS) = ~PATHSAT (M,PI) g1)
259 /\ (PATHSAT (M,PI) (g1 \/ g2) = PATHSAT (M,PI) g1 \/ PATHSAT (M,PI) g2)
260 /\ (PATHSAT (M,PI) (g1 /\ g2) = PATHSAT (M,PI) g1 /\ PATHSAT (M,PI) g2)
261 /\ (PATHSAT (M,PI) (X g1) = PATHSAT (M, PI FROM 1) g1)
262 /\ (PATHSAT (M,PI) (FU g1) = ?k. k >= 0 /\ PATHSAT (M,(PI FROM k)) g1)
263 /\ (PATHSAT (M,PI) (G g1) = !i. i>=0 ==> PATHSAT (M,PI FROM i) g1)
264 /\ (PATHSAT (M,PI) (g1 U g2) = ?k. k>=0 /\ PATHSAT (M,PI FROM k) g2 /\
265 !j. 0<=j/\j<k ==> PATHSAT(M,PI FROM j) g1)
266 /\ (PATHSAT (M,PI) (g1 R g2) = !j. j>=0
267 ==> (!i. i<j ==> ~PATHSAT(M,PI FROM i) g1)