Lines Matching defs:x3
54 zLISP_ALT side (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) =
61 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST)
66 zLISP_R (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) =
73 cond (lisp_inv (a1,a2,sl,sl1,e,ex,cs,ok) (x0,x1,x2,x3,x4,x5,^VAR_REST)
88 ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,ddd,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
298 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
299 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,p+3w::qs,code,amnt,ok) * zPC r2``
308 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
309 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,r2::qs,code,amnt,ok) * zPC (p+2w)``
318 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
319 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,TL qs,code,amnt,ok) * zPC (HD qs)``
329 val pre_tm = ``zLISP_ALT b ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
330 val post_tm = ``zLISP_ALT b ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,TL qs,code,amnt,ok) * zPC (HD qs) * ~zS``
339 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
340 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = HD qs) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,TL qs,code,amnt,ok) * zPC (p+2w)``
350 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
351 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,p+6w::qs,code,amnt,ok) * zPC (p + n2w (6 + SIGN_EXTEND 32 64 (w2n (imm32:word32))))``
365 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
366 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
373 val tm = ``lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST)
408 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
409 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
416 val tm = ``lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST)
453 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
454 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)``
461 val tm = ``lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST)
489 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
490 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (isDot x)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
530 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
531 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (isSym x)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
571 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
572 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (isVal x)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
599 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
600 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = Val 0)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
639 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
640 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = Val n)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
672 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
673 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = y:SExp)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
704 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
705 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_CF (SOME (getVal x0 < getVal x1)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_ZF``
727 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
728 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME (EVEN (getVal x0))) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
760 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
761 val post_tm = set_pc th ``zLISP ^STAT (Val n,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
785 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
786 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
825 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
826 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
850 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
851 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME (x = res:SExp)) * ~zS1 Z_PF * ~zS1 Z_SF * ~zS1 Z_AF * ~zS1 Z_OF * ~zS1 Z_CF``
877 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
878 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC ex``
889 \\ Q.EXISTS_TAC `(x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)`
898 (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,F) * zPC (rip+7w) * ~zS \/
911 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
912 val post_tm = set_pc th ``zLISP ^STAT (LISP_TEST (isQuote x0),x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
923 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
924 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
962 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
963 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = ^tm) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
996 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
997 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^NEW_STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
1024 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1025 val post_tm = set_pc th ``zLISP ^STAT (LISP_TEST (x0 = x1:SExp),Sym "NIL",x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1082 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1083 val post_tm = set_pc th ``zLISP ^STAT (LISP_ADD x0 x1,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1093 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1094 val post_tm = set_pc th ``zLISP ^STAT (Val 0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1101 ``{x1;x2;x3} UNION {x1;x2;x3;x4;x5;x6} = {x1;x2;x3;x4;x5;x6}``,
1150 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1151 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1162 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1163 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1207 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1208 val post_tm = set_pc th ``zLISP ^STAT (LISP_SUB x0 x1,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1227 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1228 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1253 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1254 val post_tm = set_pc th ``zLISP ^STAT (Val (getVal x0 DIV 2),x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1275 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1276 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1296 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1297 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1345 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond z_zf``
1346 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)``
1353 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond ~z_zf``
1354 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)``
1365 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1392 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond z_zf``
1393 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)``
1400 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf) * precond ~z_zf``
1401 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * zS1 Z_ZF (SOME z_zf)``
1412 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1438 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1439 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,IO_STATS ^tm io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1459 (zLISP_ALT b1 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c1 q1 ==>
1461 (zLISP_ALT b2 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c2 q2 ==>
1464 (zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) (c1 UNION c2) (q1 \/ q2)``,
1475 val x3 = x64_encodeLib.x64_encode "mov r2d,r1d"
1480 val ((th3,_,_),_) = spec x3
1490 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1491 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1492 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1507 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1508 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wsp = 0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1516 ``{x1;x2} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``,
1542 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1543 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1544 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1559 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1560 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1568 ``{x1;x2} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``,
1624 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1625 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1638 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1639 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(wi = we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1670 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wsp <> 0x0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1671 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,x::xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1731 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (wi <> we)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1732 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1761 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1762 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,TL xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1787 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1788 val post_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1823 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1824 val post_tm = set_pc th ``zLISP ^STAT (EL (w2n (j:29 word)) xs,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1842 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1843 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,UPDATE_NTH (w2n (j:29 word)) x0 xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1871 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1872 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,DROP (w2n (j:word30)) xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
1893 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1894 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,IO_WRITE io ^tm,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1910 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1925 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
1976 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1977 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1983 val post1_tm = subst [``n:num``|->s_len] ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,remove_parse_stack xs,xs1,io,xbp,qs,code,amnt,ok) * ~zS * zPC (rip + n2w n)``
1995 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
1996 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
2009 val post1_tm = subst [``n:num``|->s_len] ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,remove_parse_stack xs,io,xbp,qs,code,amnt,ok) * ~zS * zPC (rip + n2w n)``
2022 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
2023 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip``
2029 val post1_tm = subst [``n:num``|->s_len] ``zLISP ^STAT (no_such_function x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * ~zS * zPC (rip + n2w n)``
2057 (lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST)
2061 val post = set_pc th ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2076 val pre = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2115 (lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST)
2119 val post = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2146 val pre = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2173 val pre_tm = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2175 LISP_TEST (FST (is_eof (getINPUT io))),x1,x2,x3,x4,x5,xs,xs1,
2193 cond (lisp_inv ^STATINV (x0,x1,x2,x3,x4,x5,^VAR_REST)
2215 val pre = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2278 val pre_tm = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2279 val post_tm = set_pc th ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2292 val pre_tm = ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2293 val post_tm = set_pc th ``zLISP_R ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2304 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2305 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2309 val thB = RW [SEP_CLAUSES] (Q.INST [`x1`|->`Sym "NIL"`,`x2`|->`Sym "NIL"`,`x3`|->`Sym "NIL"`,`x0`|->`z0`] thB)
2334 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2335 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,LENGTH xs,qs,code,amnt,ok) * zPC p``
2343 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2344 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,EL (LENGTH xs + getVal x1 - xbp) xs,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2352 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2353 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,UPDATE_NTH (LENGTH xs + getVal x1 - xbp) x0 xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2364 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2365 val post_tm = set_pc th ``zLISP ^STAT (x0,Val amnt,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2376 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2377 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,DROP (getVal x1) xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2388 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2389 val post_tm = set_pc th ``zLISP ^STAT (Val (code_ptr code),x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2400 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2401 val post_tm = set_pc th ``zLISP ^STAT (EL (getVal x0) xs1,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2434 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2435 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = ^tm) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2441 (zLISP_ALT b1 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c1 q1 ==>
2443 (zLISP_ALT b2 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) c2 q2 ==>
2446 ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * p) (c1 UNION c2) (q1 \/ q2)``,
2454 val x3 = x64_encodeLib.x64_encode "mov r2d,12"
2459 val ((th3,_,_),_) = spec x3
2469 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ((tw2 = EL 7 ds) /\ (tw2 = 0w))) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2470 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2471 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2485 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ((tw2 = EL 7 ds) /\ ~(tw2 = 0w))) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2486 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (~(EL 7 ds = 0w))) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2493 ``{x1;x2} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``,
2507 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. ~(EL 7 ds = 0x0w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2508 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (Val (LENGTH xs1),x1,x2,x3,x4,x5,xs,xs1 ++ [x0],io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2542 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2543 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev (EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2544 val post1_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2560 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2561 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. Abbrev ~(EL 3 ds <=+ 0x100w)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2569 ``{x1;x2;x3} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``,
2586 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. 0x100w <+ EL 3 ds) ^NEWSTAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2587 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. T) ^NEWSTAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2690 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2691 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2700 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC rip * ~zS``
2701 val post_tm = set_pc th ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2708 ``{x1;x2;x3} UNION {x1;x2;x3;x4} = {x1;x2;x3;x4}``,
2730 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. tw2 = r2) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2731 val post_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC r2``
2740 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2741 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = EL 4 cs + n2w (getVal x2)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2759 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2760 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = ^tm) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
2813 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2814 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = EL 4 cs + n2w (getVal x2)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2824 val pre_tm = ``zLISP_ALT (\wsp wi we ds tw2. T) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2825 val post_tm = set_pc th ``zLISP_ALT (\wsp wi we ds tw2. tw2 = EL 4 cs + n2w (getVal x2)) ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2842 (zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok)) {}
2843 (zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME F,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok))``,
2887 val pre_tm = ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME F,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2888 val post_tm = set_pc th ``zLISP (a1,a2,sl,sl1,e,ex,cs,rbp,SOME T,cu) (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``
2915 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)``
2916 val post_tm = set_pc th ``zLISP ^STAT (Sym "T",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)``
2924 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)``
2925 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)``
2954 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)``
2955 val post_tm = set_pc th ``zLISP ^STAT (Sym "T",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME F)``
2963 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)``
2964 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_ZF (SOME T)``
2995 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME T)``
2996 val post_tm = set_pc th ``zLISP ^STAT (Sym "T",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME T)``
3004 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME F)``
3005 val post_tm = set_pc th ``zLISP ^STAT (Sym "NIL",x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * zS1 Z_CF (SOME F)``
3026 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
3027 val post_tm = set_pc th ``zLISP ^STAT (x1,x0,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p``
3035 val pre_tm = ``zLISP ^STAT (x0,x1,x2,x3,x4,x5,xs,xs1,io,xbp,qs,code,amnt,ok) * zPC p * ~zS``