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 Lean4GlCoalgebras.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

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

noncomputable def Lean4GlCoalgebras.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

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

noncomputable def Lean4GlCoalgebras.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

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

noncomputable def Lean4GlCoalgebras.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

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

def Lean4GlCoalgebras.splitToExt {𝕏 : 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

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

noncomputable def Lean4GlCoalgebras.partialLeftTopₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftTopᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftAxₗₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftAxₗᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftAxᵣₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftAxᵣᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftOrₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftOrᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftAndₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftAndᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftBoxₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialLeftBoxᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.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.

noncomputable def Lean4GlCoalgebras.partialRightTopₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightTopᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightAxₗₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightAxₗᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightAxᵣₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightAxᵣᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightOrₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightOrᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightAndₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightAndᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightBoxₗ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.partialRightBoxᵣ {𝕏 : 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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

noncomputable def Lean4GlCoalgebras.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.

noncomputable def Lean4GlCoalgebras.partialInterpolationLeftAlpha {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) (𝕐₂ : Split.Proof) (y₂ : 𝕐₂.X) : Unit ⊕ (partialEquationLeft x).X ⊕ 𝕐₂.X → (Ext.T x leftInterpolantSequent).obj (Unit ⊕ (partialEquationLeft x).X ⊕ 𝕐₂.X)

Carrier coalgebra of the cut-based left interpolation proof, abstracted over the right interpolant proof 𝕐₂ and its root y₂.

Equations

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

theorem Lean4GlCoalgebras.partialInterpolationLeftPath {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) (𝕐₂ : Split.Proof) (y₂ : 𝕐₂.X) (node : Unit ⊕ (partialEquationLeft x).X ⊕ 𝕐₂.X) (f : { f : ℕ → Unit ⊕ (partialEquationLeft x).X ⊕ 𝕐₂.X // f 0 = node ∧ ∀ (n : ℕ), Ext.edge (partialInterpolationLeftAlpha x 𝕐₂ y₂) (f n) (f (n + 1)) }) (n : ℕ) : ∃ (m : ℕ), (Ext.r (partialInterpolationLeftAlpha x 𝕐₂ y₂) (↑f (n + m))).isBox

The path field of the cut-based left interpolation proof: every infinite path through the combined coalgebra meets a box rule infinitely often.

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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 Lean4GlCoalgebras.partialInterpolationRightAlpha {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) (𝕐₂ : Split.Proof) (y₂ : 𝕐₂.X) : Unit ⊕ (partialEquationRight x).X ⊕ 𝕐₂.X → (Ext.T x rightInterpolantSequent).obj (Unit ⊕ (partialEquationRight x).X ⊕ 𝕐₂.X)

Carrier coalgebra of the cut-based right interpolation proof, abstracted over the right interpolant proof 𝕐₂ and its root y₂.

Equations

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

theorem Lean4GlCoalgebras.partialInterpolationRightPath {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) (𝕐₂ : Split.Proof) (y₂ : 𝕐₂.X) (node : Unit ⊕ (partialEquationRight x).X ⊕ 𝕐₂.X) (f : { f : ℕ → Unit ⊕ (partialEquationRight x).X ⊕ 𝕐₂.X // f 0 = node ∧ ∀ (n : ℕ), Ext.edge (partialInterpolationRightAlpha x 𝕐₂ y₂) (f n) (f (n + 1)) }) (n : ℕ) : ∃ (m : ℕ), (Ext.r (partialInterpolationRightAlpha x 𝕐₂ y₂) (↑f (n + m))).isBox

The path field of the cut-based right interpolation proof: every infinite path through the combined coalgebra meets a box rule infinitely often.

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

Auxiliary declaration used in the GL coalgebra development.

Equations

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

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

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

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

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

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

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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.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 Lean4GlCoalgebras.interpolantProofLeft {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] : ExtSkip.Proof

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

Equations

• Lean4GlCoalgebras.interpolantProofLeft = Lean4GlCoalgebras.proofTransformation Lean4GlCoalgebras.partialInterpolationLeft ⋯ ⋯

theorem Lean4GlCoalgebras.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)ʳ.

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

theorem Lean4GlCoalgebras.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 Lean4GlCoalgebras.interpolantProofRight {𝕏 : Split.Proof} [fin_X : Fintype 𝕏.X] : ExtSkip.Proof

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

Equations

• Lean4GlCoalgebras.interpolantProofRight = Lean4GlCoalgebras.proofTransformation Lean4GlCoalgebras.partialInterpolationRight ⋯ ⋯

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

Left syntactic interpolation result!

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

Right syntactic interpolation result!

theorem Lean4GlCoalgebras.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.