Regular Languages Included in Recursively Enumerable Languages

This file proves that every right-regular language is recursively enumerable.

Main results

• RG_subclass_RE — every regular language is recursively enumerable

theorem grammar_transforms_of_RG_transforms {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : RG_transforms g w₁ w₂) : grammar_transforms (grammar_of_RG g) w₁ w₂

An RG transformation step corresponds to a grammar transformation step.

theorem RG_transforms_of_grammar_transforms {T : Type} {g : RG_grammar T} {w₁ w₂ : List (symbol T g.nt)} (h : grammar_transforms (grammar_of_RG g) w₁ w₂) : RG_transforms g w₁ w₂

A grammar transformation step from a converted RG corresponds to an RG step.

theorem RG_derives_iff_grammar_derives {T : Type} (g : RG_grammar T) (w₁ w₂ : List (symbol T g.nt)) : RG_derives g w₁ w₂ ↔ grammar_derives (grammar_of_RG g) w₁ w₂

RG derives iff grammar derives (for the converted grammar).

theorem RG_subclass_RE {T : Type} {L : Language T} (h : is_RG L) : is_RE L

Every right-regular language is recursively enumerable.

theorem is_RE_of_isRegular {T : Type} [Fintype T] {L : Language T} (h : L.IsRegular) : is_RE L

Every Mathlib-regular language over a finite alphabet is recursively enumerable.