internlm/Lean-Github huggingface dataset:
Theorem: repl_in_Con
Proof state before:
x : ℕ
ψ φ1 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: l)) = Con (List.map (repl_in_F x ψ) (φ1 :: l))
Tactic:
cases l
Proof state after:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (Con [φ1]) = Con (List.map (repl_in_F x ψ) [φ1])

case cons
x : ℕ
ψ φ1 head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: head✝ :: tail✝)) = Con (List.map (repl_in_F x ψ) (φ1 :: head✝ :: tail✝))
Theorem: repl_in_Con
Proof state before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: φ2 :: l)) = Con (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
case cons φ2 l =>
  simp [Con]
  apply repl_in_Con
Proof state after:
no goals
Theorem: repl_in_Con
Proof state before:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (Con [φ1]) = Con (List.map (repl_in_F x ψ) [φ1])
Tactic:
simp
Proof state after:
no goals
Theorem: repl_in_Con
Proof state before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ1 :: φ2 :: l)) = Con (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
simp [Con]
Proof state after:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ2 :: l)) = Con (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)
Theorem: repl_in_Con
Proof state before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (Con (φ2 :: l)) = Con (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)
Tactic:
apply repl_in_Con
Proof state after:
no goals
Theorem: repl_in_dis
Proof state before:
x : ℕ
ψ : Formula
l : List Formula
⊢ repl_in_F x ψ (dis l) = dis (List.map (repl_in_F x ψ) l)
Tactic:
cases l
Proof state after:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (dis []) = dis (List.map (repl_in_F x ψ) [])

case cons
x : ℕ
ψ head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (dis (head✝ :: tail✝)) = dis (List.map (repl_in_F x ψ) (head✝ :: tail✝))
Theorem: repl_in_dis
Proof state before:
case nil
x : ℕ
ψ : Formula
⊢ repl_in_F x ψ (dis []) = dis (List.map (repl_in_F x ψ) [])
Tactic:
simp
Proof state after:
no goals
Theorem: repl_in_dis
Proof state before:
x : ℕ
ψ φ1 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: l)) = dis (List.map (repl_in_F x ψ) (φ1 :: l))
Tactic:
cases l
Proof state after:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (dis [φ1]) = dis (List.map (repl_in_F x ψ) [φ1])

case cons
x : ℕ
ψ φ1 head✝ : Formula
tail✝ : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: head✝ :: tail✝)) = dis (List.map (repl_in_F x ψ) (φ1 :: head✝ :: tail✝))
Theorem: repl_in_dis
Proof state before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: φ2 :: l)) = dis (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
case cons φ2 l =>
  simp [dis]
  apply repl_in_dis
Proof state after:
no goals
Theorem: repl_in_dis
Proof state before:
case nil
x : ℕ
ψ φ1 : Formula
⊢ repl_in_F x ψ (dis [φ1]) = dis (List.map (repl_in_F x ψ) [φ1])
Tactic:
simp
Proof state after:
no goals
Theorem: repl_in_dis
Proof state before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ1 :: φ2 :: l)) = dis (List.map (repl_in_F x ψ) (φ1 :: φ2 :: l))
Tactic:
simp [dis]
Proof state after:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ2 :: l)) = dis (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)
Theorem: repl_in_dis
Proof state before:
x : ℕ
ψ φ1 φ2 : Formula
l : List Formula
⊢ repl_in_F x ψ (dis (φ2 :: l)) = dis (repl_in_F x ψ φ2 :: List.map (repl_in_F x ψ) l)
Tactic:
apply repl_in_dis
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
φ ρ : Formula
⊢ x ∉ voc φ → repl_in_F x ρ φ = φ
Tactic:
intro x_notin_phi
Proof state after:
x : ℕ
φ ρ : Formula
x_notin_phi : x ∉ voc φ
⊢ repl_in_F x ρ φ = φ
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
φ ρ : Formula
x_notin_phi : x ∉ voc φ
⊢ repl_in_F x ρ φ = φ
Tactic:
cases φ
Proof state after:
case bottom
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom

case atom_prop
x : ℕ
ρ : Formula
a✝ : ℕ
x_notin_phi : x ∉ voc (·a✝)
⊢ repl_in_F x ρ (·a✝) = ·a✝

