lisp-runtime/implementation/lisp_opsScript.sml

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``