The balanced-copy quotient witnesses are indexed

Let A = {(a b^n)^m | n,m > 0} be the first intersection witness. This file constructs an indexed grammar for

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

The numerator and denominator languages are defined in Langlib.Examples.AbnPowMCopy. This file proves that both are indexed. For the numerator, the grammar chooses the common b-run length on its flag stack. A recursive nonterminal then emits matched block generators on the two sides of the separator. Every nonterminal created by an indexed production receives the same stack, so the two halves agree without putting an oracle into the language representation.

inductive CopyNT : Type

• S : CopyNT
• X : CopyNT
• Z : CopyNT
• W : CopyNT
• Y : CopyNT
• P : CopyNT
• Q : CopyNT

instance instDecidableEqCopyNT : DecidableEq CopyNT

Equations

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

inductive CopyFlag : Type

• count : CopyFlag
• bottom : CopyFlag

instance instDecidableEqCopyFlag : DecidableEq CopyFlag

Equations

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

def grammarAbnPowMCopy : IndexedGrammar CopyLetter

Indexed grammar producing a word from A, a separator, and its reversal.

Equations

• One or more equations did not get rendered due to their size.

A compositional soundness interpretation

theorem grammarAbnPowMCopy_language : grammarAbnPowMCopy.Language = abnPowMCopy

The balanced-copy grammar generates exactly the numerator witness.

theorem abnPowMCopy_is_Indexed : is_Indexed abnPowMCopy

The balanced-copy numerator is indexed.

theorem abnPowMCopyDenominator_is_Indexed : is_Indexed abnPowMCopyDenominator

The quotient denominator is indexed.