machine-code/lisp/lisp_equalScript.sml

608   ``(!x. x IN bb \/ x - 4w IN bb ==> (f5 x = ft x)) ==>
609     !t a s. (lisp_x t (a,bb,ft) s = lisp_x t (a,bb,f5) s)``,
616       \\ Cases_on `f5 (a + 0xFFFFFFE4w) = 0w`
654   \\ Q.ABBREV_TAC `f5 = (a - 4w  =+ r8) f4`
655   \\ Q.ABBREV_TAC `wl = (f5 (a - 32w))`
656   \\ Q.ABBREV_TAC `wi = (f5 (a - 28w))`
660   \\ `?r3t r4t r5t r6t r7t r8t dft ft. arm_eq_loop (r3,r4,wi,wl,ww,0w ,df,f5) =
670   \\ `lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f5,s,rest)` by
673   \\ `f5 (a - 32w) = n2w (8 * limit)` by
694   \\ `lisp_inv (LISP_EQUAL x1 x2,x2,x3,x4,x5,x6,limit) (r3u,r4,r5,r6,r7,r8,a,df,f5,s,rest)` by
698   \\ Q.PAT_X_ASSUM `lisp_inv (x1,x2,x3,x4,x5,x6,limit) (r3,r4,r5,r6,r7,r8,a,df,f5,s,rest)` (K ALL_TAC)
703   \\ `~(a - 20w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
704   \\ `~(a - 16w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
705   \\ `~(a - 12w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
706   \\ `~(a - 8w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
707   \\ `~(a - 4w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
710      (RES_TAC \\ REPEAT (Q.PAT_X_ASSUM `f5 xx = yy` (fn th => REWRITE_TAC [GSYM th]))
712       \\ Q.UNABBREV_TAC `f4` \\ Q.UNABBREV_TAC `f5`
720   \\ `~(a - 28w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
721   \\ `~(a - 32w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
722   \\ `~(a + 4w IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
723   \\ `~(a IN heap_half (a, ~(f5 (a - 28w) = 0w),limit))` by tac2
724   \\ Q.PAT_X_ASSUM `f5 (a - 28w) = (if u then 0w else 1w)` ASSUME_TAC
760   \\ `(!x. x IN bb \/ x - 4w IN bb ==> (f5 x = ft x))` by
762     THEN1 (Q.PAT_X_ASSUM `!x. bbb ==> (f5 x = ft x)` MATCH_MP_TAC
767     \\ Q.PAT_X_ASSUM `!x. bbb ==> (f5 x = ft x)` MATCH_MP_TAC