Almost Instantaneous Fixed to Variable (AIFV) coding is a relatively new method of lossless coding that, unlike Huffman coding, uses more than one coding tree. The problem of constructing optimal AIFV codes is a special case of that of constructing minimum cost Markov chains. This paper provides the first complete proof of correctness for the previously known iterative algorithm for constructing such Markov chains. A recent work describes how to efficiently solve the minimum cost Markov chain problem by first constructing a "Markov Chain Polytope" and then running the Ellipsoid algorithm for linear programming on it. This paper's second result is that, in the AIFV case, a special property of the polytope instead permits solving the corresponding linear program using simple binary search.