add formal proof for OP_RLC