Theorem: freshVarForm_is_larger (Pdl/Fresh.lean)

State before:
φ : Formula
⊢ ∀ n ∈ voc φ, n < freshVarForm φ
Tactic:
cases φ
State after:
case bottom

⊢ ∀ n ∈ voc Formula.bottom, n < freshVarForm Formula.bottom

case atom_prop
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarForm (·a✝)

case neg
a✝ : Formula
⊢ ∀ n ∈ voc (~a✝), n < freshVarForm (~a✝)

case and
a✝¹ a✝ : Formula
⊢ ∀ n ∈ voc (a✝¹⋀a✝), n < freshVarForm (a✝¹⋀a✝)

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)

State before:
case bottom

⊢ ∀ n ∈ voc Formula.bottom, n < freshVarForm Formula.bottom

case atom_prop
a✝ : ℕ
⊢ ∀ n ∈ voc (·a✝), n < freshVarForm (·a✝)

case neg
a✝ : Formula
⊢ ∀ n ∈ voc (~a✝), n < freshVarForm (~a✝)

case and
a✝¹ a✝ : Formula
⊢ ∀ n ∈ voc (a✝¹⋀a✝), n < freshVarForm (a✝¹⋀a✝)

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)
Tactic:
all_goals simp [freshVarForm, voc, vocabOfFormula, not_or]
State after:
case neg
a✝ : Formula
⊢ ∀ n ∈ vocabOfFormula a✝, n < freshVarForm a✝

case and
a✝¹ a✝ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula a✝¹ ∨ n ∈ vocabOfFormula a✝ → n < freshVarForm a✝¹ ∨ n < freshVarForm a✝

case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfFormula a✝ → n < freshVarProg a✝¹ ∨ n < freshVarForm a✝

State before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
case neg φ =>
  apply freshVarForm_is_larger
State after:
no goals

State before:
φ1 φ2 : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
case and φ1 φ2 =>
  have IH1 := freshVarForm_is_larger φ1
  have IH2 := freshVarForm_is_larger φ2
  aesop
State after:
no goals

State before:
α : Program
φ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Tactic:
case box α φ =>
  have IHφ := freshVarForm_is_larger φ
  have IHα := freshVarProg_is_larger α
  aesop
State after:
no goals

State before:
case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ n ∈ voc (⌈a✝¹⌉a✝), n < freshVarForm (⌈a✝¹⌉a✝)
Tactic:
simp [freshVarForm, voc, vocabOfFormula, not_or]
State after:
case box
a✝¹ : Program
a✝ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram a✝¹ ∨ n ∈ vocabOfFormula a✝ → n < freshVarProg a✝¹ ∨ n < freshVarForm a✝

State before:
φ : Formula
⊢ ∀ n ∈ vocabOfFormula φ, n < freshVarForm φ
Tactic:
apply freshVarForm_is_larger
State after:
no goals

State before:
φ1 φ2 : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
have IH1 := freshVarForm_is_larger φ1
State after:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2

State before:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
have IH2 := freshVarForm_is_larger φ2
State after:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
IH2 : ∀ n ∈ voc φ2, n < freshVarForm φ2
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2

State before:
φ1 φ2 : Formula
IH1 : ∀ n ∈ voc φ1, n < freshVarForm φ1
IH2 : ∀ n ∈ voc φ2, n < freshVarForm φ2
⊢ ∀ (n : ℕ), n ∈ vocabOfFormula φ1 ∨ n ∈ vocabOfFormula φ2 → n < freshVarForm φ1 ∨ n < freshVarForm φ2
Tactic:
aesop
State after:
no goals

State before:
α : Program
φ : Formula
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ
Tactic:
have IHφ := freshVarForm_is_larger φ
State after:
α : Program
φ : Formula
IHφ : ∀ n ∈ voc φ, n < freshVarForm φ
⊢ ∀ (n : ℕ), n ∈ vocabOfProgram α ∨ n ∈ vocabOfFormula φ → n < freshVarProg α ∨ n < freshVarForm φ

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

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