Lines Matching refs:rw
67 rw [state_component_equality]);
77 rw [check_clock_def, state_component_equality]);
122 rw[] >> fsrw_tac[ARITH_ss][]);
146 rw[Once sem_def] >>
156 `F` suffices_by rw[] >>
163 rw[] >>
165 rw[] >> fs[] >>
181 rw [sem_def, state_component_equality] >>
182 rw [] >>
196 rw [] >>
212 rw [sem_def, state_component_equality] >>
213 rw []
249 rw []);
262 rw []);
267 rw [sem_def] >>
270 rw []);
279 rw [sem_def]
283 rw [] >>
287 rw [] >>
292 rw [] >>
299 rw [] >>
306 rw [] >>
309 >- (rw [] >>
324 rw [sem_def, state_component_equality]
334 rw [] >>
345 `r' = r with clock := r'.clock` by rw [state_component_equality] >>
347 rw [] >>
353 `(r''' with clock := r'''.clock - 1) = (r'' with clock := r'''.clock - 1)` by rw [state_component_equality] >>
362 rw [] >>
373 `r' = r with clock := r'.clock` by rw [state_component_equality] >>
375 rw [] >>
381 `(r''' with clock := r'''.clock - 1) = (r'' with clock := r'''.clock - 1)` by rw [state_component_equality] >>
405 rw [] >>