The positive language {a^n b^n c^n}

def lang_eq_eq_pos : Language (Fin 3)

The language {aⁿbⁿcⁿ | n ≥ 1} over Fin 3.

Equations

• lang_eq_eq_pos w = ∃ (n : ℕ), w = List.replicate (n + 1) 0 ++ List.replicate (n + 1) 1 ++ List.replicate (n + 1) 2