{0ⁿ1ⁿ2ᵐ3ᵐ} is not linear

The linear pumping lemma confines the pumped pieces to the two ends of the witness {0ⁿ1ⁿ2ᵐ3ᵐ}, so pumping breaks one of the two independent aⁿbⁿ matchings (anbncmdm_not_is_Linear). The relabelled version map_anbncmdm_not_is_Linear follows because linearity reflects along injective terminal maps.

theorem anbncmdm_not_is_Linear : ¬is_Linear anbncmdm

{0ⁿ1ⁿ2ᵐ3ᵐ} is not linear.

theorem map_anbncmdm_not_is_Linear {T : Type} (e : Fin 4 ↪ T) : ¬is_Linear ((Language.map ⇑e) anbncmdm)

The relabelled witness is not linear: linearity would reflect back to anbncmdm.