Change arg max to max in Appendix D.

[acoglio]

Here j is the maximum x such that there exists an \mathbf{l} such that etc. etc.
That is, j is the length of the longest common prefix of all the keys (nibble
arrays) of the \mathfrak{I} map.

Note that j is not the argument x that maximizes the value of a function over x.
The expression \exists \mathbf{l} ... following \arg \max is boolean-valued.

Also change a colon into a \wedge, which conjoins the two constraints over x and
\mathbf{l} in the set comprehension.

[nicksavers]

For review. This changes the following

into

[acoglio]

Thanks, @nicksavers. I'll add screenshots like yours to future PRs.

[acoglio]

@nicksavers, given that nobody has objected to the change, would you be willing to merge it?

I'll mention that this change is based on a formal specification of Modified Merkle Patricia trees that I have developed in the ACL2 theorem prover, available on GitHub here. In particular, to calculate that index j, I used a max (not arg max) operator, in the function mmp-encode-c-max starting at line 538 of that file. I also proved that the maximum exists, under suitable invariants of the recursive definition of the c and n functions in the Yellow Paper.