The second intersection witness is context-free

This file gives a context-free grammar for abnAbStarPowPredN = {a b^n (a b*)^(n-1) | n >= 1} and proves that it generates exactly that shared example language.

inductive AbnAbStarPowPredNNT : Type

• S : AbnAbStarPowPredNNT
• C : AbnAbStarPowPredNNT
• D : AbnAbStarPowPredNNT

instance instDecidableEqAbnAbStarPowPredNNT : DecidableEq AbnAbStarPowPredNNT

Equations

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

def grammarAbnAbStarPowPredN : CF_grammar Bool

Context-free grammar for a b^n (a b*)^(n-1), n >= 1.

Equations

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

Compositional soundness for the context-free grammar

theorem grammarAbnAbStarPowPredN_language : CF_language grammarAbnAbStarPowPredN = abnAbStarPowPredN

The context-free grammar generates exactly the second witness language.

theorem abnAbStarPowPredN_is_CF : is_CF abnAbStarPowPredN

The language a b^n (a b*)^(n-1), n >= 1, is context-free.