cases γ
γ : Program
ψ : Formula
ℓ : TP γ
⊢ (⌈γ⌉ψ)⋀signature γ ℓ≡Con (Xset γ ℓ ψ)⋀signature γ ℓ
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✝) ℓ