internlm/Lean-Github huggingface dataset:
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof 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
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof 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
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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₂⟩⟩
Proof 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
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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₂⟩
Proof 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
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof 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
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof 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₂]
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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₂⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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]
Proof 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₂)]
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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 _ _
Proof 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₂)]
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof 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₂)]
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof 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₂)]
Theorem: LO.FirstOrder.Completeness.chainSet_axL
Proof 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
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
have : ∃ s, p ⋏ q ∈ ⛓️[s] := by simpa[chainSet] using h
Proof 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
this : ∃ s, p ⋏ q ∈ ⛓️[s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
this : ∃ s, p ⋏ q ∈ ⛓️[s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
rcases this with ⟨s, hs⟩
Proof 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
have : ⛓️[(encode $ Code.and p q).pair s + 1] ≺[Code.and p q] ⛓️[(encode $ Code.and p q).pair s] := chain_spec' nwf _ _
Proof 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
this : ⛓️[(encode (Code.and p q)).pair s + 1] ≺[Code.and p q] ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
this : ⛓️[(encode (Code.and p q)).pair s + 1] ≺[Code.and p q] ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.and p q).pair s + 1] = Δ at this
Proof 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = Δ
this : Δ ≺[Code.and p q] ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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
nwf : ¬WellFounded (SearchTree.Lt T Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = Δ
this : Δ ≺[Code.and p q] ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
rcases this
Proof state after:
case intro.and₁
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
a✝ : p ⋏ q ∈ ⛓️[(encode (Code.and p q)).pair s]
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = p :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️

case intro.and₂
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
a✝ : p ⋏ q ∈ ⛓️[(encode (Code.and p q)).pair s]
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = q :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️

case intro.andRefl
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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = ⛓️[(encode (Code.and p q)).pair s]
a✝ : p ⋏ q ∉ ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
a✝ : p ⋏ q ∈ ⛓️[(encode (Code.and p q)).pair s]
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = p :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
case and₁ =>
  exact Or.inl (Set.mem_iUnion.mpr ⟨(encode $ Code.and p q).pair s + 1, by simp[hΔ]⟩)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_and
Proof 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
s : ℕ
hs : p ⋏ q ∈ ⛓️[s]
a✝ : p ⋏ q ∈ ⛓️[(encode (Code.and p q)).pair s]
hΔ : ⛓️[(encode (Code.and p q)).pair s + 1] = q :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
case and₂ =>
  exact Or.inr (Set.mem_iUnion.mpr ⟨(encode $ Code.and p q).pair s + 1, by simp[hΔ]⟩)
Proof state after:
no goals