internlm/Lean-Github huggingface dataset:
Theorem: existsWitnessPath
Proof state before:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ (M, v)⊨(~⌈⌈δ⌉⌉ξ)
Tactic:
simp [modelCanSemImplyForm, evaluatePoint] at *
Proof state after:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)
Theorem: existsWitnessPath
Proof state before:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)
Tactic:
have := existsWitnessPath_rtl M wit.length v δ ξ wit
Proof state after:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
this : wit.length = wit.length → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)
Theorem: existsWitnessPath
Proof state before:
case mpr.intro
W : Type
ξ : Formula
M : KripkeModel W
δ : List Program
v : W
wit : witness M v δ ξ
this : wit.length = wit.length → evaluate M v (~⌈⌈δ⌉⌉ξ)
⊢ ¬evaluate M v (⌈⌈δ⌉⌉ξ)
Tactic:
simp_all
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
α : Program
⊢ x ∉ voc α → ∀ (F : List Formula) (δ : List Program), (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
Tactic:
intro x_notin F δ Fδ_in_H
Proof state after:
x : ℕ
α : Program
x_notin : x ∉ voc α
F : List Formula
δ : List Program
Fδ_in_H : (F, δ) ∈ H α
⊢ x ∉ voc F ∧ x ∉ voc δ
Theorem: keepFreshH
Proof state before:
x : ℕ
α : Program
x_notin : x ∉ voc α
F : List Formula
δ : List Program
Fδ_in_H : (F, δ) ∈ H α
⊢ x ∉ voc F ∧ x ∉ voc δ
Tactic:
cases α
Proof state after:
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : x ∉ voc (·a✝)
Fδ_in_H : (F, δ) ∈ H (·a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹;'a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹;'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹⋓a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹⋓a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ voc (∗a✝)
Fδ_in_H : (F, δ) ∈ H (∗a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ
Theorem: keepFreshH
Proof state before:
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : x ∉ voc (·a✝)
Fδ_in_H : (F, δ) ∈ H (·a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹;'a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹;'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ voc (a✝¹⋓a✝)
Fδ_in_H : (F, δ) ∈ H (a✝¹⋓a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ voc (∗a✝)
Fδ_in_H : (F, δ) ∈ H (∗a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ
Tactic:
all_goals
  simp [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram] at *
Proof state after:
case atom_prog
x : ℕ
F : List Formula
δ : List Program
a✝ : ℕ
x_notin : ¬x = a✝
Fδ_in_H : F = [] ∧ δ = [·a✝]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
Fδ_in_H : F = [] ∧ δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
case atom_prog a =>
  cases Fδ_in_H
  subst_eqs
  simp [vocabOfProgram]
  assumption
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
case test =>
  cases Fδ_in_H
  subst_eqs
  aesop
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case sequence
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case union
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1

case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
all_goals
  constructor <;> intro y y_in
Proof state after:
case sequence.left
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case sequence.right
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H a✝¹ ∧
          (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H a✝)).join else [(a, b ++ [a✝])]) = l) ∧
      (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

case union.left
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case union.right
x : ℕ
F : List Formula
δ : List Program
a✝¹ a✝ : Program
x_notin : x ∉ vocabOfProgram a✝¹ ∧ x ∉ vocabOfProgram a✝
Fδ_in_H : (F, δ) ∈ H a✝¹ ∨ (F, δ) ∈ H a✝
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y

case star.left
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case star.right
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ voc (?'a✝)
Fδ_in_H : (F, δ) ∈ H (?'a✝)
⊢ x ∉ voc F ∧ x ∉ voc δ
Tactic:
simp [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram] at *
Proof state after:
case test
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
Fδ_in_H : F = [] ∧ δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
cases Fδ_in_H
Proof state after:
case intro
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
left✝ : F = []
right✝ : δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Theorem: keepFreshH
Proof state before:
case intro
x : ℕ
F : List Formula
δ : List Program
a : ℕ
x_notin : ¬x = a
left✝ : F = []
right✝ : δ = [·a]
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
subst_eqs
Proof state after:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ (∀ x_1 ∈ [], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [·a], x ∉ vocabOfProgram x_1
Theorem: keepFreshH
Proof state before:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ (∀ x_1 ∈ [], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [·a], x ∉ vocabOfProgram x_1
Tactic:
simp [vocabOfProgram]
Proof state after:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ ¬x = a
Theorem: keepFreshH
Proof state before:
case intro.refl.refl
x a : ℕ
x_notin : ¬x = a
⊢ ¬x = a
Tactic:
assumption
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
Fδ_in_H : F = [a✝] ∧ δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
cases Fδ_in_H
Proof state after:
case intro
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
left✝ : F = [a✝]
right✝ : δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Theorem: keepFreshH
Proof state before:
case intro
x : ℕ
F : List Formula
δ : List Program
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
left✝ : F = [a✝]
right✝ : δ = []
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
subst_eqs
Proof state after:
case intro.refl.refl
x : ℕ
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
⊢ (∀ x_1 ∈ [a✝], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [], x ∉ vocabOfProgram x_1
Theorem: keepFreshH
Proof state before:
case intro.refl.refl
x : ℕ
a✝ : Formula
x_notin : x ∉ vocabOfFormula a✝
⊢ (∀ x_1 ∈ [a✝], x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ [], x ∉ vocabOfProgram x_1
Tactic:
aesop
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case star
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
⊢ (∀ x_1 ∈ F, x ∉ vocabOfFormula x_1) ∧ ∀ x_1 ∈ δ, x ∉ vocabOfProgram x_1
Tactic:
constructor <;> intro y y_in
Proof state after:
case star.left
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y

case star.right
x : ℕ
F : List Formula
δ : List Program
a✝ : Program
x_notin : x ∉ vocabOfProgram a✝
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H a✝ ∧ (if b = [] then [] else [(a, b ++ [∗a✝])]) = l) ∧ (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H :
  ∃ l,
    (∃ a b,
        (a, b) ∈ H α ∧ (if b = [] then (List.map (fun x => [(a ∪ x.1, x.2)]) (H β)).join else [(a, b ++ [β])]) = l) ∧
      (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
Tactic:
rcases Fδ_in_H with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in, def_l⟩⟩, Fδ_in_l⟩⟩
Proof state after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
def_l : (if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]) = l
⊢ x ∉ vocabOfFormula y
Tactic:
subst def_l
Proof state after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then (List.map (fun x => [(F' ∪ x.1, x.2)]) (H β)).join else [(F', δ' ++ [β])]
⊢ x ∉ vocabOfFormula y
Tactic:
cases em (δ' = []) <;> simp_all
Proof state after:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfFormula y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' : List Formula
δ' : List Program
y_in : y ∈ F'
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
h✝ : δ' = []
⊢ x ∉ vocabOfFormula y
Tactic:
subst_eqs
Proof state after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Tactic:
have IHα := keepFreshH α x_notin.1 F' [] Fδ'_in
Proof state after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : x ∉ voc F' ∧ x ∉ voc []
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
⊢ x ∉ vocabOfFormula y
Tactic:
rcases Fδ_in_l with ⟨l', ⟨⟨a', b', ⟨a'b'_in_Hβ, def_l'⟩⟩, Fδ_in_l'⟩⟩
Proof state after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
l' : List (List Formula × List Program)
Fδ_in_l' : (F, δ) ∈ l'
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
def_l' : [(F' ∪ a', b')] = l'
⊢ x ∉ vocabOfFormula y
Tactic:
subst_eqs
Proof state after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : (F, δ) ∈ [(F' ∪ a', b')]
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
F' : List Formula
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a' : List Formula
b' : List Program
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : (F, δ) ∈ [(F' ∪ a', b')]
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all
Proof state after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
y_in : y ∈ F' ∨ y ∈ a'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
y_in : y ∈ F' ∨ y ∈ a'
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
⊢ x ∉ vocabOfFormula y
Tactic:
cases y_in
Proof state after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ x ∉ vocabOfFormula y

case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ x ∉ vocabOfFormula y
Tactic:
apply IHα
Proof state after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl.a
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ y ∈ F'
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inl.a
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ F'
⊢ y ∈ F'
Tactic:
assumption
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
⊢ x ∉ vocabOfFormula y
Tactic:
have IHβ := keepFreshH β x_notin.2 a' b' a'b'_in_Hβ
Proof state after:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inl.refl.intro.intro.intro.intro.intro.refl.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
F' a' : List Formula
b' : List Program
Fδ'_in : (F', []) ∈ H α
IHα : ∀ x_1 ∈ F', x ∉ vocabOfFormula x_1
a'b'_in_Hβ : (a', b') ∈ H β
Fδ_in_l' : F = F' ∪ a' ∧ δ = b'
h✝ : y ∈ a'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals