Theorem: LO.FirstOrder.Completeness.chainSet_verum (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 Γ)
⊢ ⊤ ∉ ⛓️
Tactic:
simp[chainSet]
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 Γ)
⊢ ∀ (x : ℕ), ⊤ ∉ ⛓️[x]

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 Γ)
⊢ ∀ (x : ℕ), ⊤ ∉ ⛓️[x]
Tactic:
intro s h
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
⊢ 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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
⊢ False
Tactic:
have : ⊤ ∈ ⛓️[(encode (Code.verum : Code L)).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) h
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
⊢ 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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
⊢ False
Tactic:
have : ¬⊤ ∈ ⛓️[(encode (Code.verum : Code L)).pair s] := by
  have : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s] := chain_spec' nwf _ _
  generalize ⛓️[(encode (Code.verum : Code L)).pair s + 1] = Δ' at this
  rcases this; assumption
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ 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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ 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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
have : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s] := chain_spec' nwf _ _
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]

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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
this : ⛓️[(encode Code.verum).pair s + 1] ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
generalize ⛓️[(encode (Code.verum : Code L)).pair s + 1] = Δ' at this
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
Δ' : Sequent L
this : Δ' ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]

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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this✝ : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
Δ' : Sequent L
this : Δ' ≺[Code.verum] ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
rcases this
State after:
case verumRefl
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
a✝ : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]

State before:
case verumRefl
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 Γ)
s : ℕ
h : ⊤ ∈ ⛓️[s]
this : ⊤ ∈ ⛓️[(encode Code.verum).pair s]
a✝ : ⊤ ∉ ⛓️[(encode Code.verum).pair s]
⊢ ⊤ ∉ ⛓️[(encode Code.verum).pair s]
Tactic:
assumption
State after:
no goals