Theorem: repl_in_boxes_non_occ_eq (Pdl/Substitution.lean)

State before:
x : ℕ
ψ : Formula
δ : List Program
⊢ x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Tactic:
intro nonOcc
State after:
x : ℕ
ψ : Formula
δ : List Program
nonOcc : x ∉ voc δ
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ

State before:
x : ℕ
ψ : Formula
δ : List Program
nonOcc : x ∉ voc δ
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Tactic:
induction δ
State after:
case nil
x : ℕ
ψ : Formula
nonOcc : x ∉ voc []
⊢ repl_in_F x ψ (⌈⌈[]⌉⌉~·x) = ⌈⌈[]⌉⌉~ψ

case cons
x : ℕ
ψ : Formula
head✝ : Program
tail✝ : List Program
tail_ih✝ : x ∉ voc tail✝ → repl_in_F x ψ (⌈⌈tail✝⌉⌉~·x) = ⌈⌈tail✝⌉⌉~ψ
nonOcc : x ∉ voc (head✝ :: tail✝)
⊢ repl_in_F x ψ (⌈⌈head✝ :: tail✝⌉⌉~·x) = ⌈⌈head✝ :: tail✝⌉⌉~ψ

State before:
case nil
x : ℕ
ψ : Formula
nonOcc : x ∉ voc []
⊢ repl_in_F x ψ (⌈⌈[]⌉⌉~·x) = ⌈⌈[]⌉⌉~ψ
Tactic:
simp
State after:
no goals

State before:
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_F x ψ (⌈⌈α :: δ⌉⌉~·x) = ⌈⌈α :: δ⌉⌉~ψ
Tactic:
simp only [Formula.boxes, repl_in_F, Formula.box.injEq]
State after:
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_P x ψ α = α ∧ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ

State before:
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_P x ψ α = α ∧ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Tactic:
constructor
State after:
case left
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_P x ψ α = α

case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ

State before:
case left
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_P x ψ α = α
Tactic:
apply repl_in_P_non_occ_eq
State after:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc α

State before:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc α
Tactic:
simp [voc,vocabOfProgram,vocabOfListProgram] at *
State after:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : (∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram α

State before:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : (∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
⊢ x ∉ vocabOfProgram α
Tactic:
intro _
State after:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : (∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
a✝ : x ∈ vocabOfProgram α
⊢ False

State before:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : (∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1) → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
a✝ : x ∈ vocabOfProgram α
⊢ False
Tactic:
simp_all
State after:
no goals

State before:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Tactic:
apply IH
State after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ

State before:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
Tactic:
clear IH
State after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ

State before:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
Tactic:
simp [voc,vocabOfProgram,vocabOfListProgram] at *
State after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
⊢ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

State before:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
⊢ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
intro d d_in
State after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
d : Program
d_in : d ∈ δ
⊢ x ∉ vocabOfProgram d

State before:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
d : Program
d_in : d ∈ δ
⊢ x ∉ vocabOfProgram d
Tactic:
simp_all
State after:
no goals