have osTruth := oneSidedLocalRuleTruth orule W M w
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
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)
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci