Sequents

Optional loaded formulas (Olfs)

@[reducible, inline]

abbrev Olf : Type

In nodes we optionally have a negated loaded formula on the left or right.

Equations

• Olf = Option (NegLoadFormula ⊕ NegLoadFormula)

def Olf.voc : Olf → Vocab

Equations

• Olf.voc none = ∅
• Olf.voc (some (Sum.inl nlf)) = nlf.voc
• Olf.voc (some (Sum.inr nlf)) = nlf.voc

def Olf.L : Olf → List Formula

Equations

• Olf.L none = []
• Olf.L (some (Sum.inl (~'lf))) = [~lf.unload]
• Olf.L (some (Sum.inr val)) = []

@[simp]

theorem Olf.L_none : L none = []

@[simp]

theorem Olf.L_inr {lf : NegLoadFormula} : L (some (Sum.inr lf)) = []

@[simp]

theorem Olf.L_map_inr {olf : Option NegLoadFormula} : L (Option.map Sum.inr olf) = []

@[simp]

theorem Olf.L_inl {lf : NegLoadFormula} : L (some (Sum.inl lf)) = [~lf.1.unload]

def Olf.R : Olf → List Formula

Equations

• Olf.R none = []
• Olf.R (some (Sum.inl val)) = []
• Olf.R (some (Sum.inr (~'lf))) = [~lf.unload]

@[simp]

theorem Olf.R_none : R none = []

@[simp]

theorem Olf.R_inl {lf : NegLoadFormula} : R (some (Sum.inl lf)) = []

@[simp]

theorem Olf.R_map_inl {olf : Option NegLoadFormula} : R (Option.map Sum.inl olf) = []

@[simp]

theorem Olf.R_inr {lf : NegLoadFormula} : R (some (Sum.inr lf)) = [~lf.1.unload]

instance Option.instHasSubsetOption {α : Type u_1} : HasSubset (Option α)

Equations

• Option.instHasSubsetOption = { Subset := fun (o1 o2 : Option α) => match o1, o2 with | none, x => True | some val, none => False | some f, some g => f = g }

@[simp]

theorem Option.some_subseteq {α : Type u_1} {x : α} {O : Option α} : some x ⊆ O ↔ some x = O

instance Option.insHasSdiff {α : Type u_1} [DecidableEq α] : SDiff (Option α)

Instance that is used to say (O : Olf) \ (O' : Olf).

Equations

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

@[simp]

theorem Option.insHasSdiff_none {α : Type u_1} {o : Option α} [DecidableEq α] : none \ o = none

@[simp]

theorem Option.insHasSdiff_remove_none_cancel {α : Type u_1} {o : Option α} [DecidableEq α] : o \ none = o

@[simp]

theorem Option.insHasSdiff_remove_sem_eq_none {α : Type u_1} {x : α} [DecidableEq α] : some x \ some x = none

def Option.overwrite {α : Type u_1} : Option α → Option α → Option α

Equations

• x✝.overwrite none = x✝
• x✝.overwrite (some x_3) = some x_3

def Olf.change (oldO Ocond newO : Olf) : Olf

Equations

• oldO.change Ocond newO = Option.overwrite (oldO \ Ocond) newO

@[simp]

theorem Olf.change_old_none_none {oldO : Olf} : oldO.change none none = oldO

@[simp]

theorem Olf.change_none_none_new {newO : Olf} : change none none newO = newO

@[simp]

theorem Olf.change_some {oldO whatever : Olf} {wnlf : NegLoadFormula ⊕ NegLoadFormula} : oldO.change whatever (some wnlf) = some wnlf

@[simp]

theorem Olf.change_some_some_eq {nχ : NegLoadFormula ⊕ NegLoadFormula} {Onew : Olf} : change (some nχ) (some nχ) Onew = Onew

def Olf.isNone : Olf → Prop

Equations

• Olf.isNone none = True
• Olf.isNone (some (Sum.inl nlf)) = False
• Olf.isNone (some (Sum.inr nlf)) = False

def Olf.isLeft : Olf → Prop

Equations

• Olf.isLeft none = False
• Olf.isLeft (some (Sum.inl nlf)) = True
• Olf.isLeft (some (Sum.inr nlf)) = False

def Olf.isRight : Olf → Prop

Equations

• Olf.isRight none = False
• Olf.isRight (some (Sum.inl nlf)) = False
• Olf.isRight (some (Sum.inr nlf)) = True

Sequents and their (multi)set quality

def Sequent : Type

A tableau node is labelled with two lists of formulas and an Olf. Each formula is placed on the left or right and up to one formula may be loaded.

Equations

• Sequent = (List Formula × List Formula × Olf)

instance instDecidableEqSequent : DecidableEq Sequent

Equations

• instDecidableEqSequent a b = instDecidableEqProd a b

instance instReprSequent : Repr Sequent

Equations

• instReprSequent = instReprProdOfReprTuple

def Sequent.setEqTo : Sequent → Sequent → Prop

Two Sequents are set-equal when their components are finset-equal. That is, we do not care about the order of the lists, but we do care about the side of the formula and what formual is loaded. Hint: use List.toFinset.ext_iff with this.

Equations

• Sequent.setEqTo (L, R, O) (L', R', O') = (L.toFinset = L'.toFinset ∧ R.toFinset = R'.toFinset ∧ O = O')

instance Sequent.instDecidableSetEqTo (x✝ x✝¹ : Sequent) : Decidable (x✝.setEqTo x✝¹)

Equations

• x✝¹.instDecidableSetEqTo x✝ = instDecidableAnd

instance instDecidableRelSequentSetEqTo : DecidableRel Sequent.setEqTo

Equations

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

def equivalenceSequentSetEqTo : Equivalence Sequent.setEqTo

Equations

• equivalenceSequentSetEqTo = ⋯

instance instSetoidSequent : Setoid Sequent

Equations

• instSetoidSequent = { r := Sequent.setEqTo, iseqv := equivalenceSequentSetEqTo }

@[reducible, inline]

abbrev Seqt : Type

Yes, it's a pun. A Sequent modulo Sequent.setEqTo.

Equations

• Seqt = Quotient instSetoidSequent

instance instDecidableEqSeqt : DecidableEq Seqt

Needed to make List.toFinset work for List Seqt. Strange that this is not inferred from instDecidableRelSequentSetEqTo automatically.

Equations

• instDecidableEqSeqt = Quotient.decidableEq

def Sequent.multisetEqTo : Sequent → Sequent → Prop

Two Sequents are multiset-equal when their components are multiset-equal. That is, we do not care about the order of the lists, but we do care about the side on which the formula is, whether it is loaded or not, and how often it occurs.

Equations

• Sequent.multisetEqTo (L, R, O) (L', R', O') = (↑L = ↑L' ∧ ↑R = ↑R' ∧ O = O')

instance instDecidableRelSequentMultisetEqTo : DecidableRel Sequent.multisetEqTo

Equations

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

theorem Sequent.setEqTo_of_multisetEqTo (X Y : Sequent) : X.multisetEqTo Y → X.setEqTo Y

@[simp]

theorem Sequent.setEqTo_refl (X : Sequent) : X.setEqTo X

theorem Sequent.setEqTo_symm (X Y : Sequent) : X.setEqTo Y ↔ Y.setEqTo X

theorem Sequent.setEqTo_trans (X Y Z : Sequent) : X.setEqTo Y → Y.setEqTo Z → X.setEqTo Z

@[simp]

theorem Sequent.multisetEqTo_refl (X : Sequent) : X.multisetEqTo X

theorem Sequent.multisetEqTo_symm (X Y : Sequent) : X.multisetEqTo Y ↔ Y.multisetEqTo X

def Sequent.toFinset : Sequent → Finset Formula

Equations

• Sequent.toFinset (L, R, O) = L.toFinset ∪ R.toFinset ∪ (Option.map (Sum.elim negUnload negUnload) O).toFinset

Components and sides of sequents

def Sequent.L : Sequent → List Formula

Equations

• Sequent.L (L, R, O) = L

def Sequent.R : Sequent → List Formula

Equations

• Sequent.R (L, R, O) = R

def Sequent.O : Sequent → Olf

Equations

• Sequent.O (L, R, O) = O

@[simp]

theorem Sequent.L_eq {L R : List Formula} {O : Olf} : Sequent.L (L, R, O) = L

@[simp]

theorem Sequent.R_eq {L R : List Formula} {O : Olf} : Sequent.R (L, R, O) = R

@[simp]

theorem Sequent.O_eq {L R : List Formula} {O : Olf} : Sequent.O (L, R, O) = O

def Sequent.left (X : Sequent) : List Formula

Equations

• X.left = X.L ++ X.O.L

def Sequent.right (X : Sequent) : List Formula

Equations

• X.right = X.R ++ X.O.R

def Sequent.bothSides (X : Sequent) : List Formula

Equations

• X.bothSides = X.left ++ X.right

@[simp]

theorem Sequent.left_eq {L R : List Formula} {O : Olf} : left (L, R, O) = L ++ O.L

@[simp]

def Sequent.right_eq {L R : List Formula} {O : Olf} : right (L, R, O) = R ++ O.R

Equations

• ⋯ = ⋯

@[simp]

def Sequent.bothSides_eq {L R : List Formula} {O : Olf} : bothSides (L, R, O) = L ++ O.L ++ R ++ O.R

Equations

• ⋯ = ⋯

(Joint) vocabulary of sequents

def onlfvoc : Option NegLoadFormula → Vocab

Like Olf.voc but without the ⊕ inside.

Equations

• onlfvoc none = ∅
• onlfvoc (some nlf) = nlf.voc

def lfovoc (L : List (List Formula × Option NegLoadFormula)) : Vocab

Equations

• lfovoc L = L.toFinset.sup fun (x : List Formula × Option NegLoadFormula) => match x with | (fs, o) => fs.fvoc ∪ onlfvoc o

def jvoc (X : Sequent) : Vocab

The joint vocabulary occurring on both the left and the right side.

Equations

• jvoc X = X.left.fvoc ∩ X.right.fvoc

theorem jvoc_sub_of_voc_sub {Y X : Sequent} (hl : Y.left.fvoc ⊆ X.left.fvoc) (hr : Y.right.fvoc ⊆ X.right.fvoc) : jvoc Y ⊆ jvoc X

Formulas as elements of sequents

instance instMembershipFormulaSequent : Membership Formula Sequent

Equations

• instMembershipFormulaSequent = { mem := fun (X : Sequent) (φ : Formula) => φ ∈ X.L ∨ φ ∈ X.R }

instance instDecidableMemFormulaSequent {φ : Formula} {X : Sequent} : Decidable (φ ∈ X)

Equations

• instDecidableMemFormulaSequent = Prod.casesOn X fun (L : List Formula) (snd : List Formula × Olf) => Prod.casesOn snd fun (R : List Formula) (o : Olf) => id inferInstance

instance instFintypeSubtypeMemSequent {X : Sequent} : Fintype { x : Formula // x ∈ X }

Equations

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

def NegLoadFormula.mem_Sequent (X : Sequent) (nlf : NegLoadFormula) : Prop

Equations

• NegLoadFormula.mem_Sequent X nlf = (X.O = some (Sum.inl nlf) ∨ X.O = some (Sum.inr nlf))

instance instDecidableMem_SequentMkListFormulaProdOlf {L R : List Formula} {O : Olf} {nlf : NegLoadFormula} : Decidable (NegLoadFormula.mem_Sequent (L, R, O) nlf)

Equations

• instDecidableMem_SequentMkListFormulaProdOlf = if h : O = some (Sum.inl nlf) then isTrue ⋯ else if h2 : O = some (Sum.inr nlf) then isTrue ⋯ else isFalse ⋯

instance instMembershipNegLoadFormulaSequent : Membership NegLoadFormula Sequent

Equations

• instMembershipNegLoadFormulaSequent = { mem := NegLoadFormula.mem_Sequent }

def AnyNegFormula.mem_Sequent (X : Sequent) (anf : AnyNegFormula) : Prop

Equations

• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.normal φ)) = (~φ ∈ x✝)
• AnyNegFormula.mem_Sequent x✝ (~''(AnyFormula.loaded χ)) = ((~'χ) ∈ x✝)

instance instMembershipAnyNegFormulaSequent : Membership AnyNegFormula Sequent

Equations

• instMembershipAnyNegFormulaSequent = { mem := AnyNegFormula.mem_Sequent }

Closed, basic, loaded and free sequents

def Sequent.closed (X : Sequent) : Prop

A sequent is closed iff it contains ⊥ or contains a formula and its negation.

Equations

• X.closed = (⊥ ∈ X ∨ ∃ f ∈ X, ~f ∈ X)

def Sequent.basic : Sequent → Prop

A sequent is basic iff it only contains basic formulas and is not closed.

Equations

• Sequent.basic (L, R, O) = ((∀ f ∈ L ++ R ++ (Option.map (Sum.elim negUnload negUnload) O).toList, f.basic = true) ∧ ¬Sequent.closed (L, R, O))

instance Fintype.decidableExistsConjFintype {α : Type u_1} {p q : α → Prop} [DecidablePred q] [Fintype (Subtype p)] : Decidable (∃ (a : α), p a ∧ q a)

A variant of Fintype.decidableExistsFintype, used by instDecidableClosed.

Equations

• Fintype.decidableExistsConjFintype = if h : ∃ (x : Subtype p), q ↑x then isTrue ⋯ else isFalse ⋯

instance Sequent.instDecidableClosed {X : Sequent} : Decidable X.closed

Equations

• Sequent.instDecidableClosed = id (if h : ⊥ ∈ X then isTrue ⋯ else if h_1 : ∃ f ∈ X, ~f ∈ X then isTrue ⋯ else isFalse ⋯)

instance instDecidableBasic {X : Sequent} : Decidable X.basic

Equations

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

def Sequent.isLoaded : Sequent → Bool

Equations

• Sequent.isLoaded (fst, fst_1, none) = decide False
• Sequent.isLoaded (fst, fst_1, some val) = decide True

def Sequent.isFree (Γ : Sequent) : Bool

Equations

• Γ.isFree = decide ¬Γ.isLoaded = true

@[simp]

theorem Sequent.none_isFree (L R : List Formula) : isFree (L, R, none) = true

@[simp]

theorem Sequent.some_not_isFree (L R : List Formula) (olf : NegLoadFormula ⊕ NegLoadFormula) : ¬isFree (L, R, some olf) = true

theorem setEqTo_isLoaded_iff {X Y : Sequent} (h : X.setEqTo Y) : X.isLoaded = Y.isLoaded

theorem Sequent.mem_iff_of_setEqTo {X Y : Sequent} (h : X.setEqTo Y) (f : Formula) : f ∈ X ↔ f ∈ Y

Set-equal sequents have the same members.

theorem Sequent.closed_iff_of_setEqTo {X Y : Sequent} (h : X.setEqTo Y) : X.closed ↔ Y.closed

Set-equal sequents are closed together.

theorem Sequent.basic_iff_of_setEqTo {X Y : Sequent} (h : X.setEqTo Y) : X.basic ↔ Y.basic

Set-equal sequents are basic together.

theorem multisetEqTo_isLoaded_iff {X Y : Sequent} (h : X.multisetEqTo Y) : X.isLoaded = Y.isLoaded

Semantics of sequents

instance modelCanSemImplySequent {W : Type} : vDash (KripkeModel W × W) Sequent

Equations

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

instance modelCanSemImplyLLO {W : Type} : vDash (KripkeModel W × W) (List Formula × List Formula × Olf)

Equations

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

instance instSequentHasSat : HasSat Sequent

Equations

• instSequentHasSat = { satisfiable := fun (Δ : Sequent) => ∃ (W : Type) (M : KripkeModel W) (w : W), (M, w) ⊨ Δ }

theorem tautImp_iff_SequentUnsat {φ ψ : Formula} {X : Sequent} : X = ([φ], [~ψ], none) → (tautology (~(φ ⋀ ~ψ)) ↔ ¬HasSat.satisfiable X)

theorem vDash_setEqTo_iff {W : Type} {X Y : Sequent} (h : X.setEqTo Y) (M : KripkeModel W) (w : W) : (M, w) ⊨ X ↔ (M, w) ⊨ Y

theorem vDash_multisetEqTo_iff {W : Type} {X Y : Sequent} (h : X.multisetEqTo Y) (M : KripkeModel W) (w : W) : (M, w) ⊨ X ↔ (M, w) ⊨ Y

Removing loaded formulas from sequents

def Sequent.without (LRO : Sequent) (naf : AnyNegFormula) : Sequent

Equations

• Sequent.without (L, R, O) (~''(AnyFormula.normal f)) = (L \ {~f}, R \ {~f}, O)
• Sequent.without (L, R, O) (~''(AnyFormula.loaded lf)) = if NegLoadFormula.mem_Sequent (L, R, O) (~'lf) then (L, R, none) else (L, R, O)

@[simp]

theorem Sequent.without_normal_isFree_iff_isFree {φ : Formula} (LRO : Sequent) : (LRO.without (~''(AnyFormula.normal φ))).isFree = true ↔ LRO.isFree = true

@[simp]

theorem Sequent.isFree_then_without_isFree (LRO : Sequent) : LRO.isFree = true → ∀ (anf : AnyNegFormula), (LRO.without anf).isFree = true

theorem Sequent.without_loadBoxes_isFree_of_eq_inl {αs : List Program} {d : Program} {L R : List Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inl (~'⌊⌊d :: δs⌋⌋χ))) (~''(AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadBoxes_isFree_of_eq_inr {αs : List Program} {d : Program} {L R : List Formula} {δs : List Program} {χ : LoadFormula} {φ : Formula} (h : AnyFormula.loaded χ = AnyFormula.loadBoxes αs (AnyFormula.normal φ)) : (without (L, R, some (Sum.inr (~'⌊⌊d :: δs⌋⌋χ))) (~''(AnyFormula.loadBoxes (d :: (δs ++ αs)) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inl {d : Program} {δ_β : List Program × Program} {L R : List Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inl (~'loadMulti δ_β.1 δ_β.2 φ))) (~''(AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree = true

theorem Sequent.without_loadMulti_isFree_of_splitLast_cons_inr {d : Program} {δ_β : List Program × Program} {L R : List Formula} {δs : List Program} {φ : Formula} (h : splitLast (d :: δs) = some δ_β) : (without (L, R, some (Sum.inr (~'loadMulti δ_β.1 δ_β.2 φ))) (~''(AnyFormula.loadBoxes (d :: δs) (AnyFormula.normal φ)))).isFree = true

inductive Side : Type

• LL : Side
• RR : Side

def sideOf {α : Type u_1} : α ⊕ α → Side

Equations

• sideOf (Sum.inl val) = Side.LL
• sideOf (Sum.inr val) = Side.RR

def AnyNegFormula.in_side (anf : AnyNegFormula) : Side → (X : Sequent) → Prop

Equations

• (~''(AnyFormula.normal φ)).in_side Side.LL (L, fst, snd) = (~φ ∈ L)
• (~''(AnyFormula.normal φ)).in_side Side.RR (fst, R, snd) = (~φ ∈ R)
• (~''(AnyFormula.loaded χ)).in_side Side.LL (fst, fst_1, O) = (O = some (Sum.inl (~'χ)))
• (~''(AnyFormula.loaded χ)).in_side Side.RR (fst, fst_1, O) = (O = some (Sum.inr (~'χ)))

theorem AnyNegFormula.in_side_of_setEqTo {side : Side} {X Y : Sequent} (h : X.setEqTo Y) {anf : AnyNegFormula} : anf.in_side side X ↔ anf.in_side side Y

theorem AnyNegFormula.in_side_of_multisetEqTo {side : Side} {X Y : Sequent} (h : X.multisetEqTo Y) {anf : AnyNegFormula} : anf.in_side side X ↔ anf.in_side side Y

theorem LoadFormula.in_side_of_lf_inl {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inl (~'lf))) : (~''(AnyFormula.loaded lf)).in_side Side.LL X

theorem LoadFormula.in_side_of_lf_inr {X : Sequent} (lf : LoadFormula) (O_def : X.2.2 = some (Sum.inr (~'lf))) : (~''(AnyFormula.loaded lf)).in_side Side.RR X

theorem Sequent.isLoaded_of_negAnyFormula_loaded {α : Program} {ξ : AnyFormula} {side : Side} {X : Sequent} (negLoad_in : (~''(AnyFormula.loaded (⌊α⌋ξ))).in_side side X) : X.isLoaded = true

@[simp]

theorem Sequent.without_loaded_in_side_isFree (LRO : Sequent) (ξ : LoadFormula) (side : Side) : (~''(AnyFormula.loaded ξ)).in_side side LRO → (LRO.without (~''(AnyFormula.loaded ξ))).isFree = true

Whatever formulas

A type to describe all formulas that can occur in a sequent, without losing information about whether they are loaded or not.

inductive WhateverFormula : Type

Unfortunately our AnyFormula type does not include negated loaded formulas, so this is yet another type to describe "whatever formula" can be in a sequent, without losing information.

• any : AnyFormula → WhateverFormula
• negLoad : NegLoadFormula → WhateverFormula

instance instReprWhateverFormula : Repr WhateverFormula

Equations

• instReprWhateverFormula = { reprPrec := instReprWhateverFormula.repr }

def instReprWhateverFormula.repr : WhateverFormula → ℕ → Std.Format

Equations

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

instance instDecidableEqWhateverFormula : DecidableEq WhateverFormula

Equations

• instDecidableEqWhateverFormula = instDecidableEqWhateverFormula.decEq

def instDecidableEqWhateverFormula.decEq (x✝ x✝¹ : WhateverFormula) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqWhateverFormula.decEq (WhateverFormula.any a) (WhateverFormula.any b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqWhateverFormula.decEq (WhateverFormula.any a) (WhateverFormula.negLoad a_1) = isFalse ⋯
• instDecidableEqWhateverFormula.decEq (WhateverFormula.negLoad a) (WhateverFormula.any a_1) = isFalse ⋯
• instDecidableEqWhateverFormula.decEq (WhateverFormula.negLoad a) (WhateverFormula.negLoad b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance instCoeFormulaWhateverFormula : Coe Formula WhateverFormula

Equations

• instCoeFormulaWhateverFormula = { coe := WhateverFormula.any ∘ AnyFormula.normal }

instance instCoeLoadFormulaWhateverFormula : Coe LoadFormula WhateverFormula

Equations

• instCoeLoadFormulaWhateverFormula = { coe := WhateverFormula.any ∘ AnyFormula.loaded }

instance instCoeNegLoadFormulaWhateverFormula : Coe NegLoadFormula WhateverFormula

Equations

• instCoeNegLoadFormulaWhateverFormula = { coe := WhateverFormula.negLoad }

def Olf.wForms : Olf → List WhateverFormula

Equations

• Olf.wForms none = []
• Olf.wForms (some (Sum.inl nlf)) = [WhateverFormula.negLoad nlf]
• Olf.wForms (some (Sum.inr nlf)) = [WhateverFormula.negLoad nlf]

def Sequent.wForms : Sequent → List WhateverFormula

Equations

• Sequent.wForms (L, R, O) = List.map Coe.coe L ++ List.map Coe.coe R ++ O.wForms

theorem Sequent.mem_bothSides_iff (φ : Formula) (X : Sequent) : φ ∈ X.bothSides ↔ WhateverFormula.any (AnyFormula.normal φ) ∈ X.wForms ∨ (∃ (χ : LoadFormula), χ.unload = φ ∧ WhateverFormula.any (AnyFormula.loaded χ) ∈ X.wForms) ∨ ∃ (ψ : NegLoadFormula), negUnload ψ = φ ∧ WhateverFormula.negLoad ψ ∈ X.wForms

theorem Sequent.mem_wForms_normal_iff {ψ : Formula} {L R : List Formula} {O : Olf} : (WhateverFormula.any ∘ AnyFormula.normal) ψ ∈ wForms (L, R, O) ↔ ψ ∈ L ∨ ψ ∈ R

A normal formula is in X.wForms iff it is on the left or on the right of X. (Note that the Olf part of X only contributes negated loaded formulas.)

theorem Sequent.isAtomic_of_basic_of_negBox_mem_wForms {X : Sequent} {α : Program} {φ : Formula} (bas : X.basic) (h : (WhateverFormula.any ∘ AnyFormula.normal) (~⌈α⌉φ) ∈ X.wForms) : α.isAtomic

In a basic sequent all free diamonds are atomic.

@[simp]

theorem Sequent.bothSides_toFinset_eq_toFinset {X : Sequent} : X.bothSides.toFinset = X.toFinset

theorem Sequent.mem_wForms_negLoad_iff {nlf : NegLoadFormula} {L R : List Formula} {O : Olf} : WhateverFormula.negLoad nlf ∈ wForms (L, R, O) ↔ O = some (Sum.inl nlf) ∨ O = some (Sum.inr nlf)

A negated loaded formula is in X.wForms iff it is the loaded formula of X.

theorem Sequent.isAtomic_of_basic_of_negLoad_mem_wForms {X : Sequent} {α : Program} {ξ : AnyFormula} (bas : X.basic) (h : WhateverFormula.negLoad (~'⌊α⌋ξ) ∈ X.wForms) : α.isAtomic

In a basic sequent all loaded diamonds are atomic.