attempting formal proof of OP_EXTSWSLI