Helpers for Lemma 9.4: single steps keep the loading on the right

The lemmas here say that a single step in a tableau, starting at a node that is loaded on the right, can only lead to a node that is loaded on the right or free, and that no rule adds formulas to an empty left component.

theorem pdlRule_inv {X Y : Sequent} (r : PdlRule X Y) (h : X.2.2.isRight) : ¬Y.2.2.isLeft ∧ (X.1 = ∅ → Y.1 = ∅)

A PDL rule applied to a sequent that is loaded on the right leads to a sequent that is not loaded on the left, and it does not add formulas to an empty left component.

theorem applyLocalRule_not_isLeft {Lcond Rcond : Finset Formula} {Ocond : Olf} {ress : Finset Sequent} (lr : LocalRule (Lcond, Rcond, Ocond) ress) {L R : Finset Formula} {O : Olf} (hO : Ocond ⊆ O) (hnl : ¬O.isLeft) (c : Sequent) : c ∈ applyLocalRule lr (L, R, O) → ¬c.2.2.isLeft

Local rules never load on the left: if the given sequent is not loaded on the left, then neither are the results of applying a local rule to it.

theorem applyLocalRule_L_empty {Lcond Rcond : Finset Formula} {Ocond : Olf} {ress : Finset Sequent} (lr : LocalRule (Lcond, Rcond, Ocond) ress) {L R : Finset Formula} {O : Olf} (hL : L = ∅) (hsub : Lcond ⊆ L) (hO : Ocond ⊆ O) (hnl : ¬O.isLeft) (c : Sequent) : c ∈ applyLocalRule lr (L, R, O) → c.1 = ∅

Local rules do not add formulas to an empty left component, provided the sequent is not loaded on the left.

theorem endNodesOf_inv {X : Sequent} (lt : LocalTableau X) (hnl : ¬X.2.2.isLeft) (Y : Sequent) : Y ∈ endNodesOf lt → ¬Y.2.2.isLeft ∧ (X.1 = ∅ → Y.1 = ∅)

End nodes of a local tableau for a sequent that is not loaded on the left are also not loaded on the left, and they have an empty left component if the given sequent has.

theorem edge_inv {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} (h : s ⋖_ t) (hs : (nodeAt s).2.2.isRight) : ¬(nodeAt t).2.2.isLeft ∧ ((nodeAt s).1 = ∅ → (nodeAt t).1 = ∅)

A ⋖_ step from a node loaded on the right leads to a node that is not loaded on the left, and it does not add formulas to an empty left component.

theorem cEdge_inv {X : Sequent} {tab : Tableau [] X} {s t : PathIn tab} (h : s ◃ t) (hs : (nodeAt s).2.2.isRight) (ht : (nodeAt t).isLoaded) : (nodeAt t).2.2.isRight ∧ ((nodeAt s).1 = ∅ → (nodeAt t).1 = ∅)

A ◃ step from a node loaded on the right to a loaded node leads to a node that is also loaded on the right, and it does not add formulas to an empty left component.

theorem cReach_inv {X : Sequent} {tab : Tableau [] X} {a b : PathIn tab} (hab : a ◃* b) (hloaded : ∀ (v : PathIn tab), a ◃* v → v ◃* b → (nodeAt v).isLoaded) (ha : (nodeAt a).2.2.isRight) : (nodeAt b).2.2.isRight ∧ ((nodeAt a).1 = ∅ → (nodeAt b).1 = ∅)

Along a ◃-path where all nodes are loaded, the loading stays on the right and an empty left component stays empty.