internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□p) → ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
intro h
Proof state after:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
obtain ⟨z, rwz, hz⟩ := by simpa using h;
Proof state after:
case intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
obtain ⟨xm, ⟨hxm₁, hxm₂⟩⟩ := hWF.has_min ({ x | (F.Rel w x) ∧ ¬(Satisfies ⟨F, V⟩ x p) }) (by existsi z; simp_all)
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ¬Satisfies { Frame := F, Valuation := V } w (□(□p ⟶ p))
Tactic:
simp [Satisfies.box_def]
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ∃ x,
    w ≺ x ∧
      (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
        ¬Satisfies { Frame := F, Valuation := V } x p
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ ∃ x,
    w ≺ x ∧
      (∀ (w' : F.World), x ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
        ¬Satisfies { Frame := F, Valuation := V } x p
Tactic:
existsi xm
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p
Tactic:
have : Satisfies ⟨F, V⟩ xm (□p) := by
  by_contra hC;
  obtain ⟨y, hy₁, hy₂⟩ := by simpa using hC;
  have : ¬(xm ≺ y) := hxm₂ y ⟨(hTrans (by simp_all) hy₁), hy₂⟩;
  contradiction;
Proof state after:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
this : Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro.intro.intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
this : Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ w ≺ xm ∧
    (∀ (w' : F.World), xm ≺ w' → Satisfies { Frame := F, Valuation := V } w' p) ∧
      ¬Satisfies { Frame := F, Valuation := V } xm p
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
⊢ ?m.44125
Tactic:
simpa using h
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}.Nonempty
Tactic:
existsi z
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ z ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
⊢ z ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
⊢ Satisfies { Frame := F, Valuation := V } xm (□p)
Tactic:
by_contra hC
Proof state after:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ False
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ False
Tactic:
obtain ⟨y, hy₁, hy₂⟩ := by simpa using hC;
Proof state after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ False
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ False
Tactic:
have : ¬(xm ≺ y) := hxm₂ y ⟨(hTrans (by simp_all) hy₁), hy₂⟩
Proof state after:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
this : ¬xm ≺ y
⊢ False
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
case intro.intro
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
this : ¬xm ≺ y
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
⊢ ?m.80491
Tactic:
simpa using hC
Proof state after:
no goals
Theorem: LO.Modal.Standard.AxiomSet.L.definability.impliedby
Proof state before:
W α : Type u
inst✝¹ : Inhabited W
inst✝ : Inhabited α
F : Frame' α
hTrans : Transitive F.Rel
hWF : ConverseWellFounded F.Rel
p : Formula α
V : Valuation F.World α
w : { Frame := F, Valuation := V }.World
h : ¬Satisfies { Frame := F, Valuation := V } w (□p)
z : F.World
rwz : w ≺ z
hz : ¬Satisfies { Frame := F, Valuation := V } z p
xm : F.World
hxm₁ : xm ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}
hxm₂ : ∀ x ∈ {x | F.Rel w x ∧ ¬Satisfies { Frame := F, Valuation := V } x p}, ¬flip (fun x x_1 => F.Rel x x_1) x xm
hC : ¬Satisfies { Frame := F, Valuation := V } xm (□p)
y : F.World
hy₁ : xm ≺ y
hy₂ : ¬Satisfies { Frame := F, Valuation := V } y p
⊢ F.Rel w xm
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.Redux.antimonotone
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
c : Code L
Δ₂ Δ₁ : Sequent L
h : Δ₂ ≺[c] Δ₁
⊢ Δ₁ ⊆ Δ₂
Tactic:
cases h <;> simp[List.subset_cons_of_subset _ (List.subset_cons _ _)]
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone
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
s : ℕ
Δ₂ Δ₁ : Sequent L
h : Δ₂ ≺⟨s⟩ Δ₁
⊢ Δ₁ ⊆ Δ₂
Tactic:
cases h
Proof 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
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[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
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone
Proof 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
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[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
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Tactic:
{ exact Redux.antimonotone (by assumption) }
Proof 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
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone
Proof 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
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Tactic:
{ exact List.Subset.refl Δ₂ }
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone
Proof 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
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[c✝] Δ₁
⊢ Δ₁ ⊆ Δ₂
Tactic:
exact Redux.antimonotone (by assumption)
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone
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
s : ℕ
Δ₂ Δ₁ : Sequent L
c✝ : Code L
a✝¹ : decode s.unpair.1 = some c✝
a✝ : Δ₂ ≺[c✝] Δ₁
⊢ Redux ?m.13639 ?m.13640 Δ₂ Δ₁
Tactic:
assumption
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.ReduxNat.antimonotone
Proof 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
s : ℕ
Δ₂ : Sequent L
a✝ : decode s.unpair.1 = none
⊢ Δ₂ ⊆ Δ₂
Tactic:
exact List.Subset.refl Δ₂
Proof state after:
no goals
Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux
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
c : Code L
i : ℕ
Δ₂ Δ₁ : Sequent L
h : Δ₂ ≺⟨(encode c).pair i⟩ Δ₁
⊢ Δ₂ ≺[c] Δ₁
Tactic:
rcases h with (⟨h, r⟩ | ⟨h⟩)
Proof 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] Δ₂
Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux
Proof 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 }
Proof 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] Δ₂
Theorem: LO.FirstOrder.Completeness.ReduxNat.toRedux
Proof 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 }
Proof state after:
no goals