Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux (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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
h : Δ₂ ≺⟨(encode c).pair i⟩ Δ₁
⊢ Δ₂ ≺[c] Δ₁
Tactic:
rcases h with (⟨h, r⟩ | ⟨h⟩)
State after:
case redux
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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
h : decode ((encode c).pair i).unpair.1 = some c✝
r : Δ₂ ≺[c✝] Δ₁
⊢ Δ₂ ≺[c] Δ₁

case refl
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
c : Code L
i : ℕ
Δ₂ : Sequent L
h : decode ((encode c).pair i).unpair.1 = none
⊢ Δ₂ ≺[c] Δ₂

State before:
case redux
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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
h : decode ((encode c).pair i).unpair.1 = some c✝
r : Δ₂ ≺[c✝] Δ₁
⊢ Δ₂ ≺[c] Δ₁

case refl
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
c : Code L
i : ℕ
Δ₂ : Sequent L
h : decode ((encode c).pair i).unpair.1 = none
⊢ Δ₂ ≺[c] Δ₂
Tactic:
{ simp at h; simpa[h] using r }
State after:
case refl
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
c : Code L
i : ℕ
Δ₂ : Sequent L
h : decode ((encode c).pair i).unpair.1 = none
⊢ Δ₂ ≺[c] Δ₂

State before:
case refl
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
c : Code L
i : ℕ
Δ₂ : Sequent L
h : decode ((encode c).pair i).unpair.1 = none
⊢ Δ₂ ≺[c] Δ₂
Tactic:
{ simp at h }
State after:
no goals

State before:
case redux
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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
h : decode ((encode c).pair i).unpair.1 = some c✝
r : Δ₂ ≺[c✝] Δ₁
⊢ Δ₂ ≺[c] Δ₁
Tactic:
simp at h
State after:
case redux
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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
r : Δ₂ ≺[c✝] Δ₁
h : c = c✝
⊢ Δ₂ ≺[c] Δ₁

State before:
case redux
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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
r : Δ₂ ≺[c✝] Δ₁
h : c = c✝
⊢ Δ₂ ≺[c] Δ₁
Tactic:
simpa[h] using r
State after:
no goals

State before:
case refl
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
c : Code L
i : ℕ
Δ₂ : Sequent L
h : decode ((encode c).pair i).unpair.1 = none
⊢ Δ₂ ≺[c] Δ₂
Tactic:
simp at h
State after:
no goals