Boolean closure of stably computable predicates (CRN-3)

[AADFP06, §4.1, Lemma 3 and Corollary 2]: the stably computable predicates are closed under every 2-place Boolean function, by the parallel composition of two protocols. Its states are pairs (p₁, p₂), its input function is s ↦ (I₁ s, I₂ s), both components make their own transition in every encounter, and the output of (p₁, p₂) is ξ(O₁ p₁, O₂ p₂).

theorem Crn.StablyComputable.map₂ {X : Type u_1} [Fintype X] [DecidableEq X] {φ ψ : (X → ℕ) → Bool} (ξ : Bool → Bool → Bool) (hφ : StablyComputable φ) (hψ : StablyComputable ψ) : StablyComputable fun (x : X → ℕ) => ξ (φ x) (ψ x)

[AADFP06, Lemma 3] For every 2-place Boolean function ξ, if φ and ψ are stably computable then so is ξ(φ, ψ) (parallel composition).

theorem Crn.StablyComputable.not {X : Type u_1} [Fintype X] [DecidableEq X] {φ : (X → ℕ) → Bool} (hφ : StablyComputable φ) : StablyComputable fun (x : X → ℕ) => !φ x

Stably computable predicates are closed under negation [AADFP06, Corollary 2].

theorem Crn.StablyComputable.and {X : Type u_1} [Fintype X] [DecidableEq X] {φ ψ : (X → ℕ) → Bool} (hφ : StablyComputable φ) (hψ : StablyComputable ψ) : StablyComputable fun (x : X → ℕ) => φ x && ψ x

Stably computable predicates are closed under conjunction [AADFP06, Corollary 2].

theorem Crn.StablyComputable.or {X : Type u_1} [Fintype X] [DecidableEq X] {φ ψ : (X → ℕ) → Bool} (hφ : StablyComputable φ) (hψ : StablyComputable ψ) : StablyComputable fun (x : X → ℕ) => φ x || ψ x

Stably computable predicates are closed under disjunction [AADFP06, Corollary 2].