Positive a b c slice witnesses

The witness languages used for the non-closure of deterministic context-free languages under union and Kleene star. They restrict the standard {aⁿbⁿcᵐ} / {aⁿbᵐcᵐ} witnesses to the regular slice a⁺b⁺c⁺ (abcPositive), which prevents a Kleene-star slice from splitting one a⁺b⁺c⁺ payload into several witness blocks.

The positive {aⁿbⁿcⁿ} witness is the shared lang_eq_eq_pos of Langlib.Examples.AnBnCnPos; the identity lang_eq_eq_pos = lang_eq_eq ⊓ abcPositive is lang_eq_eq_pos_eq_inter in Langlib.Classes.DeterministicContextFree.Examples.AbcPositive.

Class-membership facts live in Langlib.Classes.DeterministicContextFree.Examples.AbcPositive.

def abcPositive : Language (Fin 3)

The regular slice a⁺ b⁺ c⁺ over Fin 3.

Equations

• abcPositive w = ∃ (n : ℕ) (m : ℕ) (k : ℕ), w = List.replicate (n + 1) a_ ++ List.replicate (m + 1) b_ ++ List.replicate (k + 1) c_

def lang_eq_any_pos : Language (Fin 3)

{aⁿbⁿcᵐ} restricted to the positive slice.

Equations

• lang_eq_any_pos = lang_eq_any ⊓ abcPositive

def lang_any_eq_pos : Language (Fin 3)

{aⁿbᵐcᵐ} restricted to the positive slice.

Equations

• lang_any_eq_pos = lang_any_eq ⊓ abcPositive

def lang_not_eq_any_pos : Language (Fin 3)

The positive-slice words that are not {aⁿbⁿcᵐ}.

Equations

• lang_not_eq_any_pos = lang_eq_any_posᶜ ⊓ abcPositive

def lang_not_any_eq_pos : Language (Fin 3)

The positive-slice words that are not {aⁿbᵐcᵐ}.

Equations

• lang_not_any_eq_pos = lang_any_eq_posᶜ ⊓ abcPositive