internlm/Lean-Github huggingface dataset:
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
⊢ False
Tactic:
have hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory := iff_mem_conj'.mpr hΔ₂
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ False
Tactic:
have : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj') := imp_trans! (andImplyIffImplyImply'!.mp hC)
  $ contra₂'! $ imp_trans! (conj₂'! multidiaDuality!)
  $ imp_trans! iff_conj'multidia_multidiaconj'! $ by
    apply conj'conj'_subset;
    intro q hq;
    obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
    subst_vars;
    simpa;
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
⊢ False
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
⊢ False
Tactic:
have : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj') := by simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this;
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
⊢ False
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
⊢ False
Tactic:
have : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory := iff_mem_neg.mp $ h $ membership_iff.mpr $ (Context.of! this) ⨀ dΓconj
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝¹ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this✝ : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
this : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory
⊢ False
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this✝¹ : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
this✝ : L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
this : (◇'⁻¹^[n]Δ).conj' ∉ Ω₂.theory
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΓ : ∀ p ∈ Γ, p ∈ □''⁻¹Ω₁.theory
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
⊢ ∀ p ∈ Γ, □p ∈ Ω₁.theory
Tactic:
simpa using hΓ
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
⊢ ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
Tactic:
intro p hp
Proof state after:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
p : Formula α
hp : p ∈ ◇'⁻¹^[n]Δ
⊢ p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
p : Formula α
hp : p ∈ ◇'⁻¹^[n]Δ
⊢ p ∈ Ω₂.theory
Tactic:
simpa using hΔ (◇^[n]p) (by simp_all)
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
p : Formula α
hp : p ∈ ◇'⁻¹^[n]Δ
⊢ ◇^[n]p ∈ Δ
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ L ⊢! (◇'^[n]◇'⁻¹^[n]Δ).conj' ⟶ Δ.conj'
Tactic:
apply conj'conj'_subset
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ ∀ p ∈ Δ, p ∈ ◇'^[n]◇'⁻¹^[n]Δ
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
⊢ ∀ p ∈ Δ, p ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
intro q hq
Proof state after:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
obtain ⟨r, _, _⟩ := by simpa using hΔ q hq;
Proof state after:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
r : Formula α
left✝ : r ∈ Ω₂.theory
right✝ : (UnaryModalOperator.mop false)^[n] r = q
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
r : Formula α
left✝ : r ∈ Ω₂.theory
right✝ : (UnaryModalOperator.mop false)^[n] r = q
⊢ q ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
subst_vars
Proof state after:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
r : Formula α
left✝ : r ∈ Ω₂.theory
hq : (UnaryModalOperator.mop false)^[n] r ∈ Δ
⊢ (UnaryModalOperator.mop false)^[n] r ∈ ◇'^[n]◇'⁻¹^[n]Δ
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case h.intro.intro
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
r : Formula α
left✝ : r ∈ Ω₂.theory
hq : (UnaryModalOperator.mop false)^[n] r ∈ Δ
⊢ (UnaryModalOperator.mop false)^[n] r ∈ ◇'^[n]◇'⁻¹^[n]Δ
Tactic:
simpa
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
q : Formula α
hq : q ∈ Δ
⊢ ?m.521811
Tactic:
simpa using hΔ q hq
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Γ Δ : List (Formula α)
hΔ : ∀ p ∈ Δ, p ∈ ◇''^[n]Ω₂.theory
hC : L ⊢! Γ.conj' ⋏ Δ.conj' ⟶ ⊥
hΓ : ∀ p ∈ Γ, □p ∈ Ω₁.theory
dΓconj : Ω₁.theory *⊢[L]! □Γ.conj'
hΔ₂ : ∀ p ∈ ◇'⁻¹^[n]Δ, p ∈ Ω₂.theory
hΔconj : (◇'⁻¹^[n]Δ).conj' ∈ Ω₂.theory
this : L ⊢! Γ.conj' ⟶ □^[n](~(◇'⁻¹^[n]Δ).conj')
⊢ L ⊢! □Γ.conj' ⟶ □^[(n + 1)](~(◇'⁻¹^[n]Δ).conj')
Tactic:
simpa only [UnaryModalOperator.multimop_succ] using imply_box_distribute'! this
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ (fun x x_1 => x ≺ x_1) Ω₁ Ω
Tactic:
intro p hp
Proof state after:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ Ω.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.left
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ Ω.theory
Tactic:
apply hΩ
Proof state after:
case succ.mpr.intro.left.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.left.a
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
p : Formula α
hp : p ∈ □''⁻¹Ω₁.theory
⊢ p ∈ □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory
Tactic:
simp_all
Proof state after:
no goals
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ RelItr (fun x x_1 => x ≺ x_1) n Ω Ω₂
Tactic:
apply ih.mpr
Proof state after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω.theory → p ∈ Ω₂.theory
Theorem: LO.Modal.Standard.Kripke.CanonicalFrame.multiframe_def_multibox
Proof state before:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, □^[n]p ∈ Ω.theory → p ∈ Ω₂.theory
Tactic:
apply multibox_multidia.mpr
Proof state after:
case succ.mpr.intro.right
α : Type u_1
inst✝⁴ : DecidableEq α
inst✝³ : Inhabited α
L : DeductionParameter α
inst✝² : L.Normal
inst✝¹ : Minimal L
inst✝ : Inhabited (MCT L)
n : ℕ
ih : ∀ {Ω₁ Ω₂ : (CanonicalFrame L).World}, Ω₁ ≺^[n] Ω₂ ↔ ∀ {p : Formula α}, □^[n]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω₁ Ω₂ : (CanonicalFrame L).World
h : ∀ {p : Formula α}, □^[(n + 1)]p ∈ Ω₁.theory → p ∈ Ω₂.theory
Ω : MCT L
hΩ : □''⁻¹Ω₁.theory ∪ ◇''^[n]Ω₂.theory ⊆ Ω.theory
⊢ ∀ {p : Formula α}, p ∈ Ω₂.theory → ◇^[n]p ∈ Ω.theory