Theorem: LO.FirstOrder.Completeness.chainSet_axL (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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
⊢ rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️
Tactic:
by_contra 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
⊢ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
⊢ False
Tactic:
have : (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ (∃ s₂, nrel r v ∈ ⛓️[s₂]) := by
  have h : rel r v ∈ ⛓️ ∧ nrel r v ∈ ⛓️ := by simpa[not_or] using h
  simpa[chainSet] using 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
this : (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ ∃ s₂, nrel r v ∈ ⛓️[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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
this : (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ ∃ s₂, nrel r v ∈ ⛓️[s₂]
⊢ False
Tactic:
rcases this with ⟨⟨s₁, hs₁⟩, ⟨s₂, hs₂⟩⟩
State after:
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
⊢ False

State before:
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
⊢ False
Tactic:
have : rel r v ∈ ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂)] := by
  exact ⟨chain_monotone nwf (le_trans (by simp) (Nat.right_le_pair _ _)) hs₁,
  chain_monotone nwf (le_trans (by simp) (Nat.right_le_pair _ _)) hs₂⟩
State after:
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ False

State before:
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ False
Tactic:
have : ¬(rel r v ∈ ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂)]) := by
  rw[not_and_or]
  have : ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂) + 1] ≺[Code.axL r v] ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂)] := chain_spec' nwf _ _
  generalize ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂) + 1] = Δ' at this
  rcases this; assumption
State after:
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
this :
  ¬(rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)])
⊢ False

State before:
case intro.intro.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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
this :
  ¬(rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
⊢ (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ ∃ s₂, nrel r v ∈ ⛓️[s₂]
Tactic:
have h : rel r v ∈ ⛓️ ∧ nrel r v ∈ ⛓️ := by simpa[not_or] using 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h✝ : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
h : rel r v ∈ ⛓️ ∧ nrel r v ∈ ⛓️
⊢ (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ ∃ s₂, nrel r v ∈ ⛓️[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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h✝ : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
h : rel r v ∈ ⛓️ ∧ nrel r v ∈ ⛓️
⊢ (∃ s₁, rel r v ∈ ⛓️[s₁]) ∧ ∃ s₂, nrel r v ∈ ⛓️[s₂]
Tactic:
simpa[chainSet] using h
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
⊢ rel r v ∈ ⛓️ ∧ nrel r v ∈ ⛓️
Tactic:
simpa[not_or] using h
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
⊢ rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Tactic:
exact ⟨chain_monotone nwf (le_trans (by simp) (Nat.right_le_pair _ _)) hs₁,
chain_monotone nwf (le_trans (by simp) (Nat.right_le_pair _ _)) hs₂⟩
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
⊢ s₁ ≤ max s₁ s₂
Tactic:
simp
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
⊢ s₂ ≤ max s₁ s₂
Tactic:
simp
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ ¬(rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)])
Tactic:
rw[not_and_or]
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Tactic:
have : ⛓️[(encode $ Code.axL r v).pair (max s₁ s₂) + 1] ≺[Code.axL r v] ⛓️[(encode $ Code.axL r v).pair (max s₁ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
this : ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂) + 1] ≺[Code.axL r v] ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
this : ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂) + 1] ≺[Code.axL r v] ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Tactic:
generalize ⛓️[(encode $ Code.axL r v).pair (max s₁ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Δ' : Sequent L
this : Δ' ≺[Code.axL r v] ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ 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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this✝ : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Δ' : Sequent L
this : Δ' ≺[Code.axL r v] ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Tactic:
rcases this
State after:
case axLRefl
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
a✝ : rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]

State before:
case axLRefl
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 Γ)
k : ℕ
r : L.Rel k
v : Fin k → SyntacticTerm L
h : ¬(rel r v ∉ ⛓️ ∨ nrel r v ∉ ⛓️)
s₁ : ℕ
hs₁ : rel r v ∈ ⛓️[s₁]
s₂ : ℕ
hs₂ : nrel r v ∈ ⛓️[s₂]
this : rel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∧ nrel r v ∈ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
a✝ : rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
⊢ rel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)] ∨ nrel r v ∉ ⛓️[(encode (Code.axL r v)).pair (max s₁ s₂)]
Tactic:
assumption
State after:
no goals