Theorem: localRuleTruth (Pdl/LocalTableau.lean)

State before:
W : Type
L R : List Formula
C : List TNode
O : Option (NegLoadFormula ⊕ NegLoadFormula)
lrA : LocalRuleApp (L, R, O) C
M : KripkeModel W
w : W
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
rcases lrA with ⟨Lcond, Rcond, Ocond, rule, preconditionProof⟩
State after:
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

State before:
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
Tactic:
cases rule
State after:
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

State before:
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
Tactic:
case LRnegL φ hC =>
  subst hC
  simp [applyLocalRule] at *
  intro hyp
  have := hyp φ
  have := hyp (~φ)
  aesop
State after:
no goals

State before:
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
Tactic:
case LRnegR φ hC =>
  subst hC
  simp [applyLocalRule] at *
  intro hyp
  have := hyp φ
  have := hyp (~φ)
  aesop
State after:
no goals

State before:
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
Tactic:
have osTruth := oneSidedLocalRuleTruth orule W M w
State after:
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

State before:
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
Tactic:
subst hC
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
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.oneSidedL orule) (L, R, O), (M, w)⊨Ci

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
preconditionProof : Lcond.Sublist L ∧ ∅.Sublist R ∧ none ⊆ O
osTruth : evaluate M w (Con Lcond) ↔ evaluate M w (discon ress)
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.oneSidedL orule) (L, R, O), (M, w)⊨Ci
Tactic:
simp [applyLocalRule] at *
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
⊢ (M, w)⊨(L, R, O) ↔ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

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
⊢ (M, w)⊨(L, R, O) ↔ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
constructor
State after:
case mp
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
⊢ (M, w)⊨(L, R, O) → ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

case mpr
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
⊢ (∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)) → (M, w)⊨(L, R, O)

State before:
case mp
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
⊢ (M, w)⊨(L, R, O) → ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
intro w_LRO
State after:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

State before:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, 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.inl $ List.Sublist.subset preconditionProof f_in
State after:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

State before:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : evaluate M w (discon ress)
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
rw [disconEval] at this
State after:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)

State before:
case mp
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
w_LRO : (M, w)⊨(L, R, O)
this : ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
⊢ ∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)
Tactic:
rcases this with ⟨Y, Y_in, claim⟩
State after:
case mp.intro.intro
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
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.diff Lcond ++ a, R, O)

State before:
case mp.intro.intro
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
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.diff Lcond ++ a, R, O)
Tactic:
use Y
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
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.diff Lcond ++ Y, R, O)

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
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.diff Lcond ++ Y, R, O)
Tactic:
constructor
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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ 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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ (M, w)⊨(L.diff Lcond ++ Y, R, O)

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
w_LRO : (M, w)⊨(L, R, O)
⊢ evaluate M w (discon ress)
Tactic:
rw [← osTruth, conEval]
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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∀ f ∈ Lcond, evaluate M w f

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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∀ f ∈ Lcond, evaluate M w f
Tactic:
intro f f_in
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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ evaluate M w f

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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ evaluate M w f
Tactic:
apply w_LRO
State after:
case 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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case 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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case 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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case 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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Lcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inl $ List.Sublist.subset preconditionProof f_in
State after:
no goals

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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ Y ∈ ress
Tactic:
exact Y_in
State after:
no goals

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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
⊢ (M, w)⊨(L.diff Lcond ++ Y, R, O)
Tactic:
intro f f_in
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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in : f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in : f ∈ L.diff Lcond ++ Y ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
simp only [List.mem_union_iff, List.mem_append] at f_in
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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in : ((f ∈ L.diff Lcond ∨ f ∈ Y) ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in : ((f ∈ L.diff Lcond ∨ f ∈ Y) ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
rcases f_in with (((f_in_L | f_in_Y) | f_in_R) | f_in_O)
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L.diff Lcond
⊢ evaluate M w f

case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_Y : f ∈ Y
⊢ evaluate M w f

case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_R : f ∈ R
⊢ evaluate M w f

case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L.diff Lcond
⊢ evaluate M w f
Tactic:
apply w_LRO f
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L.diff Lcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L.diff Lcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L.diff Lcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_L : f ∈ L.diff Lcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inl $ List.diff_subset L Lcond f_in_L
State after:
no goals

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_Y : f ∈ Y
⊢ evaluate M w f
Tactic:
exact claim f f_in_Y
State after:
no goals

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_R : f ∈ R
⊢ evaluate M w f
Tactic:
apply w_LRO f
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_R : f ∈ R
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_R : f ∈ R
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_R : f ∈ R
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_R : f ∈ R
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
tauto
State after:
no goals

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
apply w_LRO f
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.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
w_LRO : (M, w)⊨(L, R, O)
Y : List Formula
Y_in : Y ∈ ress
claim : ∀ f ∈ Y, evaluate M w f
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inr f_in_O
State after:
no goals

State before:
case mpr
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
⊢ (∃ a ∈ ress, (M, w)⊨(L.diff Lcond ++ a, R, O)) → (M, w)⊨(L, R, O)
Tactic:
rintro ⟨Y, Y_in, w_LYRO⟩
State after:
case mpr.intro.intro
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)
⊢ (M, w)⊨(L, R, O)

State before:
case mpr.intro.intro
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)
⊢ (M, w)⊨(L, R, O)
Tactic:
intro f f_in
State after:
case mpr.intro.intro
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 : f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case mpr.intro.intro
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 : f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
simp only [List.mem_union_iff, List.mem_append] at f_in
State after:
case mpr.intro.intro
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 : (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case mpr.intro.intro
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 : (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
rcases f_in with ((f_in_L | f_in_R) | f_in_O)
State after:
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

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

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

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
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

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
State after:
no goals

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]
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

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
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

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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]
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
State after:
no goals

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
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

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
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

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
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

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 *
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)

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
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)

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
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)

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
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)

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
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)

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⟩
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)

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
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)

