KRF.theta_recursion

import Definitions.Def_KRF_Machinery
noncomputable section
open KRFCore
open KRFCore.FStruct
open KRF
variable {σD σQ : Sig}
/-- The canonical-KRF predicate (platform form of thetaKrf): the theory
engine mapping carried by the StarContract. -/
def IsTheta {σD σQ : Sig} {Q : QueryLanguage σQ} (c : Coding σD σQ)
    (S : StarContract σD σQ Q) (T : Krf σD σQ Q) : Prop :=
  ∃ hdom : T.dom = S.isTheory,
    ∀ (π : Nat) (h : S.isTheory π), ∀ D φ,
      T.Γ π (hdom ▸ h) D φ ↔ KM (S.theoryEngine h) D φ

theorem KRF.theta_recursion {Q : QueryLanguage σQ} (c : Coding σD σQ) (S : StarContract σD σQ Q)
    (p : Nat → Nat) (hp_dom : ∀ π, S.isTheory π → S.isTheory (p π)) :
    ∃ T : Krf σD σQ Q, ∃ hdom : T.dom = S.isTheory,
      (∀ (π₀ : Nat) (h₀ : S.isTheory π₀), ∀ D φ,
          T.Γ π₀ (hdom ▸ h₀) D φ ↔ KM (S.theoryEngine h₀) D φ) ∧
      ∃ π : Nat, ∃ h : S.isTheory π, ∀ D φ,
        T.Γ π (hdom ▸ h) D φ ↔ T.Γ (p π) (hdom ▸ (hp_dom π h)) D φ :=
  sorry