Langlib

Langlib.Classes.RecursivelyEnumerable.Examples.AnBnCn

{aⁿbⁿcⁿ} as an RE Language #

The language {aⁿbⁿcⁿ} is recursively enumerable because it is context-sensitive (lang_eq_eq_is_CS, with the generating grammar and its derivation in Langlib.Classes.ContextSensitive.Examples.AnBnCn) and every context-sensitive language is recursively enumerable (is_RE_of_CS).

Main declarations #

source
theorem lang_eq_eq_is_RE :
is_RE lang_eq_eq

The language {aⁿbⁿcⁿ} is recursively enumerable, since it is context-sensitive.