Lines Matching refs:seq
39 (qspecl_then [`state`, `seq`, `r * r'`] imp_res_tac)
71 !state y seq.
72 p (SELECT_STATE m y (seq 0)) /\ rel_sequence next seq state ==>
73 q (SELECT_STATE m y (seq 1)) /\
74 (FRAME_STATE m y (seq 0) = FRAME_STATE m y (seq 1))`,
98 \\ `NEXT_REL (=) next (seq 0) (seq (SUC 0))`
100 `?x. NEXT_REL (=) next (seq 0) x`
104 \\ qexists_tac `seq 0`
111 \\ qpat_assum `!y:'b set. P` (qspecl_then [`y`,`seq 0`] imp_res_tac)