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

Words use the binary alphabet with false = a and true = b. Language-class membership facts live in the corresponding files under Langlib.Classes.

def varyingBlocks : List ℕ → List Bool

A sequence of a b* blocks whose individual b-run lengths are listed in ns.

Equations

• varyingBlocks [] = []
• varyingBlocks (n :: ns) = abBlock n ++ varyingBlocks ns

def abnAbStarPowPredN : Language Bool

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

Equations

• abnAbStarPowPredN w = ∃ (n : ℕ) (ns : List ℕ), 0 < n ∧ ns.length + 1 = n ∧ w = abBlock n ++ varyingBlocks ns

@[simp]

theorem varyingBlocks_append (xs ys : List ℕ) : varyingBlocks (xs ++ ys) = varyingBlocks xs ++ varyingBlocks ys

@[simp]

theorem count_false_varyingBlocks (ns : List ℕ) : List.count false (varyingBlocks ns) = ns.length

@[simp]

theorem varyingBlocks_replicate (n m : ℕ) : varyingBlocks (List.replicate m n) = blockPower n m