The diagonal language {(a b^n)^n | n > 0} is not indexed

This file applies the one-factor indexed-language shrinking theorem to the language {(a b^n)^n | n > 0}. Splitting a word at a exposes all complete b-runs. A bounded factorization of a sufficiently large diagonal word has one factor (including either fixed outer context) containing two as, hence an entire run b^n. That run survives shrinking and fixes the parameter of the resulting diagonal word, contradicting the strict decrease in length.

theorem abnPowN_not_is_Indexed : ¬is_Indexed abnPowN

The diagonal language {(a b^n)^n | n > 0} is not indexed.