Begin adding formal proof for fpcmp