Lines Matching refs:i2
635 (cheney_step(i,j,e,m) = (i2,j2,e2,m2)) ==> (e2 = e) /\ j <= j2 /\
636 cheney_inv(b,b',i2,j2,j2,e2,f,m2,w,xx,r)``,
646 \\ Q.PAT_X_ASSUM `i + 1 = i2` (K ALL_TAC)
787 !i2 m2. (cheney(i,j,e,m) = (i2,m2)) ==>
788 cheney_inv(b,b',i2,i2,i2,e,f,m2,w,xx,r) /\ j <= i2) (i,j,e,m)``,
790 \\ `?i2 j2 e2 m2. cheney_step (i,j,e,m) = (i2,j2,e2,m2)` by METIS_TAC [PAIR]