Theorem: semEquiv.transitive (Pdl/Semantics.lean)

State before:
⊢ Transitive semEquiv
Tactic:
unfold Transitive
State after:
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z

State before:
⊢ ∀ ⦃x y z : Formula⦄, semEquiv x y → semEquiv y z → semEquiv x z
Tactic:
unfold semEquiv
State after:
⊢ ∀ ⦃x y z : Formula⦄,
    (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w y) →
      (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w y ↔ evaluate M w z) →
        ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w z

State before:
⊢ ∀ ⦃x y z : Formula⦄,
    (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w y) →
      (∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w y ↔ evaluate M w z) →
        ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w x ↔ evaluate M w z
Tactic:
intro f g h f_is_g g_is_h W M w
State after:
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w f ↔ evaluate M w g
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w g ↔ evaluate M w h
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w f ↔ evaluate M w h

State before:
f g h : Formula
f_is_g : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w f ↔ evaluate M w g
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w g ↔ evaluate M w h
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w f ↔ evaluate M w h
Tactic:
specialize f_is_g W M w
State after:
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w g ↔ evaluate M w h
W : Type
M : KripkeModel W
w : W
f_is_g : evaluate M w f ↔ evaluate M w g
⊢ evaluate M w f ↔ evaluate M w h

State before:
f g h : Formula
g_is_h : ∀ (W : Type) (M : KripkeModel W) (w : W), evaluate M w g ↔ evaluate M w h
W : Type
M : KripkeModel W
w : W
f_is_g : evaluate M w f ↔ evaluate M w g
⊢ evaluate M w f ↔ evaluate M w h
Tactic:
specialize g_is_h W M w
State after:
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : evaluate M w f ↔ evaluate M w g
g_is_h : evaluate M w g ↔ evaluate M w h
⊢ evaluate M w f ↔ evaluate M w h

State before:
f g h : Formula
W : Type
M : KripkeModel W
w : W
f_is_g : evaluate M w f ↔ evaluate M w g
g_is_h : evaluate M w g ↔ evaluate M w h
⊢ evaluate M w f ↔ evaluate M w h
Tactic:
tauto
State after:
no goals