State before:
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)
Tactic:
constructor
State after:
case h.left
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

case h.right
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
⊢ (M, w)⊨(L, R.diff Rcond ++ Y, O)

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
w_LRO : (M, w)⊨(L, R, O)
⊢ evaluate M w (discon ress)
Tactic:
rw [← osTruth, conEval]
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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∀ f ∈ Rcond, evaluate M w f

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
w_LRO : (M, w)⊨(L, R, O)
⊢ ∀ f ∈ Rcond, evaluate M w f
Tactic:
intro f f_in
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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Rcond
⊢ evaluate M w f

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
w_LRO : (M, w)⊨(L, R, O)
f : Formula
f_in : f ∈ Rcond
⊢ evaluate M w f
Tactic:
apply w_LRO
State after:
case a
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)
f : Formula
f_in : f ∈ Rcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case a
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)
f : Formula
f_in : f ∈ Rcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case a
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)
f : Formula
f_in : f ∈ Rcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case a
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)
f : Formula
f_in : f ∈ Rcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inr $ List.Sublist.subset preconditionProof f_in
State after:
no goals

State before:
case h.left
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
Tactic:
exact Y_in
State after:
no goals

State before:
case h.right
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
⊢ (M, w)⊨(L, R.diff Rcond ++ Y, O)
Tactic:
intro f f_in
State after:
case h.right
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
f : Formula
f_in : f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case h.right
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
f : Formula
f_in : f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
simp only [List.mem_union_iff, List.mem_append] at f_in
State after:
case h.right
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
f : Formula
f_in : (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case h.right
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
f : Formula
f_in : (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
rcases f_in with ((f_in_L | (f_in_R | f_in_Y)) | f_in_O)
State after:
case h.right.inl.inl
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
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f

case h.right.inl.inr.inl
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
f : Formula
f_in_R : f ∈ R.diff Rcond
⊢ evaluate M w f

case h.right.inl.inr.inr
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
f : Formula
f_in_Y : f ∈ Y
⊢ evaluate M w f

case h.right.inr
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
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case h.right.inl.inl
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
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f
Tactic:
apply w_LRO f
State after:
case h.right.inl.inl
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
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.inl.inl
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
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case h.right.inl.inl
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
f : Formula
f_in_L : f ∈ L
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.inl.inl
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
f : Formula
f_in_L : f ∈ L
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inl f_in_L
State after:
no goals

State before:
case h.right.inl.inr.inl
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
f : Formula
f_in_R : f ∈ R.diff Rcond
⊢ evaluate M w f
Tactic:
apply w_LRO f
State after:
case h.right.inl.inr.inl
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
f : Formula
f_in_R : f ∈ R.diff Rcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.inl.inr.inl
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
f : Formula
f_in_R : f ∈ R.diff Rcond
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case h.right.inl.inr.inl
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
f : Formula
f_in_R : f ∈ R.diff Rcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.inl.inr.inl
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
f : Formula
f_in_R : f ∈ R.diff Rcond
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inr $ List.diff_subset R Rcond f_in_R
State after:
no goals

State before:
case h.right.inl.inr.inr
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
f : Formula
f_in_Y : f ∈ Y
⊢ evaluate M w f
Tactic:
exact claim f f_in_Y
State after:
no goals

State before:
case h.right.inr
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
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
apply w_LRO f
State after:
case h.right.inr
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
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.inr
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
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case h.right.inr
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
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.inr
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
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inr f_in_O
State after:
no goals

State before:
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)
Tactic:
rintro ⟨Y, Y_in, w_LYRO⟩
State after:
case mpr.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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
⊢ (M, w)⊨(L, R, O)

State before:
case mpr.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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
⊢ (M, w)⊨(L, R, O)
Tactic:
intro f f_in
State after:
case mpr.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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in : f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case mpr.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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in : f ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
simp only [List.mem_union_iff, List.mem_append] at f_in
State after:
case mpr.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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case mpr.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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
rcases f_in with ((f_in_L | f_in_R) | f_in_O)
State after:
case mpr.intro.intro.inl.inl
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f

case mpr.intro.intro.inl.inr
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
⊢ evaluate M w f

case mpr.intro.intro.inr
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f

State before:
case mpr.intro.intro.inl.inl
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ evaluate M w f
Tactic:
apply w_LYRO
State after:
case mpr.intro.intro.inl.inl.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case mpr.intro.intro.inl.inl.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_L : f ∈ L
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
State after:
no goals

State before:
case mpr.intro.intro.inl.inr
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
⊢ evaluate M w f
Tactic:
rcases em (f ∈ Rcond) with f_in_cond | f_notin_cond
State after:
case mpr.intro.intro.inl.inr.inl
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ evaluate M w f

case mpr.intro.intro.inl.inr.inr
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ evaluate M w f

State before:
case mpr.intro.intro.inl.inr.inl
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
this : ∀ f ∈ Rcond, evaluate M w f
⊢ evaluate M w f
Tactic:
exact this f f_in_cond
State after:
no goals

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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∀ f ∈ Rcond, evaluate M w f
Tactic:
rw [← conEval, osTruth, disconEval]
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f

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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∃ Y ∈ ress, ∀ f ∈ Y, evaluate M w f
Tactic:
use Y
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress ∧ ∀ f ∈ Y, evaluate M w f

State before:
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress ∧ ∀ f ∈ Y, evaluate M w f
Tactic:
constructor
State after:
case h.left
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress

case h.right
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∀ f ∈ Y, evaluate M w f

State before:
case h.left
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ Y ∈ ress
Tactic:
exact Y_in
State after:
no goals

State before:
case h.right
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_in_cond : f ∈ Rcond
⊢ ∀ f ∈ Y, evaluate M w f
Tactic:
intro f f_in
State after:
case h.right
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f

State before:
case h.right
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ evaluate M w f
Tactic:
apply w_LYRO
State after:
case h.right.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case h.right.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f✝ : Formula
f_in_R : f✝ ∈ R
f_in_cond : f✝ ∈ Rcond
f : Formula
f_in : f ∈ Y
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
State after:
no goals

State before:
case mpr.intro.intro.inl.inr.inr
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ evaluate M w f
Tactic:
apply w_LYRO
State after:
case mpr.intro.intro.inl.inr.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case mpr.intro.intro.inl.inr.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp only [List.mem_union_iff, List.mem_append]
State after:
case mpr.intro.intro.inl.inr.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case mpr.intro.intro.inl.inr.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_R : f ∈ R
f_notin_cond : f ∉ Rcond
⊢ (f ∈ L ∨ f ∈ R.diff Rcond ∨ f ∈ Y) ∨ f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
exact Or.inl $ Or.inr $ Or.inl $ List.mem_diff_of_mem f_in_R f_notin_cond
State after:
no goals

State before:
case mpr.intro.intro.inr
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ evaluate M w f
Tactic:
apply w_LYRO
State after:
case mpr.intro.intro.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList

State before:
case mpr.intro.intro.inr.a
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
Y : List Formula
Y_in : Y ∈ ress
w_LYRO : (M, w)⊨(L, R.diff Rcond ++ Y, O)
f : Formula
f_in_O : f ∈ (Option.map (Sum.elim negUnload negUnload) O).toList
⊢ f ∈ L ∪ (R.diff Rcond ++ Y) ∪ (Option.map (Sum.elim negUnload negUnload) O).toList
Tactic:
simp_all
State after:
no goals

State before:
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
Tactic:
subst hC
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [φ].Sublist L ∧ [~φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegL φ) (L, R, O), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [φ].Sublist L ∧ [~φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegL φ) (L, R, O), (M, w)⊨Ci
Tactic:
simp [applyLocalRule] at *
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
⊢ ¬(M, w)⊨(L, R, O)

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
⊢ ¬(M, w)⊨(L, R, O)
Tactic:
intro hyp
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False
Tactic:
have := hyp φ
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
Tactic:
have := hyp (~φ)
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : φ ∈ L ∧ (~φ) ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False
Tactic:
aesop
State after:
no goals

State before:
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
Tactic:
subst hC
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [~φ].Sublist L ∧ [φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegR φ) (L, R, O), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : [~φ].Sublist L ∧ [φ].Sublist R ∧ none ⊆ O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.LRnegR φ) (L, R, O), (M, w)⊨Ci
Tactic:
simp [applyLocalRule] at *
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
⊢ ¬(M, w)⊨(L, R, O)

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
⊢ ¬(M, w)⊨(L, R, O)
Tactic:
intro hyp
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
⊢ False
Tactic:
have := hyp φ
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
⊢ False
Tactic:
have := hyp (~φ)
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
φ : Formula
preconditionProof : (~φ) ∈ L ∧ φ ∈ R
hyp : (M, w)⊨(L, R, O)
this✝ : φ ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w φ
this : (~φ) ∈ L ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) O).toList → evaluate M w (~φ)
⊢ False
Tactic:
aesop
State after:
no goals

