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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Split.Split_to_CutPre {𝕏 : Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} : RuleApp → CutPre.RuleApp x τ

Equations

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

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

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

theorem Split.Split_to_CutPre_f {𝕏 : Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : RuleApp) : CutPre.f (Split_to_CutPre r) = f r

theorem Split.Split_to_CutPre_fₚ {𝕏 : Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : RuleApp) : CutPre.fₚ (Split_to_CutPre r) = fₚ r

theorem Split.Split_to_CutPre_fₙ {𝕏 : Proof} {x : 𝕏.X} {τ : 𝕏.X → SplitSequent} (r : RuleApp) : CutPre.fₙ (Split_to_CutPre r) = fₙ r

Partial Interpolation Proofs

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

theorem Split.PartialInterpolationLeft_eq_proves_eq {𝕏 : Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : CutPre.Proves x (PartialInterpolationLeft_eq x) (leftEquationSequent x)

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

Equations

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

theorem Split.PartialInterpolationLeft_proves_int {𝕏 : Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : CutPre.Proves x (PartialInterpolationLeft x) (leftInterpolantSequent x)

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

noncomputable def Split.InterpolantProofLeft {𝕏 : Proof} [fin_X : Fintype 𝕏.X] : SplitCut.Proof

Equations

• Split.InterpolantProofLeft = Split.ProofTransformation Split.PartialInterpolationLeft ⋯ ⋯

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

theorem Split.PartialInterpolationRight_eq_proves_eq {𝕏 : Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : CutPre.Proves x (PartialInterpolationRight_eq x) (rightEquationSequent x)

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

Equations

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

theorem Split.PartialInterpolationRight_proves_int {𝕏 : Proof} [fin_X : Fintype 𝕏.X] (x : 𝕏.X) : CutPre.Proves x (PartialInterpolationRight x) (rightInterpolantSequent x)

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

noncomputable def Split.InterpolantProofRight {𝕏 : Proof} [fin_X : Fintype 𝕏.X] : SplitCut.Proof

Equations

• Split.InterpolantProofRight = Split.ProofTransformation Split.PartialInterpolationRight ⋯ ⋯

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