Theorem: P_goes_down (Pdl/Unfold.lean)

State before:
γ : Program
δ : List Program
α : Program
ℓ : TP α
⊢ γ ∈ δ →
    δ ∈ P α ℓ →
      if isAtomic α = true then γ = α
      else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
Tactic:
intro γ_in δ_in
State after:
γ : Program
δ : List Program
α : Program
ℓ : TP α
γ_in : γ ∈ δ
δ_in : δ ∈ P α ℓ
⊢ if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α

State before:
γ : Program
δ : List Program
α : Program
ℓ : TP α
γ_in : γ ∈ δ
δ_in : δ ∈ P α ℓ
⊢ if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
Tactic:
cases α
State after:
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✝)

State before:
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✝)
Tactic:
all_goals
  simp_all [isAtomic, isStar, P]
State after:
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✝

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case union α β =>
  cases δ_in
  case inl δ_in =>
    have IH := P_goes_down γ_in δ_in
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr δ_in =>
    have IH := P_goes_down γ_in δ_in
    cases em (isAtomic β) <;> cases em (isStar β)
    all_goals (simp_all;try linarith)
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α : Program
ℓ : TP (∗α)
δ_in : δ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = δ
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case star α =>
  cases δ
  case nil =>
    exfalso; cases γ_in
  case cons =>
    simp_all only [false_or]
    rcases δ_in with ⟨αs, αs_in, def_δ⟩
    subst_eqs
    cases em (γ ∈ αs)
    case inl γ_in =>
      have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
      cases em (isAtomic α) <;> cases em (isStar α)
      all_goals (simp_all;try linarith)
    case inr γ_not_in =>
      have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
      subst_eqs
      simp
State after:
no goals

State before:
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✝)
Tactic:
simp_all [isAtomic, isStar, P]
State after:
case test
γ : Program
δ : List Program
γ_in : γ ∈ δ
a✝ : Formula
ℓ : TP (?'a✝)
δ_in : δ ∈ if ℓ ⟨a✝, ⋯⟩ = true then [[]] else []
⊢ lengthOfProgram γ < 2 + lengthOfFormula a✝

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in :
  (∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ) ∨
    δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases δ_in
State after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
h✝ : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
h✝ : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl δ_in =>
  rcases δ_in with ⟨αs, αs_in, def_δ⟩
  subst def_δ
  simp_all
  cases γ_in
  case inl γ_in =>
    have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr γ_in =>
    subst γ_in
    linarith
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩), a ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
rcases δ_in with ⟨αs, αs_in, def_δ⟩
State after:
case intro.intro
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
def_δ : αs ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case intro.intro
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
def_δ : αs ++ [β] = δ
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
subst def_δ
State after:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ++ [β]
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ++ [β]
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ∨ γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case intro.intro
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs ∨ γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases γ_in
State after:
case intro.intro.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
h✝ : γ ∈ αs
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case intro.intro.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
h✝ : γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl γ_in =>
  have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
State after:
no goals

State before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr γ_in =>
  subst γ_in
  linarith
State after:
no goals

State before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
State after:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic α) <;> cases em (isStar α)
State after:
case inl.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
State after:
no goals

