Lines Matching defs:pre
790 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\
795 cond (stack_ok rsp top base stack dm m /\ ^pre)``
809 ``zPC p * zR 0x8w r8 * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)``
823 val pre = ``w2n r8 DIV 8 < LENGTH (stack:word64 list) /\
828 cond (stack_ok rsp top base stack dm m /\ ^pre)``
841 ``zPC p * zR 0x8w r8 * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)``
892 val pre = ``k < LENGTH (stack:word64 list) /\ k < 268435456``
896 cond (stack_ok rsp top base stack dm m /\ ^pre)``
910 ``zPC p * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)``
933 val pre = ``k < LENGTH (stack:word64 list) /\ k < 268435456``
937 cond (stack_ok rsp top base stack dm m /\ ^pre)``
952 ``zPC p * zR 0x0w r0 * zSTACK (base,stack) * cond (^pre)``