Partition Interpolants

def isPartInterpolant (X : Sequent) (θ : Formula) : Prop

Equations

• isPartInterpolant X θ = (θ.voc ⊆ jvoc X ∧ ¬HasSat.satisfiable ({~θ} ∪ X.left) ∧ ¬HasSat.satisfiable ({θ} ∪ X.right))

def PartInterpolant (N : Sequent) : Type

Equations

• PartInterpolant N = Subtype (isPartInterpolant N)

Interpolants for local rules

theorem LoadRule.voc {χ : LoadFormula} {ress : Finset (Finset Formula × Option NegLoadFormula)} (lr : LoadRule (~'χ) ress) : lfovocFin ress ⊆ χ.voc

theorem localRule_does_not_increase_vocab_L {Cond : Sequent} {B : Finset Sequent} (rule : LocalRule Cond B) (res : Sequent) : res ∈ B → res.left.fvoc ⊆ Cond.left.fvoc

theorem localRule_does_not_increase_vocab_R {Cond : Sequent} {B : Finset Sequent} (rule : LocalRule Cond B) (res : Sequent) : res ∈ B → res.right.fvoc ⊆ Cond.right.fvoc

theorem localRuleApp_does_not_increase_jvoc (lra : LocalRuleApp) (Y : Sequent) : Y ∈ lra.C → jvoc Y ⊆ jvoc lra.X

def localInterpolantStep (lra : LocalRuleApp) (subθs : (c : Sequent) → c ∈ lra.C → PartInterpolant c) : PartInterpolant lra.X

Maehara's method for single-step local rule applications. This covers easy cases without any loaded path repeats. We do not use localRuleTruth to prove this, but the more specific lemmas oneSidedL_sat_down and oneSidedL_sat_down.

Equations

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

Interpolants for Local Tableau

def LocalTableau.interpolant {X : Sequent} (ltX : LocalTableau X) (endθs : (Y : Sequent) → Y ∈ endNodesOf ltX → PartInterpolant Y) : PartInterpolant X

Equations

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