add formal proof for OP_RLCL