case neg
x : ℕ
ρ a✝ : Formula
x_notin_phi : x ∉ voc (~a✝)
⊢ repl_in_F x ρ (~a✝) = (~a✝)

case and
x : ℕ
ρ a✝¹ a✝ : Formula
x_notin_phi : x ∉ voc (a✝¹⋀a✝)
⊢ repl_in_F x ρ (a✝¹⋀a✝) = a✝¹⋀a✝

case box
x : ℕ
ρ : Formula
a✝¹ : Program
a✝ : Formula
x_notin_phi : x ∉ voc (⌈a✝¹⌉a✝)
⊢ repl_in_F x ρ (⌈a✝¹⌉a✝) = ⌈a✝¹⌉a✝
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom
Tactic:
case bottom => simp
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ repl_in_F x ρ (·c) = ·c
Tactic:
case atom_prop c =>
  simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
  intro c_is_x; simp [voc,vocabOfFormula] at *; tauto
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ voc (~φ0)
⊢ repl_in_F x ρ (~φ0) = (~φ0)
Tactic:
case neg φ0 =>
  simp [voc,vocabOfFormula] at *
  apply repl_in_F_non_occ_eq; tauto
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ voc (φ1⋀φ2)
⊢ repl_in_F x ρ (φ1⋀φ2) = φ1⋀φ2
Tactic:
case and φ1 φ2 =>
  simp [voc,vocabOfFormula] at *
  constructor <;> (apply repl_in_F_non_occ_eq ; tauto)
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
x_notin_phi : x ∉ voc Formula.bottom
⊢ repl_in_F x ρ Formula.bottom = Formula.bottom
Tactic:
simp
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ repl_in_F x ρ (·c) = ·c
Tactic:
simp only [repl_in_F, beq_iff_eq, ite_eq_right_iff]
Proof state after:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ c = x → ρ = ·c
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
⊢ c = x → ρ = ·c
Tactic:
intro c_is_x
Proof state after:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
c_is_x : c = x
⊢ ρ = ·c
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
c : ℕ
x_notin_phi : x ∉ voc (·c)
c_is_x : c = x
⊢ ρ = ·c
Tactic:
simp [voc,vocabOfFormula] at *
Proof state after:
x : ℕ
ρ : Formula
c : ℕ
c_is_x : c = x
x_notin_phi : ¬x = c
⊢ ρ = ·c
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
c : ℕ
c_is_x : c = x
x_notin_phi : ¬x = c
⊢ ρ = ·c
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ voc (~φ0)
⊢ repl_in_F x ρ (~φ0) = (~φ0)
Tactic:
simp [voc,vocabOfFormula] at *
Proof state after:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
Tactic:
apply repl_in_F_non_occ_eq
Proof state after:
case a
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0
Theorem: repl_in_F_non_occ_eq
Proof state before:
case a
x : ℕ
ρ φ0 : Formula
x_notin_phi : x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ voc (φ1⋀φ2)
⊢ repl_in_F x ρ (φ1⋀φ2) = φ1⋀φ2
Tactic:
simp [voc,vocabOfFormula] at *
Proof state after:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ1 = φ1 ∧ repl_in_F x ρ φ2 = φ2
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ1 = φ1 ∧ repl_in_F x ρ φ2 = φ2
Tactic:
constructor <;> (apply repl_in_F_non_occ_eq ; tauto)
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
case right
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ repl_in_F x ρ φ2 = φ2
Tactic:
apply repl_in_F_non_occ_eq
Proof state after:
case right.a
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ x ∉ voc φ2
Theorem: repl_in_F_non_occ_eq
Proof state before:
case right.a
x : ℕ
ρ φ1 φ2 : Formula
x_notin_phi : x ∉ vocabOfFormula φ1 ∧ x ∉ vocabOfFormula φ2
⊢ x ∉ voc φ2
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ voc (⌈α⌉φ0)
⊢ repl_in_F x ρ (⌈α⌉φ0) = ⌈α⌉φ0
Tactic:
simp [voc,vocabOfFormula] at *
Proof state after:
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α ∧ repl_in_F x ρ φ0 = φ0
Theorem: repl_in_F_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α ∧ repl_in_F x ρ φ0 = φ0
Tactic:
constructor
Proof state after:
case left
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α

