internlm/Lean-Github huggingface dataset:
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f
Tactic:
rcases em (f ∈ Lcond) with f_in_cond | f_notin_cond
Proof state after:
case mpr.intro.intro.inl.inl.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ evaluate M w f

case mpr.intro.intro.inl.inl.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_notin_cond : f ∉ Lcond
⊢ evaluate M w f
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl.inl
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
this : ∀ f ∈ Lcond, evaluate M w f
⊢ evaluate M w f
Tactic:
exact this f f_in_cond
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ ∀ f ∈ Lcond, evaluate M w f
Tactic:
rw [← conEval, osTruth, disconEval]
Proof state after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
Theorem: localRuleTruth
Proof state before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
Tactic:
use Y
Proof state after:
case h
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ Y ∈ ress ∧ ∀ f ∈ Y, evaluate M w f
Theorem: localRuleTruth
Proof state before:
case h
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ Y ∈ ress ∧ ∀ f ∈ Y, evaluate M w f
Tactic:
constructor
Proof state after:
case h.left
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ Y ∈ ress

case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ ∀ f ∈ Y, evaluate M w f
Theorem: localRuleTruth
Proof state before:
case h.left
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ Y ∈ ress
Tactic:
exact Y_in
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_in_cond : f ∈ Lcond
⊢ ∀ f ∈ Y, evaluate M w f
Tactic:
intro f f_in
Proof state after:
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f✝ : Formula
f_in_L : f✝ ∈ L
f_in_cond : f✝ ∈ Lcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f
Theorem: localRuleTruth
Proof state before:
case h.right
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f✝ : Formula
f_in_L : f✝ ∈ L
f_in_cond : f✝ ∈ Lcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case h.right.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f✝ : Formula
f_in_L : f✝ ∈ L
f_in_cond : f✝ ∈ Lcond
f : Formula
f_in : f ∈ Y
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case h.right.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f✝ : Formula
f_in_L : f✝ ∈ L
f_in_cond : f✝ ∈ Lcond
f : Formula
f_in : f ∈ Y
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_notin_cond : f ∉ Lcond
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case mpr.intro.intro.inl.inl.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_notin_cond : f ∉ Lcond
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_notin_cond : f ∉ Lcond
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
Proof state after:
case mpr.intro.intro.inl.inl.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_notin_cond : f ∉ Lcond
⊢ ((f ∈ L.diff Lcond ∨ f ∈ Y) ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inl.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_L : f ∈ L
f_notin_cond : f ∉ Lcond
⊢ ((f ∈ L.diff Lcond ∨ f ∈ Y) ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inl $ Or.inl $ List.mem_diff_of_mem f_in_L f_notin_cond
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_R : f ∈ R
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case mpr.intro.intro.inl.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_R : f ∈ R
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inl.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_R : f ∈ R
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inr
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
apply w_LYRO
Proof state after:
case mpr.intro.intro.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Theorem: localRuleTruth
Proof state before:
case mpr.intro.intro.inr.a
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
Lcond : List Formula
ress : List (List Formula)
orule : OneSidedLocalRule Lcond ress
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
preconditionProof : Lcond.Sublist L
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L.diff Lcond ++ Y, R, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
Proof state after:
no goals
Theorem: localRuleTruth
Proof state before:
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
Tactic:
have := oneSidedLocalRuleTruth orule W M w
Proof state after:
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)
this : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
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)
this : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
have osTruth := oneSidedLocalRuleTruth orule W M w
Proof state after:
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)
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Theorem: localRuleTruth
Proof state before:
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)
this osTruth : evaluate M w (Con Rcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
subst hC
Proof state after:
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
Theorem: localRuleTruth
Proof state before:
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
Tactic:
simp [applyLocalRule] at *
Proof state after:
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)
Theorem: localRuleTruth
Proof state before:
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)
Tactic:
constructor
Proof state after:
case mp
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)

case mpr
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
⊢ (∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)) → (M, w)⊨(L, R, O)
Theorem: localRuleTruth
Proof state before:
case mp
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)
Tactic:
intro w_LRO
Proof state after:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Theorem: localRuleTruth
Proof state before:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Tactic:
have : evaluate M w (discon ress) := by
  rw [← osTruth, conEval]
  intro f f_in; apply w_LRO
  simp only [List.mem_union_iff, List.mem_append]
  exact Or.inl $ Or.inr $ List.Sublist.subset preconditionProof f_in
Proof state after:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Theorem: localRuleTruth
Proof state before:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Tactic:
rw [disconEval] at this
Proof state after:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Theorem: localRuleTruth
Proof state before:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Tactic:
rcases this with ⟨Y, Y_in, claim⟩
Proof state after:
case mp.intro.intro
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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Theorem: localRuleTruth
Proof state before:
case mp.intro.intro
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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L, R.diff Rcond ++ a, O)
Tactic:
use Y
Proof state after:
case h
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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ Y ∈ ress ∧ (M, w)⊨(L, R.diff Rcond ++ Y, O)