Lines Matching refs:seq
17 rel_sequence R seq state =
18 (seq 0 = state) /\
19 !n. if (?x. R (seq n) x) then R (seq n) (seq (SUC n)) else (seq (SUC n) = seq n)`;
27 !seq. rel_sequence next seq state ==>
28 ?i. SEP_REFINE (q * r) less to_set (seq i) \/ allow (seq i)`;
52 !seq. rel_sequence next seq state ==>
53 ?i. SEP_REFINE (q * r) less to_set (seq i) \/ allow (seq i)``,
92 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`state`,`r'`,`seq`])
151 ``!n seq s. rel_sequence n seq s ==> !i. rel_sequence n (\j. seq (i + j)) (seq i)``,
153 \\ Cases_on `?s. n (seq (i + n')) s` \\ ASM_REWRITE_TAC []
171 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`state`,`r`,`seq`])
174 \\ Q.PAT_X_ASSUM `!x.bbb` (MP_TAC o Q.SPECL [`seq (i:num)`,`r`,`(\j. seq (i + j))`])
175 \\ `rel_sequence next (\j. seq (i + j)) (seq i)` by METIS_TAC [rel_sequence_shift]