Lines Matching refs:fp
51 (reade st (isV k) = read st (MEM (fp, NEG k))) /\
58 (writee st (isV k, v) = write st (MEM (fp, NEG k)) v) /\
84 (eq_exp st (isR r) (isV v) = (r = fp)) /\
85 (eq_exp st (isV v) (isR r) = (r = fp)) /\
197 `!st e v. ~(eq_exp st e1 e2) /\ ~(e1 = isR fp) ==> ((st |# (e1,v) '' e2 = st '' e2))`,
350 [MLDR R9 (fp, NEG k); MSTR (13,offset) R9])`;
358 [MLDR R9 (13,offset); MSTR (fp, NEG (12 + k)) R9])`;
366 [MLDR R9 (fp, NEG k); MSTR (13,NEG 0) R9; MSUB R13 R13 (MC 1w)]) /\
376 [MLDR R9 (13, POS 1); MSTR (fp,NEG k) R9; MADD R13 R13 (MC 1w)]) /\
515 `~(isR 9 = isR fp) /\ ~(isR 13 = isR fp) /\ ~(isM (w2n (read st SP) - LENGTH l) = isR fp)`
547 `~(isR 9 = isR fp) /\ ~(isR 13 = isR fp)` by RW_TAC std_ss [fp_def] THEN
562 `~(isR 9 = isR fp) /\ ~(isR 13 = isR fp)` by RW_TAC std_ss [fp_def] THEN
872 `~(isR 9 = isR fp) /\ ~(isR sp = isR fp)` by RW_TAC std_ss [fp_def, sp_def] THEN