noncomputable def leftInterpolantSequent {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : SplitSequent

Given a node x, defines what the root of the left interpolation proof should look like, i.e. f(x)ˡ ∣ ιₓ in on paper work.

Equations

• leftInterpolantSequent x = {Sum.inr (interpolant 𝕏 (at encodeVar x))} ∪ (Split.f (Split.r 𝕏.α x)).filterLeft

noncomputable def leftEquationSequent {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : SplitSequent

Given a node x, defines what the same as above except for the equation σ(χₓ), helpful for cases where the interpolant isn't defined by the interpolants of its premise nodes., i.e. f(x)ˡ ∣ σ(χₓ) in on paper work.

Equations

• leftEquationSequent x = {Sum.inr (interpolant 𝕏 (equation x))} ∪ (Split.f (Split.r 𝕏.α x)).filterLeft

noncomputable def rightInterpolantSequent {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : SplitSequent

Given a node x, defines what the root of the right interpolation proof should look like, i.e. ~ιₓ ∣ f(x)ʳ in on paper work.

Equations

• rightInterpolantSequent x = {Sum.inl (~interpolant 𝕏 (at encodeVar x))} ∪ (Split.f (Split.r 𝕏.α x)).filterRight

noncomputable def rightEquationSequent {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : SplitSequent

Given a node x, defines what the same as above except for the equation σ(χₓ), helpful for cases where the interpolant isn't defined by the interpolants of its premise nodes., i.e. ~σ(χₓ) ∣ f(x)ʳ in on paper work.

Equations

• rightEquationSequent x = {Sum.inl (~interpolant 𝕏 (equation x))} ∪ (Split.f (Split.r 𝕏.α x)).filterRight

def Split_to_Ext {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} : Split.RuleApp → Ext.RuleApp x τ

Transforms rule applications in the split system into applications in the extended system.

Equations

• Split_to_Ext (Split.RuleApp.topₗ Δ in_Δ) = Ext.RuleApp.topₗ Δ in_Δ
• Split_to_Ext (Split.RuleApp.topᵣ Δ in_Δ) = Ext.RuleApp.topᵣ Δ in_Δ
• Split_to_Ext (Split.RuleApp.axₗₗ Δ n in_Δ) = Ext.RuleApp.axₗₗ Δ n in_Δ
• Split_to_Ext (Split.RuleApp.axₗᵣ Δ n in_Δ) = Ext.RuleApp.axₗᵣ Δ n in_Δ
• Split_to_Ext (Split.RuleApp.axᵣₗ Δ n in_Δ) = Ext.RuleApp.axᵣₗ Δ n in_Δ
• Split_to_Ext (Split.RuleApp.axᵣᵣ Δ n in_Δ) = Ext.RuleApp.axᵣᵣ Δ n in_Δ
• Split_to_Ext (Split.RuleApp.orₗ Δ A B in_Δ) = Ext.RuleApp.orₗ Δ A B in_Δ
• Split_to_Ext (Split.RuleApp.orᵣ Δ A B in_Δ) = Ext.RuleApp.orᵣ Δ A B in_Δ
• Split_to_Ext (Split.RuleApp.andₗ Δ A B in_Δ) = Ext.RuleApp.andₗ Δ A B in_Δ
• Split_to_Ext (Split.RuleApp.andᵣ Δ A B in_Δ) = Ext.RuleApp.andᵣ Δ A B in_Δ
• Split_to_Ext (Split.RuleApp.boxₗ Δ A in_Δ) = Ext.RuleApp.boxₗ Δ A in_Δ
• Split_to_Ext (Split.RuleApp.boxᵣ Δ A in_Δ) = Ext.RuleApp.boxᵣ Δ A in_Δ

theorem Split_to_Ext_isBox {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : Split.RuleApp) : r.isBox → (Split_to_Ext r).isBox

theorem Split_to_Ext_notNonAxLeaf {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : Split.RuleApp) : ¬(Split_to_Ext r).isNonAxLeaf

theorem Split_to_Ext_f {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : Split.RuleApp) : Ext.f (Split_to_Ext r) = Split.f r

theorem Split_to_Ext_fₚ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : Split.RuleApp) : Ext.fₚ (Split_to_Ext r) = Split.fₚ r

theorem Split_to_Ext_fₙ {𝕏 : Split.Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : Split.RuleApp) : Ext.fₙ (Split_to_Ext r) = Split.fₙ r

Partial Left Interpolation Proofs

All of the left and right partial interpolation proofs, split apart based on rule application. These are split apart since otherwise the file runs very slow.

noncomputable def partialLeft_topₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {in_Δ : Sum.inl ⊤ ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.topₗ Δ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• partialLeft_topₗ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.topₗ (leftEquationSequent x) ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialLeft_topᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {in_Δ : Sum.inr ⊤ ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.topᵣ Δ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• partialLeft_topᵣ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.topᵣ (leftEquationSequent x) ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialLeft_axₗₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inl (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axₗₗ Δ n in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• partialLeft_axₗₗ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.axₗₗ (leftEquationSequent x) n ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialLeft_axₗᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inl (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axₗᵣ Δ n in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• partialLeft_axₗᵣ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.axₗᵣ (leftEquationSequent x) n ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialLeft_axᵣₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inr (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axᵣₗ Δ n in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• partialLeft_axᵣₗ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.axᵣₗ (leftEquationSequent x) n ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialLeft_axᵣᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inr (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axᵣᵣ Δ n in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• partialLeft_axᵣᵣ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.topᵣ (leftEquationSequent x) ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialLeft_orₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inl (φ v ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.orₗ Δ φ ψ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialLeft_orᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inr (φ v ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.orᵣ Δ φ ψ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialLeft_andₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inl (φ&ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.andₗ Δ φ ψ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialLeft_andᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inr (φ&ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.andᵣ Δ φ ψ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialLeft_boxₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ : Formula} {in_Δ : Sum.inl (□φ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.boxₗ Δ φ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialLeft_boxᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ : Formula} {in_Δ : Sum.inr (□φ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.boxᵣ Δ φ in_Δ) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialEquationLeft {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.PreProof x leftInterpolantSequent

Defines the left partial interpolation proof Lₓ.

Equations

• One or more equations did not get rendered due to their size.

theorem partialEquationLeft_proves_eq {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.Proves x (partialEquationLeft x) (leftEquationSequent x)

noncomputable def partialInterpolationLeft {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.PreProof x leftInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

theorem partialInterpolationLeft_proves_int {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.Proves x (partialInterpolationLeft x) (leftInterpolantSequent x)

Every left partial interpolation proof Lₓ proves f(x)ˡ ∣ ιₓ.

theorem partialInterpolationLeft_box_prop {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : (Split.r 𝕏.α x).isBox → ∀ (n : ℕ) (f : Fin (n + 1) → (partialInterpolationLeft x).X), f 0 = (partialInterpolationLeft x).root → (Ext.r (partialInterpolationLeft x).α (f ⟨n, ⋯⟩)).isNonAxLeaf → (∀ (m : Fin n), Ext.edge (partialInterpolationLeft x).α (f m.castSucc) (f m.succ)) → ∃ (m : Fin (n + 1)), (Ext.r (partialInterpolationLeft x).α (f m)).isBox

For every x in a finite split proof, the partial left interpolation proof associated with x has the property that on every path from the root to a non-axiomatic leaf, the box rule is applied on this path.

noncomputable def interpolantProofLeft {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] : ExtSkip.Proof

Defining the left interpolation proof with all non-axiomatic nodes removed.

Equations

• interpolantProofLeft = proofTransformation partialInterpolationLeft ⋯ ⋯

theorem interpolantProofLeft_proves_interpolant {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : interpolantProofLeft⊢leftInterpolantSequent x

Left syntactic interpolation result!

Partial Left Interpolation Proofs

All of the left and right partial interpolation proofs, split apart based on rule application. These are split apart since otherwise the file runs very slow.

noncomputable def partialRight_topₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {in_Δ : Sum.inl ⊤ ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.topₗ Δ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• partialRight_topₗ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.topₗ (rightEquationSequent x) ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialRight_topᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {in_Δ : Sum.inr ⊤ ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.topᵣ Δ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• partialRight_topᵣ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.topᵣ (rightEquationSequent x) ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialRight_axₗₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inl (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axₗₗ Δ n in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• partialRight_axₗₗ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.topₗ (rightEquationSequent x) ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialRight_axₗᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inl (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axₗᵣ Δ n in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• partialRight_axₗᵣ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.axₗᵣ (rightEquationSequent x) n ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialRight_axᵣₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inr (at n) ∈ Δ ∧ Sum.inl (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axᵣₗ Δ n in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• partialRight_axᵣₗ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.axᵣₗ (rightEquationSequent x) n ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialRight_axᵣᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {n : ℕ} {in_Δ : Sum.inr (at n) ∈ Δ ∧ Sum.inr (na n) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.axᵣᵣ Δ n in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• partialRight_axᵣᵣ x rule_def = { X := Unit, α := fun (u : Unit) => (Ext.RuleApp.axᵣᵣ (rightEquationSequent x) n ⋯, ∅), root := (), step := partialLeft_topₗ._proof_2, path := ⋯ }

noncomputable def partialRight_orₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inl (φ v ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.orₗ Δ φ ψ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialRight_orᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inr (φ v ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.orᵣ Δ φ ψ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialRight_andₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inl (φ&ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.andₗ Δ φ ψ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialRight_andᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ ψ : Formula} {in_Δ : Sum.inr (φ&ψ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.andᵣ Δ φ ψ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialRight_boxₗ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ : Formula} {in_Δ : Sum.inl (□φ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.boxₗ Δ φ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialRight_boxᵣ {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) {Δ : SplitSequent} {φ : Formula} {in_Δ : Sum.inr (□φ) ∈ Δ} (rule_def : Split.r 𝕏.α x = Split.RuleApp.boxᵣ Δ φ in_Δ) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

noncomputable def partialEquationRight {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.PreProof x rightInterpolantSequent

Defines the right partial interpolation proof Rₓ.

Equations

• One or more equations did not get rendered due to their size.

theorem partialEquationRight_proves_eq {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.Proves x (partialEquationRight x) (rightEquationSequent x)

Every right partial interpolation proof Rₓ proves ~ιₓ ∣ f(x)ʳ.

noncomputable def partialInterpolationRight {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.PreProof x rightInterpolantSequent

Equations

• One or more equations did not get rendered due to their size.

theorem partialInterpolationRight_proves_int {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : Ext.Proves x (partialInterpolationRight x) (rightInterpolantSequent x)

theorem partialInterpolationRight_box_prop {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : (Split.r 𝕏.α x).isBox → ∀ (n : ℕ) (f : Fin (n + 1) → (partialInterpolationRight x).X), f 0 = (partialInterpolationRight x).root → (Ext.r (partialInterpolationRight x).α (f ⟨n, ⋯⟩)).isNonAxLeaf → (∀ (m : Fin n), Ext.edge (partialInterpolationRight x).α (f m.castSucc) (f m.succ)) → ∃ (m : Fin (n + 1)), (Ext.r (partialInterpolationRight x).α (f m)).isBox

For every x in a finite split proof, the partial left interpolation proof associated with x has the property that on every path from the root to a non-axiomatic leaf, the box rule is applied on this path.

noncomputable def interpolantProofRight {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] : ExtSkip.Proof

Defining the right interpolation proof with all non-axiomatic nodes removed.

Equations

• interpolantProofRight = proofTransformation partialInterpolationRight ⋯ ⋯

theorem interpolantProofRight_proves_interpolant {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : interpolantProofRight⊢rightInterpolantSequent x

Right syntactic interpolation result!

theorem syntactic_interpolation {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : (interpolantProofLeft⊢leftInterpolantSequent x) ∧ (interpolantProofRight⊢rightInterpolantSequent x)

Given a finite split proof, interpolantProofLeft proves the left interpolation correctness statement and interpolantProofRight proves the right interpolation correctness statement.