Lines Matching refs:f2
3164 (!f f2 b s. f2 <> f ==>
3165 (ARM_READ_STATUS f (ARM_WRITE_STATUS f2 b s) = ARM_READ_STATUS f s)) /\
3175 (!f f2 b s. ARM_READ_STATUS f (ARM_WRITE_STATUS_SPSR f2 b s) =
3222 \\ TRY (Cases_on `f2`)
3243 (!f f2 b s. ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS f2 b s) =
3250 (!f f2 b s. f <> f2 ==>
3251 (ARM_READ_STATUS_SPSR f (ARM_WRITE_STATUS_SPSR f2 b s) =
3311 \\ TRY (Cases_on `f2`)