The language {0ⁿ1ⁿ2ᵐ3ᵐ} over Fin 4

The witness language used for Linear ⊊ CF and the non-closure of linear languages under concatenation. It is the concatenation of two relabelled copies of {aⁿbⁿ} (anbn): one mapped onto 0/1 and one onto 2/3.

Class-membership facts live in Langlib.Classes.ContextFree.Examples.L4 (L4_is_CF) and Langlib.Classes.Linear.Examples.L4 (L4_not_is_Linear).

def f4 : Bool → Fin 4

Inject aⁿbⁿ's alphabet to 0/1.

Equations

• f4 b = if b = true then 1 else 0

def g4 : Bool → Fin 4

Inject aⁿbⁿ's alphabet to 2/3.

Equations

• g4 b = if b = true then 3 else 2

def L4 : Language (Fin 4)

The witness language {0ⁿ1ⁿ2ᵐ3ᵐ} over Fin 4.

Equations

• L4 = (Language.map f4) anbn * (Language.map g4) anbn