TBF the proof is written for readability, not concision.

But also, this happens in programming as well:

"A search function looking for `x` in a sorted list that starts in the middle of the list, compares the element to `x`, and then recursively searches the front half or back half of the list"

"A valid HTML document with one button that, when clicked, downloads a text file containing the md5sum of the page"

"A facebook clone"