The balanced-copy language of abnPowM

Let A = {(a b^n)^m | n,m > 0} and B be the two intersection witnesses abnPowM and abnAbStarPowPredN. Over a fresh three-letter alphabet, define the numerator

{ code(w) # reverse(code(w)) | w ∈ A }

and the denominator { # reverse(code(v)) | v ∈ B }. The separator makes the quotient split unique, so their right quotient is exactly the encoded diagonal intersection.

Indexed-language membership facts live in Langlib.Classes.Indexed.Examples.AbnPowMCopy.

inductive CopyLetter : Type

Three-letter alphabet used to separate the copied halves.

• a : CopyLetter
• b : CopyLetter
• separator : CopyLetter

instance instDecidableEqCopyLetter : DecidableEq CopyLetter

Equations

• instDecidableEqCopyLetter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instFintypeCopyLetter : Fintype CopyLetter

Equations

• instFintypeCopyLetter = { elems := { val := ↑CopyLetter.enumList, nodup := CopyLetter.enumList_nodup }, complete := instFintypeCopyLetter._proof_1 }

def instInhabitedCopyLetter.default : CopyLetter

Equations

• instInhabitedCopyLetter.default = CopyLetter.a

instance instInhabitedCopyLetter : Inhabited CopyLetter

Equations

• instInhabitedCopyLetter = { default := instInhabitedCopyLetter.default }

def copyCode : Bool → CopyLetter

Embed the binary witness alphabet into the copy alphabet.

Equations

• copyCode false = CopyLetter.a
• copyCode true = CopyLetter.b

theorem copyCode_injective : Function.Injective copyCode

def abnPowMCopy : Language CopyLetter

The numerator of the indexed right-quotient witness.

Equations

• abnPowMCopy w = ∃ (n : ℕ) (m : ℕ), 0 < n ∧ 0 < m ∧ w = List.map copyCode (blockPower n m) ++ [CopyLetter.separator] ++ List.map copyCode (blockPower n m).reverse

def abnPowMCopyDenominator : Language CopyLetter

Denominator of the indexed right-quotient counterexample.

Equations

• abnPowMCopyDenominator = singletonWordLanguage [CopyLetter.separator] * ((Language.map copyCode) abnAbStarPowPredN).reverse

theorem abnPowMCopy_quotient_eq_abnPowN : abnPowMCopy / abnPowMCopyDenominator = (Language.map copyCode) abnPowN

The explicit quotient is exactly the encoded diagonal intersection.