Theorem: existsDiamondH (Pdl/Unfold.lean)

State before:
W✝ : Type
M : KripkeModel W✝
γ : Program
v w : W✝
v_γ_w : relate M γ v w
⊢ ∃ Fδ ∈ H γ, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
cases γ
State after:
case atom_prog
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case sequence
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹;'a✝) v w
⊢ ∃ Fδ ∈ H (a✝¹;'a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case union
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝¹ a✝ : Program
v_γ_w : relate M (a✝¹⋓a✝) v w
⊢ ∃ Fδ ∈ H (a✝¹⋓a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case star
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Program
v_γ_w : relate M (∗a✝) v w
⊢ ∃ Fδ ∈ H (∗a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case test
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : Formula
v_γ_w : relate M (?'a✝) v w
⊢ ∃ Fδ ∈ H (?'a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
case atom_prog =>
  simp [H, relateSeq] at *
  exact v_γ_w
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
⊢ ∃ Fδ ∈ H (?'τ), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
case test τ =>
  simp [H, relateSeq] at *
  aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α⋓β) v w
⊢ ∃ Fδ ∈ H (α⋓β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
case union α β =>
  simp [H, relateSeq] at *
  cases v_γ_w
  case inl hyp =>
    have IHα := existsDiamondH hyp
    aesop
  case inr hyp =>
    have IHβ := existsDiamondH hyp
    aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : relate M (·a✝) v w
⊢ ∃ Fδ ∈ H (·a✝), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at *
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : M.Rel a✝ v w
⊢ M.Rel a✝ v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
a✝ : ℕ
v_γ_w : M.Rel a✝ v w
⊢ M.Rel a✝ v w
Tactic:
exact v_γ_w
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : relate M (?'τ) v w
⊢ ∃ Fδ ∈ H (?'τ), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at *
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : v = w ∧ evaluate M v τ
⊢ evaluate M v τ ∧ v = w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
τ : Formula
v_γ_w : v = w ∧ evaluate M v τ
⊢ evaluate M v τ ∧ v = w
Tactic:
aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α⋓β) v w
⊢ ∃ Fδ ∈ H (α⋓β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at *
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M α v w ∨ relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
cases v_γ_w
State after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
h✝ : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
h✝ : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
case inl hyp =>
  have IHα := existsDiamondH hyp
  aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
case inr hyp =>
  have IHβ := existsDiamondH hyp
  aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
have IHα := existsDiamondH hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M α v w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
have IHβ := existsDiamondH hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
hyp : relate M β v w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ a b, ((a, b) ∈ H α ∨ (a, b) ∈ H β) ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
Tactic:
aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : relate M (α;'β) v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp only [relate] at v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
v_γ_w : ∃ y, relate M α v y ∧ relate M β y w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases v_γ_w with ⟨u, v_α_u, u_β_w⟩
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have IHα := existsDiamondH v_α_u
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ Fδ ∈ H α, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at IHα
State after:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ a b, (a, b) ∈ H α ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
IHα : ∃ a b, (a, b) ∈ H α ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases IHα with ⟨Fs, δ, ⟨Fδ_in, u_Fs, v_δ_u⟩⟩
State after:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro.intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
cases em (δ = ε)
State after:
case intro.intro.intro.intro.intro.intro.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
h✝ : δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case intro.intro.intro.intro.intro.intro.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
h✝ : ¬δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
subst hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : relateSeq M ε v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : relateSeq M ε v u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp only [relateSeq] at v_δ_u
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : v = u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_δ_u : v = u
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
subst v_δ_u
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have IHβ := existsDiamondH u_β_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp [H, relateSeq] at IHβ
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
IHβ : ∃ a b, (a, b) ∈ H β ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
IHβ : ∃ a b, (a, b) ∈ H β ∧ (∀ f ∈ a, evaluate M v f) ∧ relateSeq M b v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases IHβ with ⟨Gs, η, ⟨Gη_in, v_Gs, v_η_w⟩⟩
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
refine ⟨ ⟨Fs ∪ Gs, η⟩, ⟨?_, ?_, v_η_w⟩ ⟩
State after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ H (α;'β)

case intro.intro.intro.intro.refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (M, v)⊨(Fs ∪ Gs, η).1

State before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ H (α;'β)
Tactic:
simp_all [H]
State after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs ∪ Gs, η) ∈ l

State before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs ∪ Gs, η) ∈ l
Tactic:
refine ⟨_, ⟨⟨Fs, ε, ⟨Fδ_in, by rfl⟩⟩, ?_⟩⟩
State after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ if ε = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]

State before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (Fs ∪ Gs, η) ∈ if ε = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]
Tactic:
simp
State after:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, η) ∈ l

State before:
case intro.intro.intro.intro.refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = l) ∧ (Fs ∪ Gs, η) ∈ l
Tactic:
use [(Fs ∪ Gs, η)]
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = [(Fs ∪ Gs, η)]) ∧ (Fs ∪ Gs, η) ∈ [(Fs ∪ Gs, η)]

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (∃ a b, (a, b) ∈ H β ∧ [(Fs ∪ a, b)] = [(Fs ∪ Gs, η)]) ∧ (Fs ∪ Gs, η) ∈ [(Fs ∪ Gs, η)]
Tactic:
aesop
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Gs : List Formula
η : List Program
Fδ_in : (Fs, []) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (if ε = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, ε ++ [β])]) = ?m.1356173
Tactic:
rfl
State after:
no goals

State before:
case intro.intro.intro.intro.refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
⊢ (M, v)⊨(Fs ∪ Gs, η).1
Tactic:
intro f f_in
State after:
case intro.intro.intro.intro.refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
f_in : f ∈ (Fs ∪ Gs, η).1
⊢ evaluate M v f

State before:
case intro.intro.intro.intro.refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
f_in : f ∈ (Fs ∪ Gs, η).1
⊢ evaluate M v f
Tactic:
simp at f_in
State after:
case intro.intro.intro.intro.refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
f_in : f ∈ Fs ∨ f ∈ Gs
⊢ evaluate M v f

State before:
case intro.intro.intro.intro.refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
f_in : f ∈ Fs ∨ f ∈ Gs
⊢ evaluate M v f
Tactic:
cases f_in
State after:
case intro.intro.intro.intro.refine_2.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Fs
⊢ evaluate M v f

case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ evaluate M v f

State before:
case intro.intro.intro.intro.refine_2.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Fs
⊢ evaluate M v f
Tactic:
specialize u_Fs f (by assumption)
State after:
case intro.intro.intro.intro.refine_2.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f

State before:
case intro.intro.intro.intro.refine_2.inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f
Tactic:
assumption
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Fs
⊢ f ∈ Fs
Tactic:
assumption
State after:
no goals

State before:
case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ evaluate M v f
Tactic:
apply v_Gs f
State after:
case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ f ∈ Gs

State before:
case intro.intro.intro.intro.refine_2.inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
Fs : List Formula
u_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H α
v_α_u : relate M α v v
u_β_w : relate M β v w
Gs : List Formula
η : List Program
Gη_in : (Gs, η) ∈ H β
v_Gs : ∀ f ∈ Gs, evaluate M v f
v_η_w : relateSeq M η v w
f : Formula
h✝ : f ∈ Gs
⊢ f ∈ Gs
Tactic:
assumption
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ ∃ Fδ ∈ H (α;'β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
refine ⟨⟨Fs, δ ++ [β]⟩, ⟨?_, ?_, ?_⟩⟩
State after:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈ H (α;'β)

case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (M, v)⊨(Fs, δ ++ [β]).1

case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ relateSeq M (Fs, δ ++ [β]).2 v w

State before:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (Fs, δ ++ [β]) ∈ H (α;'β)
Tactic:
simp_all [H]
State after:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs, δ ++ [β]) ∈ l

State before:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (Fs, δ ++ [β]) ∈ l
Tactic:
refine ⟨_, ⟨⟨Fs, δ, ⟨ Fδ_in , by rfl⟩⟩, ?_⟩⟩
State after:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ (Fs, δ ++ [β]) ∈ if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]

State before:
case refine_1
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ (Fs, δ ++ [β]) ∈ if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]
Tactic:
simp_all
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = []
⊢ (if δ = [] then (List.map (fun x => [(Fs ∪ x.1, x.2)]) (H β)).join else [(Fs, δ ++ [β])]) = ?m.1382731
Tactic:
rfl
State after:
no goals

State before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ (M, v)⊨(Fs, δ ++ [β]).1
Tactic:
intro f f_in
State after:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ (Fs, δ ++ [β]).1
⊢ evaluate M v f

State before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ (Fs, δ ++ [β]).1
⊢ evaluate M v f
Tactic:
simp at f_in
State after:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f

State before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f
Tactic:
specialize u_Fs f f_in
State after:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f

State before:
case refine_2
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
f : Formula
f_in : f ∈ Fs
u_Fs : evaluate M v f
⊢ evaluate M v f
Tactic:
assumption
State after:
no goals

State before:
case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ relateSeq M (Fs, δ ++ [β]).2 v w
Tactic:
simp [relateSeq_append]
State after:
case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w

State before:
case refine_3
W✝ : Type
M : KripkeModel W✝
v w : W✝
α β : Program
u : W✝
v_α_u : relate M α v u
u_β_w : relate M β u w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H α
u_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_u : relateSeq M δ v u
hyp : ¬δ = ε
⊢ ∃ u, relateSeq M δ v u ∧ relate M β u w
Tactic:
use u
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : relate M (∗β) v w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
simp only [relate] at v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have := ReflTransGen.cases_tail_eq_neq v_γ_w
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
this : v = w ∨ v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
this : v = w ∨ v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
cases this
State after:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v = w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

case inr
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case inl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
h✝ : v = w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
subst_eqs
State after:
case inl.refl
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v

State before:
case inl.refl
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v
Tactic:
use ⟨∅, ε⟩
State after:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ (∅, ε) ∈ H (∗β) ∧ (M, v)⊨(∅, ε).1 ∧ relateSeq M (∅, ε).2 v v

State before:
case h
W✝ : Type
M : KripkeModel W✝
v : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v v
⊢ (∅, ε) ∈ H (∗β) ∧ (M, v)⊨(∅, ε).1 ∧ relateSeq M (∅, ε).2 v v
Tactic:
simp [H, relateSeq]
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
hyp : v ≠ w ∧ ∃ y, v ≠ y ∧ relate M β v y ∧ Relation.ReflTransGen (relate M β) y w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases hyp with ⟨_, ⟨v1, v_neq_v1, v_β_v1, v1_βS_w⟩⟩
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
have IHβ := existsDiamondH v_β_v1
State after:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
IHβ : ∃ Fδ ∈ H β, (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
rcases IHβ with ⟨⟨Fs,δ⟩, Fδ_in, v_Fs, v_δ_v1⟩
State after:
case intro.intro.intro.intro.intro.mk.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w

State before:
case intro.intro.intro.intro.intro.mk.intro.intro
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ Fδ ∈ H (∗β), (M, v)⊨Fδ.1 ∧ relateSeq M Fδ.2 v w
Tactic:
use ⟨Fs, δ ++ [∗β]⟩
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β) ∧ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β) ∧ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w
Tactic:
constructor
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β)

