simp [applyLocalRule] at *
W : Type
L R : List Formula
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
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.oneSidedR orule) (L, R, O), (M, w)⊨Ci
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Rcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Rcond ress
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
preconditionProof : Rcond.Sublist R
⊢ (M, w)⊨(L, R, O) ↔ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)