This repository contains Lean-assisted proofs about properties of the Horizontal-Compression Algorithm.
- HorizontalCompressionEXEC contains an implementation of the Horizontal-Compression Algorithm.
- HorizontalCompressionWEB contains the web version of the proof.
To run this project, please copy-paste the EXEC/WEB file to:
https://live.lean-lang.org/#project=lean-nightly
Note that it may take a minute or so until the file is ready.