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) : pairLang (OrRelation R₁ 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.

theorem Complexity.orRelation_mem_FNP {R₁ R₂ : List Bool → List Bool → Prop} (hR₁ : R₁ ∈ FNP) (hR₂ : R₂ ∈ FNP) : OrRelation R₁ R₂ ∈ FNP

The disjunctive relation is in FNP when both components are.