case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (Fs, δ ++ [∗β]) ∈ H (∗β)
Tactic:
simp [H] at *
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Tactic:
have claim : δ ≠ ε := by
  by_contra hyp
  subst_eqs
  simp [relateSeq] at v_δ_v1
  tauto
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ ∃ l, (∃ a b, (a, b) ∈ H β ∧ (if b = [] then [] else [(a, b ++ [∗β])]) = l) ∧ (Fs, δ ++ [∗β]) ∈ l
Tactic:
refine ⟨_, ⟨⟨Fs, δ, ⟨Fδ_in, by rfl⟩⟩, ?_⟩⟩
State after:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ (Fs, δ ++ [∗β]) ∈ if δ = [] then [] else [(Fs, δ ++ [∗β])]

State before:
case h.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ (Fs, δ ++ [∗β]) ∈ if δ = [] then [] else [(Fs, δ ++ [∗β])]
Tactic:
simp_all
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ δ ≠ ε
Tactic:
by_contra hyp
State after:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
hyp : δ = ε
⊢ False

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
hyp : δ = ε
⊢ False
Tactic:
subst_eqs
State after:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : relateSeq M ε v v1
⊢ False

State before:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : relateSeq M ε v v1
⊢ False
Tactic:
simp [relateSeq] at v_δ_v1
State after:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : v = v1
⊢ False

