Add proof for power_decoder2.DecodeA