all_goals
  simp_all [isAtomic, isStar, P]
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✝)
case sequence
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹;'a✝)
δ_in :
  (∃ a ∈ List.filter (fun x => x != []) (P a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [a✝] = δ) ∨
    δ ∈ if [] ∈ P a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩ then P a✝ fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case union
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝¹ a✝ : Program
ℓ : TP (a✝¹⋓a✝)
δ_in : (δ ∈ P a✝¹ fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P a✝ fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram a✝¹ + lengthOfProgram a✝

case star
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Program
ℓ : TP (∗a✝)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P a✝ fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗a✝] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram a✝

case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ if ℓ ⟨a✝, ⋯⟩ = true then [[]] else []
⊢ lengthOfProgram γ < 2 + lengthOfFormula a✝