Theorem: A4 (Pdl/Examples.lean)

State before:
a b : Program
p : ℕ
⊢ tautology ((~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p))⋀(~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p)))
Tactic:
unfold tautology evaluate
State after:
a b : Program
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))

State before:
a b : Program
p : ℕ
⊢ ∀ (W : Type) (M : KripkeModel W) (w : W),
    evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
Tactic:
intro W M w
State after:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))

State before:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a⌉⌈b⌉·p)) ∧ evaluate M w (~(⌈a;'b⌉·p)⋀(~⌈a;'b⌉·p))
Tactic:
simp
State after:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ (∀ (x x_1 : W), relate M a w x_1 → relate M b x_1 x → M.val x p) →
    ∀ (x : W), relate M a w x → ∀ (x_1 : W), relate M b x x_1 → M.val x_1 p

State before:
a b : Program
p : ℕ
W : Type
M : KripkeModel W
w : W
⊢ (∀ (x x_1 : W), relate M a w x_1 → relate M b x_1 x → M.val x p) →
    ∀ (x : W), relate M a w x → ∀ (x_1 : W), relate M b x x_1 → M.val x_1 p
Tactic:
tauto
State after:
no goals