State before:
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
Tactic:
have := loadRuleTruth lrule W M w
State after:
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)
this :
  evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress))
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

State before:
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)
this :
  evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress))
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
rw [disEval] at this
State after:
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)
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

State before:
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)
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
subst hC
State after:
W : Type
L R : List Formula
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
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, O), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
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
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, O), (M, w)⊨Ci
Tactic:
simp at preconditionProof
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
preconditionProof : some (Sum.inl (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, O), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
preconditionProof : some (Sum.inl (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, O), (M, w)⊨Ci
Tactic:
subst preconditionProof
State after:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, some (Sum.inl (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, some (Sum.inl (~'χ))), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, some (Sum.inl (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedL χ lrule) (L, R, some (Sum.inl (~'χ))), (M, w)⊨Ci
Tactic:
simp [modelCanSemImplyForm,modelCanSemImplyLLO] at *
State after:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) ↔
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) ↔
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Tactic:
constructor
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) →
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci

case mpr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci) →
    ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) →
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Tactic:
intro hyp
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
have hyp' := hyp (~unload χ)
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ((~unload χ) ∈ L ∨ (~unload χ) ∈ R) ∨ (~unload χ) = (~unload χ) → evaluate M w (~unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ((~unload χ) ∈ L ∨ (~unload χ) ∈ R) ∨ (~unload χ) = (~unload χ) → evaluate M w (~unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
simp at hyp'
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ¬evaluate M w (unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ¬evaluate M w (unload χ)
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
rw [this] at hyp'
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
hyp' : ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
rcases hyp' with ⟨f, ⟨X , O, in_ress, def_f⟩, w_f⟩
State after:
case mp.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_f : Con (X ++ (Option.map negUnload O).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_f : Con (X ++ (Option.map negUnload O).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
cases O
State after:
case mp.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

case mp.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val✝)).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci

State before:
case mp.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
use (L ++ X, R, some (Sum.inl (~'χ)))
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl (~'χ)))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl (~'χ)))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
constructor
State after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl (~'χ)))

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))

State before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
use X, none
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress ∧
    (match Option.map Sum.inl none with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl (~'χ)))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress ∧
    (match Option.map Sum.inl none with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
simp only [Option.map_none', and_true]
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (X, none) ∈ ress
Tactic:
exact in_ress
State after:
no goals

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
⊢ (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
Tactic:
intro g
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
g : Formula
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
def_f : Con (X ++ (Option.map negUnload none).toList) = f
g : Formula
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
subst def_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : evaluate M w (Con (X ++ (Option.map negUnload none).toList))
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : evaluate M w (Con (X ++ (Option.map negUnload none).toList))
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
rw [conEval] at w_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
specialize hyp g
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
hyp : (g ∈ L ∨ g ∈ R) ∨ (~unload χ) = g → evaluate M w g
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
in_ress : (X, none) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload none).toList, evaluate M w f
hyp : (g ∈ L ∨ g ∈ R) ∨ (~unload χ) = g → evaluate M w g
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w g
Tactic:
aesop
State after:
no goals

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inl b with
            | none => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci
Tactic:
use (L ++ X, R, some (Sum.inl val))
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl val))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl val))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        (match Option.map Sum.inl b with
          | none => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
          | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
          (L ++ X, R, some (Sum.inl val))) ∧
    (M, w)⊨(L ++ X, R, some (Sum.inl val))
Tactic:
constructor
State after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl val))

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (M, w)⊨(L ++ X, R, some (Sum.inl val))

State before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ ∃ a b,
    (a, b) ∈ ress ∧
      (match Option.map Sum.inl b with
        | none => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
        | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
        (L ++ X, R, some (Sum.inl val))
Tactic:
use X, some val
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress ∧
    (match Option.map Sum.inl (some val) with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl val))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress ∧
    (match Option.map Sum.inl (some val) with
      | none => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
      | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
      (L ++ X, R, some (Sum.inl val))
Tactic:
simp only [Option.map_some', and_true]
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (X, some val) ∈ ress
Tactic:
exact in_ress
State after:
no goals

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
⊢ (M, w)⊨(L ++ X, R, some (Sum.inl val))
Tactic:
intro g g_in
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
g : Formula
g_in : g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
f : Formula
w_f : evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
def_f : Con (X ++ (Option.map negUnload (some val)).toList) = f
g : Formula
g_in : g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Tactic:
subst def_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
w_f : evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
w_f : evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
⊢ evaluate M w g
Tactic:
rw [conEval] at w_f
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
g_in : g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
⊢ evaluate M w g
Tactic:
simp only [List.mem_union_iff, List.mem_append, List.mem_singleton] at g_in
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : ((g ∈ L ∨ g ∈ X) ∨ g ∈ R) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : ((g ∈ L ∨ g ∈ X) ∨ g ∈ R) ∨ g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Tactic:
rcases g_in with ((g_in|g_in)|g_in)|g_in
State after:
case h.right.inl.inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ L
⊢ evaluate M w g

case h.right.inl.inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ X
⊢ evaluate M w g

case h.right.inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ R
⊢ evaluate M w g

case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g

State before:
case h.right.inl.inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ L
⊢ evaluate M w g

case h.right.inl.inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ X
⊢ evaluate M w g

case h.right.inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ R
⊢ evaluate M w g

case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Tactic:
all_goals aesop
State after:
no goals

State before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
g : Formula
w_f : ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
g_in : g ∈ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl val))).toList
⊢ evaluate M w g
Tactic:
aesop
State after:
no goals

