cases α
γ : Program
δ : List Program
α : Program
ℓ : TP α
γ_in : γ ∈ δ
δ_in : δ ∈ P α ℓ
⊢ if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
case atom_prog
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : ℕ
ℓ : TP (·a✝)
δ_in : δ ∈ P (·a✝) ℓ
⊢ if isAtomic (·a✝) = true then γ = ·a✝
  else
    if isStar (·a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (·a✝) else lengthOfProgram γ < lengthOfProgram (·a✝)

case sequence
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
δ_in : δ ∈ P (a✝¹;'a✝) ℓ
⊢ if isAtomic (a✝¹;'a✝) = true then γ = (a✝¹;'a✝)
  else
    if isStar (a✝¹;'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (a✝¹;'a✝)
    else lengthOfProgram γ < lengthOfProgram (a✝¹;'a✝)

case union
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
δ_in : δ ∈ P (a✝¹⋓a✝) ℓ
⊢ if isAtomic (a✝¹⋓a✝) = true then γ = (a✝¹⋓a✝)
  else
    if isStar (a✝¹⋓a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (a✝¹⋓a✝)
    else lengthOfProgram γ < lengthOfProgram (a✝¹⋓a✝)

case star
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Program
ℓ : TP (∗a✝)
δ_in : δ ∈ P (∗a✝) ℓ
⊢ if isAtomic (∗a✝) = true then γ = (∗a✝)
  else
    if isStar (∗a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (∗a✝) else lengthOfProgram γ < lengthOfProgram (∗a✝)

case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ P (?'a✝) ℓ
⊢ if isAtomic (?'a✝) = true then γ = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram γ ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram γ < lengthOfProgram (?'a✝)