Theorem: LO.FirstOrder.Completeness.SearchTree.seq_of_lt (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
τ₁ τ₂ : SearchTree T Γ
h : Lt T Γ τ₂ τ₁
⊢ τ₂.seq ≺⟨τ₁.rank⟩ τ₁.seq
Tactic:
cases h
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
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ seq ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ ≺⟨rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩⟩ seq ⟨s✝, ⟨Δ₁✝, a✝⟩⟩

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
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ seq ⟨s✝ + 1, ⟨Δ₂✝, a✝.succ r✝⟩⟩ ≺⟨rank ⟨s✝, ⟨Δ₁✝, a✝⟩⟩⟩ seq ⟨s✝, ⟨Δ₁✝, a✝⟩⟩
Tactic:
simp[rank, seq]
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
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ Δ₂✝ ≺⟨s✝⟩ Δ₁✝

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
s✝ : ℕ
Δ₂✝ Δ₁✝ : Sequent L
a✝ : SearchTreeAux T Γ s✝ Δ₁✝
r✝ : Δ₂✝ ≺⟨s✝⟩ Δ₁✝
⊢ Δ₂✝ ≺⟨s✝⟩ Δ₁✝
Tactic:
assumption
State after:
no goals