State before:
case mpr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inl b with
              | none => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inl (~'χ)) => (L ++ a, R, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L ++ a, R, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci) →
    ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
Tactic:
rintro ⟨Ci, ⟨⟨X, O, ⟨in_ress, def_Ci⟩⟩, w_Ci⟩⟩
State after:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
    Ci
⊢ ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
    Ci
⊢ ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
Tactic:
intro f f_in
State after:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
    Ci
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Ci : TNode
w_Ci : (M, w)⊨Ci
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
def_Ci :
  (match Option.map Sum.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))) =
    Ci
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
⊢ evaluate M w f
Tactic:
subst def_Ci
State after:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
w_Ci :
  (M, w)⊨match Option.map Sum.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
O : Option NegLoadFormula
in_ress : (X, O) ∈ ress
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
w_Ci :
  (M, w)⊨match Option.map Sum.inl O with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
cases O
State after:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inl none with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f

case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inl (some val✝) with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inl none with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f

case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inl (some val✝) with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
all_goals simp at *
State after:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
⊢ evaluate M w f

case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val✝.1)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci :
  (M, w)⊨match Option.map Sum.inl (some val✝) with
    | none => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inl (~'χ)) => (L ++ X, R, some (Sum.inl (~'χ)))
    | some (Sum.inr (~'χ)) => (L ++ X, R, some (Sum.inr (~'χ)))