case right
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
Theorem: repl_in_F_non_occ_eq
Proof state before:
case left
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_P x ρ α = α
Tactic:
apply repl_in_P_non_occ_eq
Proof state after:
case left.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc α
Theorem: repl_in_F_non_occ_eq
Proof state before:
case left.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc α
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_F_non_occ_eq
Proof state before:
case right
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ repl_in_F x ρ φ0 = φ0
Tactic:
apply repl_in_F_non_occ_eq
Proof state after:
case right.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0
Theorem: repl_in_F_non_occ_eq
Proof state before:
case right.a
x : ℕ
ρ : Formula
α : Program
φ0 : Formula
x_notin_phi : x ∉ vocabOfProgram α ∧ x ∉ vocabOfFormula φ0
⊢ x ∉ voc φ0
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof state before:
x : ℕ
α : Program
ρ : Formula
⊢ x ∉ voc α → repl_in_P x ρ α = α
Tactic:
intro x_notin_alpha
Proof state after:
x : ℕ
α : Program
ρ : Formula
x_notin_alpha : x ∉ voc α
⊢ repl_in_P x ρ α = α
Theorem: repl_in_P_non_occ_eq
Proof state before:
x : ℕ
α : Program
ρ : Formula
x_notin_alpha : x ∉ voc α
⊢ repl_in_P x ρ α = α
Tactic:
cases α
Proof 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✝)
Theorem: repl_in_P_non_occ_eq
Proof 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 *
Proof 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✝
Theorem: repl_in_P_non_occ_eq
Proof 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)
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof 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)
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof 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
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof state before:
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ repl_in_F x ρ φ = φ
Tactic:
case test φ =>
  apply repl_in_F_non_occ_eq; tauto
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof state before:
case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ voc (?'a✝)
⊢ repl_in_P x ρ (?'a✝) = (?'a✝)
Tactic:
simp [voc,vocabOfProgram] at *
Proof state after:
case test
x : ℕ
ρ a✝ : Formula
x_notin_alpha : x ∉ vocabOfFormula a✝
⊢ repl_in_F x ρ a✝ = a✝
Theorem: repl_in_P_non_occ_eq
Proof 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)
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof 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
Proof state after:
case right.a
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ x ∉ voc γ
Theorem: repl_in_P_non_occ_eq
Proof state before:
case right.a
x : ℕ
ρ : Formula
β γ : Program
x_notin_alpha : x ∉ vocabOfProgram β ∧ x ∉ vocabOfProgram γ
⊢ x ∉ voc γ
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ repl_in_P x ρ β = β
Tactic:
apply repl_in_P_non_occ_eq
Proof state after:
case a
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ x ∉ voc β
Theorem: repl_in_P_non_occ_eq
Proof state before:
case a
x : ℕ
ρ : Formula
β : Program
x_notin_alpha : x ∉ vocabOfProgram β
⊢ x ∉ voc β
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_P_non_occ_eq
Proof state before:
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ repl_in_F x ρ φ = φ
Tactic:
apply repl_in_F_non_occ_eq
Proof state after:
case a
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ x ∉ voc φ
Theorem: repl_in_P_non_occ_eq
Proof state before:
case a
x : ℕ
ρ φ : Formula
x_notin_alpha : x ∉ vocabOfFormula φ
⊢ x ∉ voc φ
Tactic:
tauto
Proof state after:
no goals
Theorem: repl_in_boxes_non_occ_eq
Proof state before:
x : ℕ
ψ : Formula
δ : List Program
⊢ x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Tactic:
intro nonOcc
Proof state after:
x : ℕ
ψ : Formula
δ : List Program
nonOcc : x ∉ voc δ
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Theorem: repl_in_boxes_non_occ_eq
Proof state before:
x : ℕ
ψ : Formula
δ : List Program
nonOcc : x ∉ voc δ
⊢ repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
Tactic:
induction δ
Proof 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✝⌉⌉~ψ
Theorem: repl_in_boxes_non_occ_eq
Proof state before:
case nil
x : ℕ
ψ : Formula
nonOcc : x ∉ voc []
⊢ repl_in_F x ψ (⌈⌈[]⌉⌉~·x) = ⌈⌈[]⌉⌉~ψ
Tactic:
simp
Proof state after:
no goals
Theorem: repl_in_boxes_non_occ_eq
Proof 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]
Proof 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) = ⌈⌈δ⌉⌉~ψ
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof 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) = ⌈⌈δ⌉⌉~ψ
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof state after:
case left.a
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc α
Theorem: repl_in_boxes_non_occ_eq
Proof 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 *
Proof 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 α
Theorem: repl_in_boxes_non_occ_eq
Proof 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 _
Proof 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
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof state after:
no goals
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof state after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
IH : x ∉ voc δ → repl_in_F x ψ (⌈⌈δ⌉⌉~·x) = ⌈⌈δ⌉⌉~ψ
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof state after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
Theorem: repl_in_boxes_non_occ_eq
Proof state before:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ voc (α :: δ)
⊢ x ∉ voc δ
Tactic:
simp [voc,vocabOfProgram,vocabOfListProgram] at *
Proof state after:
case right
x : ℕ
ψ : Formula
α : Program
δ : List Program
nonOcc : x ∉ vocabOfProgram α ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
⊢ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof 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
Theorem: repl_in_boxes_non_occ_eq
Proof 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
Proof state after:
no goals
Theorem: repl_in_list_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
F : List Formula
⊢ x ∉ voc F → List.map (repl_in_F x ρ) F = F
Tactic:
intro nonOcc
Proof state after:
x : ℕ
ρ : Formula
F : List Formula
nonOcc : x ∉ voc F
⊢ List.map (repl_in_F x ρ) F = F
Theorem: repl_in_list_non_occ_eq
Proof state before:
x : ℕ
ρ : Formula
F : List Formula
nonOcc : x ∉ voc F
⊢ List.map (repl_in_F x ρ) F = F
Tactic:
induction F
Proof state after:
case nil
x : ℕ
ρ : Formula
nonOcc : x ∉ voc []
⊢ List.map (repl_in_F x ρ) [] = []

