formal proof of OP_EXTSWSLI