Theorem: disEvalHT (Pdl/Discon.lean)

State before:
X : List Formula
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
Tactic:
induction' X with g X IH
State after:
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis [f]) ↔ evaluate M w f ∨ evaluate M w (dis [])

case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ evaluate M w (dis (f :: g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))

State before:
case nil
f : Formula
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (dis [f]) ↔ evaluate M w f ∨ evaluate M w (dis [])
Tactic:
simp
State after:
no goals

State before:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ evaluate M w (dis (f :: g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))
Tactic:
simp
State after:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ ¬evaluate M w f → evaluate M w (dis (g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))

State before:
case cons
f : Formula
W : Type
M : KripkeModel W
w : W
g : Formula
X : List Formula
IH : evaluate M w (dis (f :: X)) ↔ evaluate M w f ∨ evaluate M w (dis X)
⊢ ¬evaluate M w f → evaluate M w (dis (g :: X)) ↔ evaluate M w f ∨ evaluate M w (dis (g :: X))
Tactic:
tauto
State after:
no goals