Lines Matching refs:guard
191 (exec_next locs (IF guard n1 n2) s t w call =
192 if guard s then exec_next locs n1 s t w call
366 !guard. IMPL_INST code locs (Inst pc1 assert1 (IF guard next1 next2))``,
372 !guard. IMPL_INST code locs
373 (Inst pc1 (\s. if guard s then assert1 s else assert2 s)
374 (IF guard next1 next2))``,
379 (Inst pc assert (IF guard (ASM (SOME s1) up1 j1)
382 (Inst pc assert (IF guard (ASM (SOME (\s. guard s ==> s1 s)) up1 j1)
383 (ASM (SOME (\s. ~guard s ==> s2 s)) up2 j2)))``,
388 (Inst pc assert (IF guard (ASM (SOME (\s. T)) up1 j1) next)) <=>
390 (Inst pc assert (IF guard (ASM NONE up1 j1) next))) /\
392 (Inst pc assert (IF guard next (ASM (SOME (\s. T)) up1 j1))) <=>
394 (Inst pc assert (IF guard next (ASM NONE up1 j1))))``,
522 (next_trans n t (IF guard n1 n2) =
525 (t2,[(n,Cond (NextNode t) (NextNode (t+2)) guard)] ++ xs ++ ys)) /\