⊢ evaluate M w f
Tactic:
simp at *
State after:
case mpr.intro.intro.intro.intro.intro.some
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val✝ : NegLoadFormula
in_ress : (X, some val✝) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val✝.1)))
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
⊢ evaluate M w f
Tactic:
have := w_Ci f
State after:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this✝ :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
this : f ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w f
⊢ evaluate M w f

State before:
case mpr.intro.intro.intro.intro.intro.none
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this✝ :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
in_ress : (X, none) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'χ)))
this : f ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'χ)))).toList → evaluate M w f
⊢ evaluate M w f
Tactic:
aesop
State after:
no goals

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
f_in : (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w f
Tactic:
rcases f_in with (f_in|f_in)|f_in
State after:
case inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ L
⊢ evaluate M w f

case inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ R
⊢ evaluate M w f

case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : (~unload χ) = f
⊢ evaluate M w f

State before:
case inl.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ L
⊢ evaluate M w f
Tactic:
apply w_Ci
State after:
case inl.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ L
⊢ f ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList

State before:
case inl.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ L
⊢ f ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
case inl.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ R
⊢ evaluate M w f
Tactic:
apply w_Ci
State after:
case inl.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ R
⊢ f ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList

State before:
case inl.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : f ∈ R
⊢ f ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
f : Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
f_in : (~unload χ) = f
⊢ evaluate M w f
Tactic:
subst f_in
State after:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (~unload χ)

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (~unload χ)
Tactic:
simp only [evaluate]
State after:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ¬evaluate M w (unload χ)

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ¬evaluate M w (unload χ)
Tactic:
rw [this]
State after:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f

State before:
case inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
Tactic:
use Con (X ++ Option.toList (Option.map negUnload (some val)))
State after:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)) ∧
    evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))

