Helper lemmas about vocabularies and interpolants

theorem isPartInterpolant_of_mem_iff {Z Y : Sequent} {θ : Formula} (hl : ∀ (f : Formula), f ∈ Z.left ↔ f ∈ Y.left) (hr : ∀ (f : Formula), f ∈ Z.right ↔ f ∈ Y.right) (h : isPartInterpolant Y θ) : isPartInterpolant Z θ

Being an interpolant only depends on which formulas are in the two components.

Interpolants for PdlRules applied to free nodes

The only rule treated here is (L+), i.e. loadL and loadR.

def freePdlRuleInterpolant {X Y : Sequent} (r : PdlRule X Y) (Xfree : X.isFree) (θY : PartInterpolant Y) : PartInterpolant X

Equations

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

Interpolants for PdlRules applied to loaded nodes

The rules treated here are (L-), i.e. freeL and freeR, and the modal rule (M), i.e. modL and modR. This is the part of Lemma 9.1 in the paper that is about loaded nodes which form a singleton cluster.

theorem exists_itp_modL {A : ℕ} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Formula} (hXl : ∀ (f : Formula), f ∈ Xl ↔ f ∈ L ∨ f = ~⌈·A⌉ψ) (hXr : ∀ (f : Formula), f ∈ Xr ↔ f ∈ R) (hYl : ∀ (f : Formula), f ∈ Yl ↔ f = ~ψ ∨ f ∈ Finset.projection A L) (hYr : ∀ (f : Formula), f ∈ Yr ↔ f ∈ Finset.projection A R) (hvoc : θ.voc ⊆ Yl.fvoc ∩ Yr.fvoc) (hL : ¬HasSat.satisfiable ({~θ} ∪ Yl)) (hR : ¬HasSat.satisfiable ({θ} ∪ Yr)) : ∃ (ρ : Formula), ρ.voc ⊆ Xl.fvoc ∩ Xr.fvoc ∧ ¬HasSat.satisfiable ({~ρ} ∪ Xl) ∧ ¬HasSat.satisfiable ({ρ} ∪ Xr)

Interpolant for the modal rule (M) applied to a node loaded on the left. The lists Xl, Xr are the two components of the premise and Yl, Yr those of the conclusion, described by which formulas are in them. The interpolant is ~⌈·A⌉(~θ), unless the projection of the right component is empty, in which case the left component is unsatisfiable and we can use ⊥.

theorem exists_itp_modR {A : ℕ} {L R Xl Xr Yl Yr : Finset Formula} {ψ θ : Formula} (hXl : ∀ (f : Formula), f ∈ Xl ↔ f ∈ L) (hXr : ∀ (f : Formula), f ∈ Xr ↔ f ∈ R ∨ f = ~⌈·A⌉ψ) (hYl : ∀ (f : Formula), f ∈ Yl ↔ f ∈ Finset.projection A L) (hYr : ∀ (f : Formula), f ∈ Yr ↔ f = ~ψ ∨ f ∈ Finset.projection A R) (hvoc : θ.voc ⊆ Yl.fvoc ∩ Yr.fvoc) (hL : ¬HasSat.satisfiable ({~θ} ∪ Yl)) (hR : ¬HasSat.satisfiable ({θ} ∪ Yr)) : ∃ (ρ : Formula), ρ.voc ⊆ Xl.fvoc ∩ Xr.fvoc ∧ ¬HasSat.satisfiable ({~ρ} ∪ Xl) ∧ ¬HasSat.satisfiable ({ρ} ∪ Xr)

Interpolant for the modal rule (M) applied to a node loaded on the right. The interpolant is ⌈·A⌉θ, unless the projection of the left component is empty, in which case the right component is unsatisfiable and we can use ~⊥.

theorem loadedPdlRuleInterpolant {Z Y : Sequent} (r : PdlRule Z Y) (Zloaded : Z.isLoaded) (h : ∃ (θ : Formula), isPartInterpolant Y θ) : ∃ (ρ : Formula), isPartInterpolant Z ρ

Given an interpolant for the conclusion of a PdlRule applied to a loaded sequent, we get an interpolant for the premise. This is the loaded analogue of freePdlRuleInterpolant, covering the rules (L-) and (M).