add formal proof for shift/rot o.ok