Constructive proofs of Higman’s lemma formalized in Agda

Folders

• Berghofer : a proof by Stefan Berghofer (for a two-letter alphabet).
• Seisenberger : proofs by Monika Seisenberger (for a finite alphabet and for an infinite alphabet).

Agda and stdlib versions

This version is compatible with

• Agda 2.6.4
• The Standard Library 1.7.3