Context-Free Closure Under Permutations

This file specializes bijective terminal renaming to permutations of a fixed alphabet.

Proof idea: a permutation is a terminal bijection whose source and target alphabets coincide, so the result is immediate from context-free closure under bijective terminal renaming.

Main declarations

• CF_of_permute_CF

@[simp]

theorem CF_of_permute_CF {T : Type} (π : Equiv.Perm T) (L : Language T) : is_CF (L.permuteLang π) ↔ is_CF L

A language is context-free iff its image under a permutation of terminals is context-free.