internlm/Lean-Github huggingface dataset:
Theorem: keepFreshH
Proof state before:
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
Tactic:
have := keepFreshH α x_notin.1 F' δ' Fδ'_in
Proof state after:
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✝ : ¬δ' = []
this : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
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✝ : ¬δ' = []
this : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
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 : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = β
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
F' : List Formula
Fδ'_in : (F', []) ∈ H α
Fδ_in_l : ∃ l, (∃ a b, (a, b) ∈ H β ∧ [(F' ∪ a, b)] = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
y_in : y ∈ δ
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 ∉ vocabOfProgram 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 : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
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 ∉ vocabOfProgram 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 : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
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 ∉ vocabOfProgram 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
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
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'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfProgram 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 : Program
F' a' : List Formula
b' : List Program
y_in : y ∈ b'
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'
IHβ : x ∉ voc a' ∧ x ∉ voc b'
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
y_in : y ∈ δ' ∨ y = β
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram y
Tactic:
cases y_in
Proof state after:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y

case intro.intro.intro.intro.intro.inr.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y = β
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin.1 F' δ' Fδ'_in
Proof state after:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y ∈ δ'
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝¹ : ¬δ' = []
h✝ : y = β
⊢ x ∉ vocabOfProgram y
Tactic:
subst_eqs
Proof state after:
case intro.intro.intro.intro.intro.inr.inr.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram β
Theorem: keepFreshH
Proof state before:
case intro.intro.intro.intro.intro.inr.inr.refl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
F' : List Formula
δ' : List Program
Fδ'_in : (F', δ') ∈ H α
Fδ_in_l : F = F' ∧ δ = δ' ++ [β]
h✝ : ¬δ' = []
⊢ x ∉ vocabOfProgram β
Tactic:
tauto
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H : (F, δ) ∈ H α ∨ (F, δ) ∈ H β
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
Tactic:
cases Fδ_in_H
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfFormula y

case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfFormula y
Tactic:
have IHα := keepFreshH α x_notin.1 F δ
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfFormula y
Tactic:
have IHβ := keepFreshH β x_notin.2 F δ
Proof state after:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Formula
y_in : y ∈ F
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfFormula y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
Fδ_in_H : (F, δ) ∈ H α ∨ (F, δ) ∈ H β
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Tactic:
cases Fδ_in_H
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfProgram y

case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
⊢ x ∉ vocabOfProgram y
Tactic:
have IHα := keepFreshH α x_notin.1 F δ
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H α
IHα : (F, δ) ∈ H α → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
⊢ x ∉ vocabOfProgram y
Tactic:
have IHβ := keepFreshH β x_notin.2 F δ
Proof state after:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y
Theorem: keepFreshH
Proof state before:
case inr
x : ℕ
F : List Formula
δ : List Program
α β : Program
x_notin : x ∉ vocabOfProgram α ∧ x ∉ vocabOfProgram β
y : Program
y_in : y ∈ δ
h✝ : (F, δ) ∈ H β
IHβ : (F, δ) ∈ H β → x ∉ voc F ∧ x ∉ voc δ
⊢ x ∉ vocabOfProgram y
Tactic:
simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
y : Formula
y_in : y ∈ F
⊢ x ∉ vocabOfFormula y
Tactic:
cases Fδ_in_H
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfFormula y

case inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Tactic:
case inr hyp =>
  rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, def_l⟩⟩, Fδ_in_l⟩⟩
  subst def_l
  have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
  cases em (δ' = []) <;> simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfFormula y
Tactic:
exfalso
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ False
Theorem: keepFreshH
Proof state before:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
h✝ : F = [] ∧ δ = []
⊢ False
Tactic:
simp_all
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
hyp : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfFormula y
Tactic:
rcases hyp with ⟨l, ⟨⟨F', δ', ⟨Fδ'_in_Hα, 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 α
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] 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 α
y : Formula
y_in : y ∈ F
l : List (List Formula × List Program)
Fδ_in_l : (F, δ) ∈ l
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
def_l : (if δ' = [] then [] 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 α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] 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 α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
⊢ x ∉ vocabOfFormula y
Tactic:
have IHα := keepFreshH α x_notin F' δ' Fδ'_in_Hα
Proof state after:
case intro.intro.intro.intro.intro
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ 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 α
y : Formula
y_in : y ∈ F
F' : List Formula
δ' : List Program
Fδ'_in_Hα : (F', δ') ∈ H α
Fδ_in_l : (F, δ) ∈ if δ' = [] then [] else [(F', δ' ++ [∗α])]
IHα : x ∉ voc F' ∧ x ∉ voc δ'
⊢ x ∉ vocabOfFormula y
Tactic:
cases em (δ' = []) <;> simp_all [H, voc,vocabOfListFormula,vocabOfListProgram,vocabOfFormula,vocabOfProgram]
Proof state after:
no goals
Theorem: keepFreshH
Proof state before:
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
Fδ_in_H : F = [] ∧ δ = [] ∨ ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
y : Program
y_in : y ∈ δ
⊢ x ∉ vocabOfProgram y
Tactic:
cases Fδ_in_H
Proof state after:
case inl
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : F = [] ∧ δ = []
⊢ x ∉ vocabOfProgram y

case inr
x : ℕ
F : List Formula
δ : List Program
α : Program
x_notin : x ∉ vocabOfProgram α
y : Program
y_in : y ∈ δ
h✝ : ∃ l, (∃ a b, (a, b) ∈ H α ∧ (if b = [] then [] else [(a, b ++ [∗α])]) = l) ∧ (F, δ) ∈ l
⊢ x ∉ vocabOfProgram y