State before:
case refl
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
v_Fs : ∀ f ∈ Fs, evaluate M v f
Fδ_in : (Fs, ε) ∈ H β
v_δ_v1 : v = v1
⊢ False
Tactic:
tauto
State after:
no goals

State before:
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
claim : δ ≠ ε
⊢ (if δ = [] then [] else [(Fs, δ ++ [∗β])]) = ?m.1478336
Tactic:
rfl
State after:
no goals

State before:
case h.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1 ∧ relateSeq M (Fs, δ ++ [∗β]).2 v w
Tactic:
constructor
State after:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1

case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M (Fs, δ ++ [∗β]).2 v w

State before:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ (M, v)⊨(Fs, δ ++ [∗β]).1
Tactic:
intro f f_in
State after:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ (Fs, δ ++ [∗β]).1
⊢ evaluate M v f

State before:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ (Fs, δ ++ [∗β]).1
⊢ evaluate M v f
Tactic:
simp at f_in
State after:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f

State before:
case h.right.left
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
f : Formula
f_in : f ∈ Fs
⊢ evaluate M v f
Tactic:
exact v_Fs f f_in
State after:
no goals

State before:
case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M (Fs, δ ++ [∗β]).2 v w
Tactic:
rw [relateSeq_append]
State after:
case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ u, relateSeq M δ v u ∧ relateSeq M [∗β] u w

