cases rule
case mk
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List TNode
Lcond Rcond : List Formula
Ocond : Option (NegLoadFormula ⊕ NegLoadFormula)
rule : LocalRule (Lcond, Rcond, Ocond) ress✝
preconditionProof : Lcond.Sublist L ∧ Rcond.Sublist R ∧ Ocond ⊆ O
hC✝ : C = applyLocalRule rule (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
case mk.oneSidedL
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Lcond ress✝
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.oneSidedL orule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.oneSidedR
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress✝ : List (List Formula)
orule✝ : OneSidedLocalRule Rcond ress✝
preconditionProof : ∅.Sublist L ∧ Rcond.Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.oneSidedR orule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.LRnegL
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ϕ✝ : Formula
preconditionProof : [ϕ✝].Sublist L ∧ [~ϕ✝].Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.LRnegL ϕ✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.LRnegR
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ϕ✝ : Formula
preconditionProof : [~ϕ✝].Sublist L ∧ [ϕ✝].Sublist R ∧ none ⊆ O
hC✝ : C = applyLocalRule (LocalRule.LRnegR ϕ✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.loadedL
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
preconditionProof : ∅.Sublist L ∧ ∅.Sublist R ∧ some (Sum.inl (~'χ✝)) ⊆ O
hC✝ : C = applyLocalRule (LocalRule.loadedL χ✝ lrule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

case mk.loadedR
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress✝ : List (List Formula × Option NegLoadFormula)
χ✝ : LoadFormula
lrule✝ : LoadRule (~'χ✝) ress✝
preconditionProof : ∅.Sublist L ∧ ∅.Sublist R ∧ some (Sum.inr (~'χ✝)) ⊆ O
hC✝ : C = applyLocalRule (LocalRule.loadedR χ✝ lrule✝) (L, R, O)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci