title: Proof of correct of the dynamic programming approach to min edit distance
body: <p>To calculate min edit distance (the minimum amount of insertions, deletions and substitutions required to transform one word to another), a dynamic programming solution is based on the recurrence relation, where the last character of both string is examined. The details are in <a href="https://en.wikipedia.org/wiki/Wagner%E2%80%93Fischer_algorithm" rel="noreferrer">https://en.wikipedia.org/wiki/Wagner%E2%80%93Fischer_algorithm</a>.</p>
  
  <p>The description of this algorithm is everywhere on the Internet when it comes to edit distance, but all of them just asserts its correctness without proof.  By definition of edit distance, you can insert, delete or substitute characters in the middle, not just at the end. Then how do you prove that this recurrence relation actually holds?</p>