State before:
case inr.inr
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
γ α β : Program
ℓ : TP (α;'β)
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
γ_in : γ = β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
subst γ_in
State after:
γ α : Program
αs : List Program
ℓ : TP (α;'γ)
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram γ

State before:
γ α : Program
αs : List Program
ℓ : TP (α;'γ)
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun τ => ℓ ⟨↑τ, ⋯⟩)
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram γ
Tactic:
linarith
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em ([] ∈ P α ℓ)
State after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∉ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in δ_in
State after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝ : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic β) <;> cases em (isStar β)
State after:
case inl.inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl.inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
State after:
no goals

State before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
State after:
no goals

State before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
State after:
no goals

State before:
case inl.inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
h✝² : [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α;'β)
δ_in : δ ∈ if [] ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩ then P β fun τ => ℓ ⟨↑τ, ⋯⟩ else []
h✝ : [] ∉ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : (δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩) ∨ δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases δ_in
State after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
h✝ : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
h✝ : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inl δ_in =>
  have IH := P_goes_down γ_in δ_in
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
case inr δ_in =>
  have IH := P_goes_down γ_in δ_in
  cases em (isAtomic β) <;> cases em (isStar β)
  all_goals (simp_all;try linarith)
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in δ_in
State after:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic α) <;> cases em (isStar α)
State after:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
State after:
no goals

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P α fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
have IH := P_goes_down γ_in δ_in
State after:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
cases em (isAtomic β) <;> cases em (isStar β)
State after:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inl.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inl.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
all_goals (simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
(simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH :
  if isAtomic β = true then γ = β
  else if isStar β = true then lengthOfProgram γ ≤ lengthOfProgram β else lengthOfProgram γ < lengthOfProgram β
h✝¹ : ¬isAtomic β = true
h✝ : ¬isStar β = true
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
simp_all
State after:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
try linarith
State after:
no goals

State before:
case inr.inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
α β : Program
ℓ : TP (α⋓β)
δ_in : δ ∈ P β fun τ => ℓ ⟨↑τ, ⋯⟩
IH : lengthOfProgram γ < lengthOfProgram β
h✝¹ : isAtomic β = false
h✝ : isStar β = false
⊢ lengthOfProgram γ < 1 + lengthOfProgram α + lengthOfProgram β
Tactic:
linarith
State after:
no goals

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

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

State before:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case nil =>
  exfalso; cases γ_in
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case cons =>
  simp_all only [false_or]
  rcases δ_in with ⟨αs, αs_in, def_δ⟩
  subst_eqs
  cases em (γ ∈ αs)
  case inl γ_in =>
    have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
    cases em (isAtomic α) <;> cases em (isStar α)
    all_goals (simp_all;try linarith)
  case inr γ_not_in =>
    have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
    subst_eqs
    simp
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
exfalso
State after:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ False

State before:
γ α : Program
ℓ : TP (∗α)
γ_in : γ ∈ []
δ_in : [] = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = []
⊢ False
Tactic:
cases γ_in
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : head✝ :: tail✝ = [] ∨ ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
simp_all only [false_or]
State after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
δ_in : ∃ a ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩), a ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
rcases δ_in with ⟨αs, αs_in, def_δ⟩
State after:
case intro.intro
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
case intro.intro
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
cases em (γ ∈ αs)
State after:
case intro.intro.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
h✝ : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case intro.intro.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
h✝ : γ ∉ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case inl γ_in =>
  have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
  cases em (isAtomic α) <;> cases em (isStar α)
  all_goals (simp_all;try linarith)
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
case inr γ_not_in =>
  have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
  subst_eqs
  simp
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
have IH := P_goes_down γ_in (List.mem_of_mem_filter αs_in)
State after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
cases em (isAtomic α) <;> cases em (isStar α)
State after:
case inl.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inl.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
case inl.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inl.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inl
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
all_goals (simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
(simp_all;try linarith)
State after:
no goals

State before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in✝ : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH :
  if isAtomic α = true then γ = α
  else if isStar α = true then lengthOfProgram γ ≤ lengthOfProgram α else lengthOfProgram γ < lengthOfProgram α
h✝¹ : ¬isAtomic α = true
h✝ : ¬isStar α = true
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
simp_all
State after:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
try linarith
State after:
no goals

State before:
case inr.inr
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in✝ : γ = head✝ ∨ γ ∈ tail✝
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : γ ∈ αs
IH : lengthOfProgram γ < lengthOfProgram α
h✝¹ : isAtomic α = false
h✝ : isStar α = false
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
linarith
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
have : γ = (∗α) := by rw [← def_δ] at γ_in; simp at γ_in; tauto
State after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
this : γ = (∗α)
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
this : γ = (∗α)
⊢ lengthOfProgram γ ≤ 1 + lengthOfProgram α
Tactic:
subst_eqs
State after:
case refl
α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : (∗α) ∈ head✝ :: tail✝
γ_not_in : (∗α) ∉ αs
⊢ lengthOfProgram (∗α) ≤ 1 + lengthOfProgram α

State before:
case refl
α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_in : (∗α) ∈ head✝ :: tail✝
γ_not_in : (∗α) ∉ αs
⊢ lengthOfProgram (∗α) ≤ 1 + lengthOfProgram α
Tactic:
simp
State after:
no goals

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ : List Program
γ_in : γ ∈ head✝ :: tail✝
αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ γ = (∗α)
Tactic:
rw [← def_δ] at γ_in
State after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in : γ ∈ αs ++ [∗α]
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ γ = (∗α)

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
γ_in : γ ∈ αs ++ [∗α]
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
⊢ γ = (∗α)
Tactic:
simp at γ_in
State after:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
γ_in : γ ∈ αs ∨ γ = (∗α)
⊢ γ = (∗α)

State before:
γ α : Program
ℓ : TP (∗α)
head✝ : Program
tail✝ αs : List Program
αs_in : αs ∈ List.filter (fun x => x != []) (P α fun x => ℓ ⟨↑x, ⋯⟩)
def_δ : αs ++ [∗α] = head✝ :: tail✝
γ_not_in : γ ∉ αs
γ_in : γ ∈ αs ∨ γ = (∗α)
⊢ γ = (∗α)
Tactic:
tauto
State after:
no goals

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Tactic:
cases em (ℓ ⟨τ, by simp [testsOfProgram]⟩)
State after:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ

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

State before:
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
⊢ τ ∈ testsOfProgram (?'τ)
Tactic:
simp [testsOfProgram]
State after:
no goals

State before:
case inl
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Tactic:
simp_all
State after:
no goals

State before:
case inr
γ : Program
δ : List Program
γ_in : γ ∈ δ
τ : Formula
ℓ : TP (?'τ)
δ_in : δ ∈ if ℓ ⟨τ, ⋯⟩ = true then [[]] else []
h✝ : ¬ℓ ⟨τ, ⋯⟩ = true
⊢ lengthOfProgram γ < 2 + lengthOfFormula τ
Tactic:
simp_all
State after:
no goals