containsZero and containsOne: "contains-a-bit" languages

The strings containing at least one 0-bit (resp. 1-bit). Decided by a 3-state scannerTM instance: the scan state is a single Bool tracking "some bit seen so far equals target".

Main definitions

• Language.containsZero, Language.containsOne.
• TM.containsTM target — scannerTM specialized to target : Bool.

Main results

• containsZero_in_DTIME, containsOne_in_DTIME — both in DTIME(n + 2).
• containsZero_mem_P, containsOne_mem_P.

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

Scanner for "some input bit equals target". Scan state: a Bool encoding "some bit seen so far equals target".

Equations

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

def Complexity.Language.containsZero : Language

Strings containing at least one 0-bit.

Equations

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

def Complexity.Language.containsOne : Language

Strings containing at least one 1-bit.

Equations

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

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

containsZero ∈ DTIME(n + 2).

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

containsOne ∈ DTIME(n + 2).

theorem Complexity.containsZero_mem_P : Language.containsZero ∈ P

containsZero ∈ P.

theorem Complexity.containsOne_mem_P : Language.containsOne ∈ P

containsOne ∈ P.