Theorem: localBoxTruth' (Pdl/Unfold.lean)

State before:
γ : Program
ψ : Formula
ℓ : TP γ
⊢ (⌈γ⌉ψ)⋀signature γ ℓ≡Con (Xset γ ℓ ψ)⋀signature γ ℓ
Tactic:
cases γ
State after:
case atom_prog
ψ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
⊢ (⌈·a✝⌉ψ)⋀signature (·a✝) ℓ≡Con (Xset (·a✝) ℓ ψ)⋀signature (·a✝) ℓ

case sequence
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
⊢ (⌈a✝¹;'a✝⌉ψ)⋀signature (a✝¹;'a✝) ℓ≡Con (Xset (a✝¹;'a✝) ℓ ψ)⋀signature (a✝¹;'a✝) ℓ

case union
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
⊢ (⌈a✝¹⋓a✝⌉ψ)⋀signature (a✝¹⋓a✝) ℓ≡Con (Xset (a✝¹⋓a✝) ℓ ψ)⋀signature (a✝¹⋓a✝) ℓ

case star
ψ : Formula
a✝ : Program
ℓ : TP (∗a✝)
⊢ (⌈∗a✝⌉ψ)⋀signature (∗a✝) ℓ≡Con (Xset (∗a✝) ℓ ψ)⋀signature (∗a✝) ℓ

case test
ψ a✝ : Formula
ℓ : TP (?'a✝)
⊢ (⌈?'a✝⌉ψ)⋀signature (?'a✝) ℓ≡Con (Xset (?'a✝) ℓ ψ)⋀signature (?'a✝) ℓ

State before:
ψ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
⊢ (⌈·a✝⌉ψ)⋀signature (·a✝) ℓ≡Con (Xset (·a✝) ℓ ψ)⋀signature (·a✝) ℓ
Tactic:
case atom_prog =>
  sorry
State after:
no goals

State before:
ψ a✝ : Formula
ℓ : TP (?'a✝)
⊢ (⌈?'a✝⌉ψ)⋀signature (?'a✝) ℓ≡Con (Xset (?'a✝) ℓ ψ)⋀signature (?'a✝) ℓ
Tactic:
case test =>
  sorry
State after:
no goals

State before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
⊢ (⌈a✝¹⋓a✝⌉ψ)⋀signature (a✝¹⋓a✝) ℓ≡Con (Xset (a✝¹⋓a✝) ℓ ψ)⋀signature (a✝¹⋓a✝) ℓ
Tactic:
case union =>
  sorry
State after:
no goals

State before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
⊢ (⌈a✝¹;'a✝⌉ψ)⋀signature (a✝¹;'a✝) ℓ≡Con (Xset (a✝¹;'a✝) ℓ ψ)⋀signature (a✝¹;'a✝) ℓ
Tactic:
case sequence =>
  sorry
State after:
no goals

State before:
ψ : Formula
a✝ : Program
ℓ : TP (∗a✝)
⊢ (⌈∗a✝⌉ψ)⋀signature (∗a✝) ℓ≡Con (Xset (∗a✝) ℓ ψ)⋀signature (∗a✝) ℓ
Tactic:
case star =>
  sorry
State after:
no goals

State before:
ψ : Formula
a✝ : ℕ
ℓ : TP (·a✝)
⊢ (⌈·a✝⌉ψ)⋀signature (·a✝) ℓ≡Con (Xset (·a✝) ℓ ψ)⋀signature (·a✝) ℓ
Tactic:
sorry
State after:
no goals

State before:
ψ a✝ : Formula
ℓ : TP (?'a✝)
⊢ (⌈?'a✝⌉ψ)⋀signature (?'a✝) ℓ≡Con (Xset (?'a✝) ℓ ψ)⋀signature (?'a✝) ℓ
Tactic:
sorry
State after:
no goals

State before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
⊢ (⌈a✝¹⋓a✝⌉ψ)⋀signature (a✝¹⋓a✝) ℓ≡Con (Xset (a✝¹⋓a✝) ℓ ψ)⋀signature (a✝¹⋓a✝) ℓ
Tactic:
sorry
State after:
no goals

State before:
ψ : Formula
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
⊢ (⌈a✝¹;'a✝⌉ψ)⋀signature (a✝¹;'a✝) ℓ≡Con (Xset (a✝¹;'a✝) ℓ ψ)⋀signature (a✝¹;'a✝) ℓ
Tactic:
sorry
State after:
no goals

State before:
ψ : Formula
a✝ : Program
ℓ : TP (∗a✝)
⊢ (⌈∗a✝⌉ψ)⋀signature (∗a✝) ℓ≡Con (Xset (∗a✝) ℓ ψ)⋀signature (∗a✝) ℓ
Tactic:
sorry
State after:
no goals