The language {(a b^n)^m | n,m >= 1} is indexed

An indexed grammar chooses the common b-run length on its flag stack and then copies that stack to an arbitrary positive number of blocks.

The indexed grammar for abnPowM

inductive AbnPowMNT : Type

• S : AbnPowMNT
• X : AbnPowMNT
• Z : AbnPowMNT
• Y : AbnPowMNT
• P : AbnPowMNT

instance instDecidableEqAbnPowMNT : DecidableEq AbnPowMNT

Equations

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

inductive AbnPowMFlag : Type

• count : AbnPowMFlag
• bottom : AbnPowMFlag

instance instDecidableEqAbnPowMFlag : DecidableEq AbnPowMFlag

Equations

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

def grammarAbnPowM : IndexedGrammar Bool

Indexed grammar which chooses a positive common run length and duplicates its stack.

Equations

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

A compositional soundness interpretation

theorem grammarAbnPowM_language : grammarAbnPowM.Language = abnPowM

The indexed grammar generates exactly the first witness language.

theorem abnPowM_is_Indexed : is_Indexed abnPowM

The language {(a b^n)^m | n,m >= 1} is indexed.