allZeros and allOnes: single-symbol languages

The strings consisting entirely of 0s (resp. 1s), including the empty string. Decided by a 3-state scannerTM instance: the scan state is a single Bool tracking "every bit so far equals target".

Main definitions

• Language.allZeros, Language.allOnes.
• TM.allSymbolTM target — scannerTM specialized to target : Bool.

Main results

• allZeros_in_DTIME, allOnes_in_DTIME — both in DTIME(n + 2).
• allZeros_mem_P, allOnes_mem_P.

def Complexity.TM.allSymbolTM (target : Bool) : TM 0

Scanner for "all input bits equal target". Scan state: a Bool encoding "all bits seen so far equal target".

Equations

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

def Complexity.Language.allZeros : Language

Strings consisting entirely of 0-bits (including []).

Equations

• Complexity.Language.allZeros = {x : List Bool | ∀ b ∈ x, b = false}

def Complexity.Language.allOnes : Language

Strings consisting entirely of 1-bits (including []).

Equations

• Complexity.Language.allOnes = {x : List Bool | ∀ b ∈ x, b = true}

theorem Complexity.allZeros_in_DTIME : Language.allZeros ∈ DTIME fun (n : ℕ) => n + 2

allZeros ∈ DTIME(n + 2).

theorem Complexity.allOnes_in_DTIME : Language.allOnes ∈ DTIME fun (n : ℕ) => n + 2

allOnes ∈ DTIME(n + 2).

theorem Complexity.allZeros_mem_P : Language.allZeros ∈ P

allZeros ∈ P.

theorem Complexity.allOnes_mem_P : Language.allOnes ∈ P

allOnes ∈ P.