Theorem: LO.FirstOrder.Completeness.semanticMainLemma_val (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 Γ)
h : ⊤ ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) ⊤
Tactic:
by_contra
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 Γ)
h : ⊤ ∈ ⛓️
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) ⊤
⊢ 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 Γ)
h : ⊤ ∈ ⛓️
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) ⊤
⊢ False
Tactic:
exact chainSet_verum nwf 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 Γ)
x✝ : ⊥ ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) ⊥
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
rcases chainSet_axL nwf r v with (hr | hr)
State after:
case inl
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : rel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)

case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)

State before:
case inl
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : rel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)

case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
{ contradiction }
State after:
case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)

State before:
case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
{ simpa[eval_rel] using hr }
State after:
no goals

State before:
case inl
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : rel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
contradiction
State after:
no goals

State before:
case inr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : rel r v ∈ ⛓️
hr : nrel r v ∉ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (rel r v)
Tactic:
simpa[eval_rel] using hr
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 Γ)
arity✝ : ℕ
r : L.Rel arity✝
v : Fin arity✝ → Semiterm L ℕ 0
h : nrel r v ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (nrel r v)
Tactic:
simpa[eval_nrel] 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋏ q)
Tactic:
simp
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 ∈ ⛓️
⊢ (Evalf (Model.structure T Γ) Semiterm.fvar) p → ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q

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 ∈ ⛓️
⊢ (Evalf (Model.structure T Γ) Semiterm.fvar) p → ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
Tactic:
intro _ _
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Tactic:
have : p ∈ ⛓️ ∨ q ∈ ⛓️ := chainSet_and nwf 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
this : p ∈ ⛓️ ∨ q ∈ ⛓️
⊢ 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 Γ)
p q : SyntacticFormula L
h : p ⋏ q ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
this : p ∈ ⛓️ ∨ q ∈ ⛓️
⊢ False
Tactic:
rcases this with (h | h)
State after:
case inl
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
⊢ False

case inr
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
⊢ False

State before:
case inl
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
⊢ False
Tactic:
have : ¬Evalf (Model.structure T Γ) Semiterm.fvar p := semanticMainLemma_val p h
State after:
case inl
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False

State before:
case inl
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : p ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
case inr
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
⊢ False
Tactic:
have : ¬Evalf (Model.structure T Γ) Semiterm.fvar q := semanticMainLemma_val q h
State after:
case inr
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False

State before:
case inr
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 ∈ ⛓️
a✝¹ : (Evalf (Model.structure T Γ) Semiterm.fvar) p
a✝ : (Evalf (Model.structure T Γ) Semiterm.fvar) q
h : q ∈ ⛓️
this : ¬(Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ 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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)
Tactic:
have hpq : p ∈ ⛓️ ∧ q ∈ ⛓️ := chainSet_or nwf 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 Γ)
p q : SyntacticFormula L
h : p ⋎ q ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)

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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (p ⋎ q)
Tactic:
simp only [LogicalConnective.HomClass.map_or, LogicalConnective.Prop.or_eq]
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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬((Evalf (Model.structure T Γ) Semiterm.fvar) p ∨ (Evalf (Model.structure T Γ) Semiterm.fvar) q)

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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
⊢ ¬((Evalf (Model.structure T Γ) Semiterm.fvar) p ∨ (Evalf (Model.structure T Γ) Semiterm.fvar) q)
Tactic:
rintro (h | h)
State after:
case inl
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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False

case inr
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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False

State before:
case inl
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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) p
⊢ False
Tactic:
exact semanticMainLemma_val p hpq.1 h
State after:
no goals

State before:
case inr
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 ∈ ⛓️
hpq : p ∈ ⛓️ ∧ q ∈ ⛓️
h : (Evalf (Model.structure T Γ) Semiterm.fvar) q
⊢ False
Tactic:
exact semanticMainLemma_val q hpq.2 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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
have : ∃ u, [→ u].hom p ∈ ⛓️ := chainSet_all nwf 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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
this : ∃ u, [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)

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 (0 + 1)
h : ∀' p ∈ ⛓️
this : ∃ u, [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
rcases this with ⟨u, hu⟩
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 (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)

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 (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
have : ¬Eval (Model.structure T Γ) ![u] Semiterm.fvar p := by
  simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) hu
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 (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)

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 (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∀' p)
Tactic:
simp
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 (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ∃ x, ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p

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 (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ∃ x, ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p
Tactic:
exact ⟨u, this⟩
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∀' p ∈ ⛓️
u : Semiterm L ℕ 0
hu : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) hu
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ¬(Evalf (Model.structure T Γ) Semiterm.fvar) (∃' p)
Tactic:
simp
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 (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ∀ (x : Model T Γ), ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p

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 (0 + 1)
h : ∃' p ∈ ⛓️
⊢ ∀ (x : Model T Γ), ¬(Eval (Model.structure T Γ) ![x] Semiterm.fvar) p
Tactic:
intro u
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 (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p

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 (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
have : [→ u].hom p ∈ ⛓️ := chainSet_ex nwf h u
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 (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p

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 (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
have : ¬Eval (Model.structure T Γ) ![u] Semiterm.fvar p := by
  simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) 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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this✝ : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p

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 (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this✝ : [→ u].hom p ∈ ⛓️
this : ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
assumption
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 Γ)
p : SyntacticSemiformula L (0 + 1)
h : ∃' p ∈ ⛓️
u : Model T Γ
this : [→ u].hom p ∈ ⛓️
⊢ ¬(Eval (Model.structure T Γ) ![u] Semiterm.fvar) p
Tactic:
simpa[eval_substs, Matrix.constant_eq_singleton] using semanticMainLemma_val ([→ u].hom p) this
State after:
no goals