State before:
case h.right.right
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ ∃ u, relateSeq M δ v u ∧ relateSeq M [∗β] u w
Tactic:
use v1
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M δ v v1 ∧ relateSeq M [∗β] v1 w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : v ≠ w
v1 : W✝
v_neq_v1 : v ≠ v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : (M, v)⊨(Fs, δ).1
v_δ_v1 : relateSeq M (Fs, δ).2 v v1
⊢ relateSeq M δ v v1 ∧ relateSeq M [∗β] v1 w
Tactic:
simp [relateSeq] at *
State after:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ relateSeq M δ v v1 ∧ Relation.ReflTransGen (relate M β) v1 w

State before:
case h
W✝ : Type
M : KripkeModel W✝
v w : W✝
β : Program
v_γ_w : Relation.ReflTransGen (relate M β) v w
left✝ : ¬v = w
v1 : W✝
v_neq_v1 : ¬v = v1
v_β_v1 : relate M β v v1
v1_βS_w : Relation.ReflTransGen (relate M β) v1 w
Fs : List Formula
δ : List Program
Fδ_in : (Fs, δ) ∈ H β
v_Fs : ∀ f ∈ Fs, evaluate M v f
v_δ_v1 : relateSeq M δ v v1
⊢ relateSeq M δ v v1 ∧ Relation.ReflTransGen (relate M β) v1 w
Tactic:
tauto
State after:
no goals