The language {(a b^n)^m | n,m >= 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 abBlock (n : ℕ) : List Bool

The binary block a b^n, with false = a and true = b.

Equations

• abBlock n = false :: List.replicate n true

def blockPower (n : ℕ) : ℕ → List Bool

m copies of the same block a b^n.

Equations

• blockPower n 0 = []
• blockPower n m.succ = abBlock n ++ blockPower n m

def abnPowM : Language Bool

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

Equations

• abnPowM w = ∃ (n : ℕ) (m : ℕ), 0 < n ∧ 0 < m ∧ w = blockPower n m

@[simp]

theorem blockPower_zero (n : ℕ) : blockPower n 0 = []

@[simp]

theorem blockPower_succ (n m : ℕ) : blockPower n (m + 1) = abBlock n ++ blockPower n m

theorem blockPower_add (n m k : ℕ) : blockPower n (m + k) = blockPower n m ++ blockPower n k

@[simp]

theorem count_false_abBlock (n : ℕ) : List.count false (abBlock n) = 1

@[simp]

theorem count_false_blockPower (n m : ℕ) : List.count false (blockPower n m) = m