case cons
x : ℕ
ρ head✝ : Formula
tail✝ : List Formula
tail_ih✝ : x ∉ voc tail✝ → List.map (repl_in_F x ρ) tail✝ = tail✝
nonOcc : x ∉ voc (head✝ :: tail✝)
⊢ List.map (repl_in_F x ρ) (head✝ :: tail✝) = head✝ :: tail✝
Theorem: repl_in_list_non_occ_eq
Proof state before:
case nil
x : ℕ
ρ : Formula
nonOcc : x ∉ voc []
⊢ List.map (repl_in_F x ρ) [] = []
Tactic:
simp
Proof state after:
no goals
Theorem: repl_in_list_non_occ_eq
Proof state before:
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ List.map (repl_in_F x ρ) (φ :: F) = φ :: F
Tactic:
simp only [List.map_cons, List.cons.injEq]
Proof state after:
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ ∧ List.map (repl_in_F x ρ) F = F
Theorem: repl_in_list_non_occ_eq
Proof state before:
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ ∧ List.map (repl_in_F x ρ) F = F
Tactic:
constructor
Proof state after:
case left
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ

case right
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ List.map (repl_in_F x ρ) F = F
Theorem: repl_in_list_non_occ_eq
Proof state before:
case left
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ repl_in_F x ρ φ = φ
Tactic:
apply repl_in_F_non_occ_eq
Proof state after:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc φ
Theorem: repl_in_list_non_occ_eq
Proof state before:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : x ∉ voc F → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ voc (φ :: F)
⊢ x ∉ voc φ
Tactic:
simp [voc,vocabOfProgram,vocabOfListFormula] at *
Proof state after:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula φ
Theorem: repl_in_list_non_occ_eq
Proof state before:
case left.a
x : ℕ
ρ φ : Formula
F : List Formula
IH : (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) → List.map (repl_in_F x ρ) F = F
nonOcc : x ∉ vocabOfFormula φ ∧ ∀ x_1 ∈ F, x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula φ
Tactic:
exact nonOcc.left
Proof state after:
no goals