Theorem: repl_in_P_non_occ_eq (Pdl/Substitution.lean)

State before:
x : ℕ
α : Program
ρ : Formula
⊢ x ∉ voc α → repl_in_P x ρ α = α
Tactic:
intro x_notin_alpha
State after:
x : ℕ
α : Program
ρ : Formula
x_notin_alpha : x ∉ voc α
⊢ repl_in_P x ρ α = α

State before:
x : ℕ
α : Program
ρ : Formula
x_notin_alpha : x ∉ voc α
⊢ repl_in_P x ρ α = α
Tactic:
cases α
State after:
case atom_prog
x : ℕ
ρ : Formula
a✝ : ℕ
x_notin_alpha : x ∉ voc (·a✝)
⊢ repl_in_P x ρ (·a✝) = ·a✝

case sequence
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ voc (a✝¹;'a✝)
⊢ repl_in_P x ρ (a✝¹;'a✝) = (a✝¹;'a✝)

case union
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ voc (a✝¹⋓a✝)
⊢ repl_in_P x ρ (a✝¹⋓a✝) = (a✝¹⋓a✝)

case star
x : ℕ
ρ : Formula
a✝ : Program
x_notin_alpha : x ∉ voc (∗a✝)
⊢ repl_in_P x ρ (∗a✝) = (∗a✝)

case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ voc (?'a✝)
⊢ repl_in_P x ρ (?'a✝) = (?'a✝)

State before:
case atom_prog
x : ℕ
ρ : Formula
a✝ : ℕ
x_notin_alpha : x ∉ voc (·a✝)
⊢ repl_in_P x ρ (·a✝) = ·a✝

case sequence
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ voc (a✝¹;'a✝)
⊢ repl_in_P x ρ (a✝¹;'a✝) = (a✝¹;'a✝)

case union
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ voc (a✝¹⋓a✝)
⊢ repl_in_P x ρ (a✝¹⋓a✝) = (a✝¹⋓a✝)

case star
x : ℕ
ρ : Formula
a✝ : Program
x_notin_alpha : x ∉ voc (∗a✝)
⊢ repl_in_P x ρ (∗a✝) = (∗a✝)

case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ voc (?'a✝)
⊢ repl_in_P x ρ (?'a✝) = (?'a✝)
Tactic:
all_goals simp [voc,vocabOfProgram] at *
State after:
case sequence
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
⊢ repl_in_P x ρ a✝¹ = a✝¹ ∧ repl_in_P x ρ a✝ = a✝

case union
x : ℕ
ρ : Formula
a✝¹ a✝ : Program
x_notin_alpha : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
⊢ repl_in_P x ρ a✝¹ = a✝¹ ∧ repl_in_P x ρ a✝ = a✝

case star
x : ℕ
ρ : Formula
a✝ : Program
x_notin_alpha : x ∉ vocabOfProgram a✝
⊢ repl_in_P x ρ a✝ = a✝

case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ vocabOfFormula a✝
⊢ repl_in_F x ρ a✝ = a✝

State before:
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ repl_in_P x ρ β = β ∧ repl_in_P x ρ γ = γ
Tactic:
case sequence β γ =>
  constructor <;> (apply repl_in_P_non_occ_eq; tauto)
State after:
no goals

State before:
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ repl_in_P x ρ β = β ∧ repl_in_P x ρ γ = γ
Tactic:
case union β γ =>
  constructor <;> (apply repl_in_P_non_occ_eq; tauto)
State after:
no goals

State before:
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ repl_in_P x ρ β = β
Tactic:
case star β =>
  apply repl_in_P_non_occ_eq ; tauto
State after:
no goals

State before:
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ repl_in_F x ρ φ = φ
Tactic:
case test φ =>
  apply repl_in_F_non_occ_eq; tauto
State after:
no goals

State before:
case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ voc (?'a✝)
⊢ repl_in_P x ρ (?'a✝) = (?'a✝)
Tactic:
simp [voc,vocabOfProgram] at *
State after:
case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ vocabOfFormula a✝
⊢ repl_in_F x ρ a✝ = a✝

State before:
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ repl_in_P x ρ β = β ∧ repl_in_P x ρ γ = γ
Tactic:
constructor <;> (apply repl_in_P_non_occ_eq; tauto)
State after:
no goals

State before:
case right
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ repl_in_P x ρ γ = γ
Tactic:
apply repl_in_P_non_occ_eq
State after:
case right.a
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ x ∉ voc γ

State before:
case right.a
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ x ∉ voc γ
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ repl_in_P x ρ β = β
Tactic:
apply repl_in_P_non_occ_eq
State after:
case a
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ x ∉ voc β

State before:
case a
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ x ∉ voc β
Tactic:
tauto
State after:
no goals

State before:
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ repl_in_F x ρ φ = φ
Tactic:
apply repl_in_F_non_occ_eq
State after:
case a
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ x ∉ voc φ

State before:
case a
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ x ∉ voc φ
Tactic:
tauto
State after:
no goals