Theorem: freshVarProg_is_larger (Pdl/Fresh.lean)

State before:
α : Program
⊢ ∀ n ∈ voc α, n < freshVarProg α
Tactic:
cases α
State after:
case atom_prog
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarProg (·a✝)

case sequence
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹;'a✝), n < freshVarProg (a✝¹;'a✝)

case union
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹⋓a✝), n < freshVarProg (a✝¹⋓a✝)

case star
a✝ : Program
⊢ ∀ n ∈ voc (∗a✝), n < freshVarProg (∗a✝)

case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)

State before:
case atom_prog
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarProg (·a✝)

case sequence
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹;'a✝), n < freshVarProg (a✝¹;'a✝)

case union
a✝¹ a✝ : Program
⊢ ∀ n ∈ voc (a✝¹⋓a✝), n < freshVarProg (a✝¹⋓a✝)

case star
a✝ : Program
⊢ ∀ n ∈ voc (∗a✝), n < freshVarProg (∗a✝)

case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)
Tactic:
all_goals simp [freshVarProg, voc, vocabOfProgram]
State after:
case sequence
a✝¹ a✝ : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfProgram a✝ → n < freshVarProg a✝¹ ∨ n < freshVarProg a✝

case union
a✝¹ a✝ : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfProgram a✝ → n < freshVarProg a✝¹ ∨ n < freshVarProg a✝

case star
a✝ : Program
⊢ ∀ n ∈ vocabOfProgram a✝, n < freshVarProg a✝

case test
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝

State before:
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
case union α β =>
  have IHα := freshVarProg_is_larger α
  have IHβ := freshVarProg_is_larger β
  aesop
State after:
no goals

State before:
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
case sequence α β =>
  have IHα := freshVarProg_is_larger α
  have IHβ := freshVarProg_is_larger β
  aesop
State after:
no goals

State before:
α : Program
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Tactic:
case star α =>
  have IHα := freshVarProg_is_larger α
  aesop
State after:
no goals

State before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
case test φ =>
  have IHφ := freshVarForm_is_larger φ
  aesop
State after:
no goals

State before:
case test
a✝ : Formula
⊢ ∀ n ∈ voc (?'a✝), n < freshVarProg (?'a✝)
Tactic:
simp [freshVarProg, voc, vocabOfProgram]
State after:
case test
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝

State before:
α β : Program
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
have IHα := freshVarProg_is_larger α
State after:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β

State before:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
have IHβ := freshVarProg_is_larger β
State after:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
IHβ : ∀ n ∈ voc β, n < freshVarProg β
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β

State before:
α β : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
IHβ : ∀ n ∈ voc β, n < freshVarProg β
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfProgram β → n < freshVarProg α ∨ n < freshVarProg β
Tactic:
aesop
State after:
no goals

State before:
α : Program
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Tactic:
have IHα := freshVarProg_is_larger α
State after:
α : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α

State before:
α : Program
IHα : ∀ n ∈ voc α, n < freshVarProg α
⊢ ∀ n ∈ vocabOfProgram α, n < freshVarProg α
Tactic:
aesop
State after:
no goals

State before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
have IHφ := freshVarForm_is_larger φ
State after:
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ

State before:
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
aesop
State after:
no goals