An overview over the KIV project can be found here
The problem is formulated algebraically. The entire axiomatization can be found in the specification solitaire. The game is formalized as the function solitaire, which returns the list of stacks after distributing all cards over the stacks, with the helper function push. The latter recurses over the stacks and prepends to the first stack where this is possible.
The idea of the proves is to switch the representation, i.e., we use the function solix, which returns the stack of indices (into the original sequence) instead of the cards themselves.
The first theorem solix-to-solitaire states that we can obtain the result of solitaire by calculating solix of the same cards and then replacing the indices in the stacks by the actual elements. This conversion is done by the function .tolist.
This allows us to prove the main theorem by proving the same theorem (found here) over the stack of indices. The proof of this theorem follows the description given by the organizers of the competition, i.e., the proof is decomposed into
- showing that there is an ascending sequence with a length equal to the number of stacks (main lemma theoremx-atleast)
- showing that the existence of a longer sequence is contradictory (main lemma theoremx-atmost-h shows that a longer ascending sequence yields two indices in the same stack)
A few properties about the result of solix are needed throughout the proofs and are defined by the predicates inv (stacks are nonempty and all indices are within the bounds of the original sequence), covers (all indices are covered by the resulting list of stacks) and ordered (the indices within each stack are ordered and the corresponding elements are also ordered).