FNP and TFNP — Internal proofs #
Helper lemmas for OrRelation used by the surface-layer theorem
orRelation_mem_TFNP_of_NP_coNP_witnesses.
theorem
Complexity.polyBalanced_orRelation
{R₁ R₂ : List Bool → List Bool → Prop}
(h₁ : PolyBalanced R₁)
(h₂ : PolyBalanced R₂)
:
PolyBalanced (OrRelation R₁ R₂)
The combined relation is polynomially balanced when both components are.
theorem
Complexity.pairLang_orRelation_mem_P
{R₁ R₂ : List Bool → List Bool → Prop}
(h₁ : pairLang R₁ ∈ P)
(h₂ : pairLang R₂ ∈ P)
:
If both pair languages are in P, so is the pair language of the combined
relation. Since OrRelation R₁ R₂ = R₁ ∨ R₂, the pair language is
pairLang R₁ ∪ pairLang R₂, and P is closed under union.