Folding-grid proof of the deletion condition (source code)

= Folding-grid proof of the deletion condition

Arrange the lengths of all consecutive subwords of a word in a triangular grid. Under the <folding condition>, the boundary between length ascents and descents must contain a folding square. Its equal opposite vertices identify two letters that can be deleted. Induction proves the <deletion condition for involutory generators>.