State before:
case h
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ (∃ a b,
      (a, b) ∈ ress ∧
        Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)) ∧
    evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
Tactic:
constructor
State after:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∃ a b,
    (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)

case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))

State before:
case h.left
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∃ a b,
    (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = Con (X ++ (Option.map negUnload (some val)).toList)
Tactic:
use X, some val
State after:
no goals

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (Con (X ++ (Option.map negUnload (some val)).toList))
Tactic:
rw [conEval]
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∀ f ∈ X ++ (Option.map negUnload (some val)).toList, evaluate M w f
Tactic:
simp only [Option.map_some', negUnload, Option.toList_some, List.mem_append, List.mem_singleton]
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∀ (f : Formula), f ∈ X ∨ f = (~unload val.1) → evaluate M w f

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ ∀ (f : Formula), f ∈ X ∨ f = (~unload val.1) → evaluate M w f
Tactic:
intro g g_in
State after:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
g_in : g ∈ X ∨ g = (~unload val.1)
⊢ evaluate M w g

State before:
case h.right
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
g_in : g ∈ X ∨ g = (~unload val.1)
⊢ evaluate M w g
Tactic:
rcases g_in with (_|g_def)
State after:
case h.right.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ evaluate M w g

case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
g_def : g = (~unload val.1)
⊢ evaluate M w g

State before:
case h.right.inl
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ evaluate M w g
Tactic:
apply w_Ci
State after:
case h.right.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList

State before:
case h.right.inl.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
h✝ : g ∈ X
⊢ g ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
g : Formula
g_def : g = (~unload val.1)
⊢ evaluate M w g
Tactic:
subst g_def
State after:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (~unload val.1)

State before:
case h.right.inr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ evaluate M w (~unload val.1)
Tactic:
apply w_Ci
State after:
case h.right.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ (~unload val.1) ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList

State before:
case h.right.inr.a
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
X : List Formula
val : NegLoadFormula
in_ress : (X, some val) ∈ ress
w_Ci : (M, w)⊨(L ++ X, R, some (Sum.inl (~'val.1)))
⊢ (~unload val.1) ∈ L ++ X ∪ R ∪ (Option.map (Sum.elim negUnload negUnload) (some (Sum.inl (~'val.1)))).toList
Tactic:
simp_all
State after:
no goals

State before:
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
Tactic:
have := loadRuleTruth lrule W M w
State after:
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)
this :
  evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress))
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

State before:
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)
this :
  evaluate M w (~unload χ) ↔
    evaluate M w
      (dis
        (List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress))
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
rw [disEval] at this
State after:
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)
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci

State before:
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)
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ C, (M, w)⊨Ci
Tactic:
subst hC
State after:
W : Type
L R : List Formula
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
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, O), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
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
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, O), (M, w)⊨Ci
Tactic:
simp at preconditionProof
State after:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
preconditionProof : some (Sum.inr (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, O), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
preconditionProof : some (Sum.inr (~'χ)) = O
⊢ (M, w)⊨(L, R, O) ↔ ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, O), (M, w)⊨Ci
Tactic:
subst preconditionProof
State after:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, some (Sum.inr (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, some (Sum.inr (~'χ))), (M, w)⊨Ci

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  evaluate M w (~unload χ) ↔
    ∃
      f ∈
        List.map
          (fun x =>
            match x with
            | (fs, o) => Con (fs ++ (Option.map negUnload o).toList))
          ress,
      evaluate M w f
⊢ (M, w)⊨(L, R, some (Sum.inr (~'χ))) ↔
    ∃ Ci ∈ applyLocalRule (LocalRule.loadedR χ lrule) (L, R, some (Sum.inr (~'χ))), (M, w)⊨Ci
Tactic:
simp [modelCanSemImplyForm,modelCanSemImplyLLO] at *
State after:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) ↔
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci

State before:
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) ↔
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Tactic:
constructor
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) →
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci

case mpr
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci) →
    ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f

State before:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
⊢ (∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f) →
    ∃ Ci,
      (∃ a b,
          (a, b) ∈ ress ∧
            (match Option.map Sum.inr b with
              | none => (L, R ++ a, some (Sum.inr (~'χ)))
              | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
              | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
              Ci) ∧
        (M, w)⊨Ci
Tactic:
intro hyp
State after:
case mp
W : Type
L R : List Formula
M : KripkeModel W
w : W
ress : List (List Formula × Option NegLoadFormula)
χ : LoadFormula
lrule : LoadRule (~'χ) ress
this :
  ¬evaluate M w (unload χ) ↔
    ∃ f, (∃ a b, (a, b) ∈ ress ∧ Con (a ++ (Option.map negUnload b).toList) = f) ∧ evaluate M w f
hyp : ∀ (f : Formula), (f ∈ L ∨ f ∈ R) ∨ (~unload χ) = f → evaluate M w f
⊢ ∃ Ci,
    (∃ a b,
        (a, b) ∈ ress ∧
          (match Option.map Sum.inr b with
            | none => (L, R ++ a, some (Sum.inr (~'χ)))
            | some (Sum.inl (~'χ)) => (L, R ++ a, some (Sum.inl (~'χ)))
            | some (Sum.inr (~'χ)) => (L, R ++ a, some (Sum.inr (~'χ)))) =
            Ci) ∧
      (M, w)⊨Ci