Langlib

Langlib.Examples.AbnPowN

The diagonal language {(a b^n)^n | n >= 1} #

The two shared positive block witnesses abnPowM and abnAbStarPowPredN meet in exactly this language. Language-class membership facts live in the corresponding files under Langlib.Classes.

source
def abnPowN :
Language Bool

The language {(a b^n)^n | n >= 1}.

Equations
Instances For
    source
    theorem abnPowM_inter_abnAbStarPowPredN :
    abnPowM ⊓ abnAbStarPowPredN = abnPowN

    The two positive witness languages meet in exactly {(a b^n)^n | n >= 1}.