Lines Matching refs:f2
278 \\ Q.ABBREV_TAC `f2 = (r1 =+ n2w y) f`
279 \\ `(x * one (r1,n2w y)) (fun2set (f2,df))` by
280 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC)
466 \\ Q.ABBREV_TAC `f2 = (a + 0x4w =+ n2w (w2n c)) ((a =+ 0xE9w) f)`
470 one (a + 0x4w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by
471 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC)
476 `b2`,`f2`,`df`,`a+4w`,`r4`,`r3`]) x86_addr_thm
489 \\ Q.PAT_ABBREV_TAC `f2 = (a + 0x7w =+ (n2w (w2n (c:word7))):word8) ff`
495 one (a + 0x7w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by
496 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC)
502 `b2`,`f2`,`df`,`a+7w`,`r4`,`r3`]) x86_addr_thm
516 \\ Q.PAT_ABBREV_TAC `f2 = (a + 0x7w =+ (n2w (w2n (c:word7))):word8) ff`
522 one (a + 0x7w,n2w (w2n (c:word7)))) (fun2set (f2,df))` by
523 (Q.UNABBREV_TAC `f2` \\ SEP_WRITE_TAC)
529 `b2`,`f2`,`df`,`a+7w`,`r4`,`r3`]) x86_addr_thm