Lines Matching refs:seq
57 seq_relation (NEXT_REL (=) next) seq s
61 seq 0 = s,
62 seq 1 = THE (next s),
63 seq 2 = THE (next (THE (next s))), ...
65 If ``next (seq n) = NONE`` for some "n" then this final state is repeated
220 !y s t1 seq.
221 p (SELECT_STATE m y t1) /\ r t1 s /\ rel_sequence next seq s ==>
222 ?k t2. q (SELECT_STATE m y t2) /\ r t2 (seq k) /\
243 !y s seq.
244 p (SELECT_STATE m y s) /\ rel_sequence next seq s ==>
245 ?k. q (SELECT_STATE m y (seq k)) /\
246 (FRAME_STATE m y s = FRAME_STATE m y (seq k))`,
263 \\ `NEXT_REL r next (seq 0) (seq (SUC 0))`
265 `?x. NEXT_REL r next (seq 0) x`
269 \\ qexists_tac `seq 0`
276 \\ `seq 0 = s` by full_simp_tac std_ss [rel_sequence_def]