internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
case intro.allRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
{ have : ∀' p ∈ ⛓️[(encode $ Code.all p).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
  contradiction }
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
⊢ ∃ s, ∀' p ∈ ⛓️[s]
Tactic:
simpa[chainSet] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
case intro.all
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
a✝ : ∀' p ∈ ⛓️[(encode (Code.all p)).pair s]
hΔ :
  ⛓️[(encode (Code.all p)).pair s + 1] =
    [→ &(newVar ⛓️[(encode (Code.all p)).pair s])].hom p :: ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
exact ⟨&(newVar ⛓️[(encode $ Code.all p).pair s]), Set.mem_iUnion.mpr ⟨(encode $ Code.all p).pair s + 1, by simp[hΔ]⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
a✝ : ∀' p ∈ ⛓️[(encode (Code.all p)).pair s]
hΔ :
  ⛓️[(encode (Code.all p)).pair s + 1] =
    [→ &(newVar ⛓️[(encode (Code.all p)).pair s])].hom p :: ⛓️[(encode (Code.all p)).pair s]
⊢ [→ &(newVar ⛓️[(encode (Code.all p)).pair s])].hom p ∈ {x | x ∈ ⛓️[(encode (Code.all p)).pair s + 1]}
Tactic:
simp[hΔ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
case intro.allRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
have : ∀' p ∈ ⛓️[(encode $ Code.all p).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
Proof state after:
case intro.allRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
this : ∀' p ∈ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
case intro.allRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
this : ∀' p ∈ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
⊢ [→ t].hom p ∈ ⛓️
Tactic:
have : ∃ s, ∃' p ∈ ⛓️[s] := by simpa[chainSet] using h
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
this : ∃ s, ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
this : ∃ s, ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
rcases this with ⟨s, hs⟩
Proof state after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
have : ⛓️[(encode $ Code.ex p t).pair s + 1] ≺[Code.ex p t] ⛓️[(encode $ Code.ex p t).pair s] := chain_spec' nwf _ _
Proof state after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.ex p t)).pair s + 1] ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.ex p t)).pair s + 1] ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.ex p t).pair s + 1] = Δ at this
Proof state after:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = Δ
this : Δ ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = Δ
this : Δ ≺[Code.ex p t] ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
rcases this
Proof state after:
case intro.ex
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro.ex
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️

case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
{ exact Set.mem_iUnion.mpr ⟨(encode $ Code.ex p t).pair s + 1, by simp[hΔ]⟩ }
Proof state after:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
{ have : ∃' p ∈ ⛓️[(encode $ Code.ex p t).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
  contradiction }
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
⊢ ∃ s, ∃' p ∈ ⛓️[s]
Tactic:
simpa[chainSet] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro.ex
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
exact Set.mem_iUnion.mpr ⟨(encode $ Code.ex p t).pair s + 1, by simp[hΔ]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
a✝ : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = [→ t].hom p :: ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ {x | x ∈ ⛓️[(encode (Code.ex p t)).pair s + 1]}
Tactic:
simp[hΔ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
have : ∃' p ∈ ⛓️[(encode $ Code.ex p t).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
Proof state after:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
this : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_ex
Proof state before:
case intro.exRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p : SyntacticSemiformula L 1
h : ∃' p ∈ ⛓️
t : Semiterm L ℕ 0
s : ℕ
hs : ∃' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.ex p t)).pair s + 1] = ⛓️[(encode (Code.ex p t)).pair s]
a✝ : ∃' p ∉ ⛓️[(encode (Code.ex p t)).pair s]
this : ∃' p ∈ ⛓️[(encode (Code.ex p t)).pair s]
⊢ [→ t].hom p ∈ ⛓️
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
have : ⛓️[(encode $ Code.id σ).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode $ Code.id σ).pair 0] := chain_spec' nwf _ _
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.id σ).pair 0 + 1] = Δ
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
this : ⛓️[(encode (Code.id σ)).pair 0 + 1] ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
rw[hΔ] at this
Proof state after:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
Δ : Sequent L
this : Δ ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
Δ : Sequent L
this : Δ ≺[Code.id σ] ⛓️[(encode (Code.id σ)).pair 0]
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = Δ
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
rcases this
Proof state after:
case id
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

case idRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
case id
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️

case idRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
{ exact Set.mem_iUnion.mpr ⟨(encode $ Code.id σ).pair 0 + 1, by simp[hΔ]⟩ }
Proof state after:
case idRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
case idRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
{ contradiction }
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
case id
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
exact Set.mem_iUnion.mpr ⟨(encode $ Code.id σ).pair 0 + 1, by simp[hΔ]⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h hσ✝ : σ ∈ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ~Rew.emb.hom σ :: ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ {x | x ∈ ⛓️[(encode (Code.id σ)).pair 0 + 1]}
Tactic:
simp[hΔ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_id
Proof state before:
case idRefl
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
σ : Sentence L
h : σ ∈ T
hσ✝ : σ ∉ T
hΔ : ⛓️[(encode (Code.id σ)).pair 0 + 1] = ⛓️[(encode (Code.id σ)).pair 0]
⊢ ~Rew.emb.hom σ ∈ ⛓️
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.Model.val
Proof state before:
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
n : ℕ
e : Fin n → SyntacticTerm L
ε : ℕ → Model T Γ
t : SyntacticSemiterm L n
⊢ Semiterm.val (structure T Γ) e ε t = (Rew.bind e ε) t
Tactic:
induction t <;> simp[*, Semiterm.val_func, Rew.func]
Proof state after:
case func
L : Language
inst✝³ : (k : ℕ) → DecidableEq (L.Func k)
inst✝² : (k : ℕ) → DecidableEq (L.Rel k)
inst✝¹ : (k : ℕ) → Encodable (L.Func k)
inst✝ : (k : ℕ) → Encodable (L.Rel k)
T : Theory L
Γ : Sequent L
nwf : ¬WellFounded (SearchTree.Lt T Γ)
n : ℕ
e : Fin n → SyntacticTerm L
ε : ℕ → Model T Γ
arity✝ : ℕ
a✝¹ : L.Func arity✝
a✝ : Fin arity✝ → Semiterm L ℕ n
a_ih✝ : ∀ (a : Fin arity✝), Semiterm.val (structure T Γ) e ε (a✝ a) = (Rew.bind e ε) (a✝ a)
⊢ (Structure.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)) = Semiterm.func a✝¹ fun i => (Rew.bind e ε) (a✝ i)