Theorem: LO.FirstOrder.Completeness.top_inaccessible (Logic/FirstOrder/Completeness/SearchTree.lean)

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 Γ)
⊢ ¬Acc (SearchTree.Lt T Γ) ⊤
Tactic:
intro A
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
⊢ False

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
⊢ False
Tactic:
have : WellFounded (SearchTree.Lt T Γ) := ⟨by
  rintro ⟨s, Δ, a⟩
  induction a
  case zero => exact A
  case succ s Δ₁ Δ₂ a r ih => exact ih.inv (SearchTree.Lt.intro a r)⟩
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
this : WellFounded (SearchTree.Lt T Γ)
⊢ False

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
this : WellFounded (SearchTree.Lt T Γ)
⊢ False
Tactic:
contradiction
State after:
no goals

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
⊢ ∀ (a : SearchTree T Γ), Acc (SearchTree.Lt T Γ) a
Tactic:
rintro ⟨s, Δ, a⟩
State after:
case mk.mk
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
a : SearchTreeAux T Γ s Δ
⊢ Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ, a⟩⟩

State before:
case mk.mk
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
a : SearchTreeAux T Γ s Δ
⊢ Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ, a⟩⟩
Tactic:
induction a
State after:
case mk.mk.zero
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
⊢ Acc (SearchTree.Lt T Γ) ⟨0, ⟨Γ, SearchTreeAux.zero⟩⟩

case mk.mk.succ
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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
s✝ : ℕ
Δ₁✝ Δ₂✝ : Sequent L
a✝¹ : SearchTreeAux T Γ s✝ Δ₁✝
a✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
a_ih✝ : Acc (SearchTree.Lt T Γ) ⟨s✝, ⟨Δ₁✝, a✝¹⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s✝ + 1, ⟨Δ₂✝, a✝¹.succ a✝⟩⟩

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
⊢ Acc (SearchTree.Lt T Γ) ⟨0, ⟨Γ, SearchTreeAux.zero⟩⟩
Tactic:
case zero => exact A
State after:
no goals

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s✝ : ℕ
Δ : Sequent L
s : ℕ
Δ₁ Δ₂ : Sequent L
a : SearchTreeAux T Γ s Δ₁
r : Δ₂ ≺⟨s⟩ Δ₁
ih : Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ₁, a⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩
Tactic:
case succ s Δ₁ Δ₂ a r ih => exact ih.inv (SearchTree.Lt.intro a r)
State after:
no goals

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s : ℕ
Δ : Sequent L
⊢ Acc (SearchTree.Lt T Γ) ⟨0, ⟨Γ, SearchTreeAux.zero⟩⟩
Tactic:
exact A
State after:
no goals

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 Γ)
A : Acc (SearchTree.Lt T Γ) ⊤
s✝ : ℕ
Δ : Sequent L
s : ℕ
Δ₁ Δ₂ : Sequent L
a : SearchTreeAux T Γ s Δ₁
r : Δ₂ ≺⟨s⟩ Δ₁
ih : Acc (SearchTree.Lt T Γ) ⟨s, ⟨Δ₁, a⟩⟩
⊢ Acc (SearchTree.Lt T Γ) ⟨s + 1, ⟨Δ₂, a.succ r⟩⟩
Tactic:
exact ih.inv (SearchTree.Lt.intro a r)
State after:
no goals