internlm/Lean-Github huggingface dataset:
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]
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 ∈ ⛓️
Tactic:
case andRefl =>
  have : p ⋏ q ∈ ⛓️[(encode $ Code.and p q).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
  contradiction
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, p ⋏ q ∈ ⛓️[s]
Tactic:
simpa[chainSet] using 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] = p :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
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] = p :: ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ {x | x ∈ ⛓️[(encode (Code.and p q)).pair s + 1]}
Tactic:
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:
exact Or.inr (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]
⊢ q ∈ {x | x ∈ ⛓️[(encode (Code.and p q)).pair s + 1]}
Tactic:
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]
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 ∈ ⛓️
Tactic:
have : p ⋏ q ∈ ⛓️[(encode $ Code.and p q).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
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 ∈ ⛓️
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]
this : 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]
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]
this : p ⋏ q ∈ ⛓️[(encode (Code.and p q)).pair s]
⊢ p ∈ ⛓️ ∨ q ∈ ⛓️
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_or
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_or
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_or
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.or p q).pair s + 1] ≺[Code.or p q] ⛓️[(encode $ Code.or 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.or p q)).pair s + 1] ≺[Code.or p q] ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_or
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.or p q)).pair s + 1] ≺[Code.or p q] ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.or 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.or p q)).pair s + 1] = Δ
this : Δ ≺[Code.or p q] ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_or
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.or p q)).pair s + 1] = Δ
this : Δ ≺[Code.or p q] ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
rcases this
Proof state after:
case intro.or
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.or p q)).pair s]
hΔ : ⛓️[(encode (Code.or p q)).pair s + 1] = p :: q :: ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️

case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_or
Proof state before:
case intro.or
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.or p q)).pair s]
hΔ : ⛓️[(encode (Code.or p q)).pair s + 1] = p :: q :: ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️

case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
{ exact ⟨Set.mem_iUnion.mpr ⟨(encode $ Code.or p q).pair s + 1, by simp[hΔ]⟩,
  Set.mem_iUnion.mpr ⟨(encode $ Code.or p q).pair s + 1, by simp[hΔ]⟩⟩ }
Proof state after:
case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_or
Proof state before:
case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
{ have : p ⋎ q ∈ ⛓️[(encode $ Code.or p q).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
  contradiction }
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_or
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, p ⋎ q ∈ ⛓️[s]
Tactic:
simpa[chainSet] using h
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_or
Proof state before:
case intro.or
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.or p q)).pair s]
hΔ : ⛓️[(encode (Code.or p q)).pair s + 1] = p :: q :: ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
exact ⟨Set.mem_iUnion.mpr ⟨(encode $ Code.or p q).pair s + 1, by simp[hΔ]⟩,
Set.mem_iUnion.mpr ⟨(encode $ Code.or p q).pair s + 1, by simp[hΔ]⟩⟩
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_or
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.or p q)).pair s]
hΔ : ⛓️[(encode (Code.or p q)).pair s + 1] = p :: q :: ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ {x | x ∈ ⛓️[(encode (Code.or p q)).pair s + 1]}
Tactic:
simp[hΔ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_or
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.or p q)).pair s]
hΔ : ⛓️[(encode (Code.or p q)).pair s + 1] = p :: q :: ⛓️[(encode (Code.or p q)).pair s]
⊢ q ∈ {x | x ∈ ⛓️[(encode (Code.or p q)).pair s + 1]}
Tactic:
simp[hΔ]
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_or
Proof state before:
case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
have : p ⋎ q ∈ ⛓️[(encode $ Code.or p q).pair s] := chain_monotone nwf (Nat.right_le_pair _ _) hs
Proof state after:
case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
this : p ⋎ q ∈ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_or
Proof state before:
case intro.orRefl
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.or p q)).pair s + 1] = ⛓️[(encode (Code.or p q)).pair s]
a✝ : p ⋎ q ∉ ⛓️[(encode (Code.or p q)).pair s]
this : p ⋎ q ∈ ⛓️[(encode (Code.or p q)).pair s]
⊢ p ∈ ⛓️ ∧ q ∈ ⛓️
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.chainSet_all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
have : ∃ s, ∀' p ∈ ⛓️[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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
this : ∃ s, ∀' p ∈ ⛓️[s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
this : ∃ s, ∀' p ∈ ⛓️[s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
have : ⛓️[(encode $ Code.all p).pair s + 1] ≺[Code.all p] ⛓️[(encode $ Code.all p).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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.all p)).pair s + 1] ≺[Code.all p] ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
this : ⛓️[(encode (Code.all p)).pair s + 1] ≺[Code.all p] ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
generalize hΔ : ⛓️[(encode $ Code.all p).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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = Δ
this : Δ ≺[Code.all p] ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
Δ : Sequent L
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = Δ
this : Δ ≺[Code.all p] ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
rcases this
Proof state after:
case intro.all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
a✝ : ∀' p ∈ ⛓️[(encode (Code.all p)).pair s]
hΔ :
  ⛓️[(encode (Code.all p)).pair s + 1] =
    [→ &(newVar ⛓️[(encode (Code.all p)).pair s])].hom p :: ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️

case intro.allRefl
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Theorem: LO.FirstOrder.Completeness.chainSet_all
Proof state before:
case intro.all
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
a✝ : ∀' p ∈ ⛓️[(encode (Code.all p)).pair s]
hΔ :
  ⛓️[(encode (Code.all p)).pair s + 1] =
    [→ &(newVar ⛓️[(encode (Code.all p)).pair s])].hom p :: ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️

case intro.allRefl
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️
Tactic:
{ exact ⟨&(newVar ⛓️[(encode $ Code.all p).pair s]), Set.mem_iUnion.mpr ⟨(encode $ Code.all p).pair s + 1, by simp[hΔ]⟩⟩ }
Proof state after:
case intro.allRefl
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 : SyntacticSemiformula L 1
h : ∀' p ∈ ⛓️
s : ℕ
hs : ∀' p ∈ ⛓️[s]
hΔ : ⛓️[(encode (Code.all p)).pair s + 1] = ⛓️[(encode (Code.all p)).pair s]
a✝ : ∀' p ∉ ⛓️[(encode (Code.all p)).pair s]
⊢ ∃ t, [→ t].hom p ∈ ⛓️