coNL ⊆ NL

⚠️ Unreviewed by Bolton

The reverse half of the Immerman–Szelepcsényi theorem.

Either inclusion implies the other, and this file proves that reduction unconditionally: coNL is the complement class of NL, so complementing both sides of one inclusion produces the other. Only one direction therefore has to be proved by inductive counting — see NLSubsetCoNL.

Main results

• coNL_subset_NL_of_NL_subset_coNL, NL_subset_coNL_of_coNL_subset_NL — the two directions are equivalent
• NL_eq_coNL_of_NL_subset_coNL — either one settles NL = coNL

def Complexity.CoNLSubsetNL : Prop

coNL ⊆ NL (Immerman–Szelepcsényi).

Equations

• Complexity.CoNLSubsetNL = (Complexity.coNL ⊆ Complexity.NL)

theorem Complexity.coNL_subset_NL_of_NL_subset_coNL (h : NL ⊆ coNL) : coNL ⊆ NL

One inclusion gives the other: complementing Lᶜ ∈ NL turns membership in coNL into membership in NL.

theorem Complexity.NL_subset_coNL_of_coNL_subset_NL (h : coNL ⊆ NL) : NL ⊆ coNL

The mirror implication.

theorem Complexity.NL_eq_coNL_of_NL_subset_coNL (h : NL ⊆ coNL) : NL = coNL

Either inclusion settles the equality.