internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
specialize andSplit QandR_in_X
Proof state after:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
andSplit : Q ∈ ↑X ∧ R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
andSplit : Q ∈ ↑X ∧ R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
cases' andSplit with Q_in_X R_in_X
Proof state after:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
simp only [evaluate]
Proof state after:
case intro.intro.intro.intro.intro.left.intro
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X Q ∧ evaluate M X R
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.left.intro.left
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X Q
Tactic:
exact plus_Q Q_in_X
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.left.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
QandR_in_X : Q⋀R ∈ ↑X
Q_in_X : Q ∈ ↑X
R_in_X : R ∈ ↑X
⊢ evaluate M X R
Tactic:
exact plus_R R_in_X
Proof state after:
no goals
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
⊢ (~Q⋀R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
intro notQandR_in_X
Proof state after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X (Q⋀R)
Tactic:
unfold evaluate
Proof state after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬(evaluate (↑⟨M, ⋯⟩) X Q ∧ evaluate (↑⟨M, ⋯⟩) X R)
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬(evaluate (↑⟨M, ⋯⟩) X Q ∧ evaluate (↑⟨M, ⋯⟩) X R)
Tactic:
rw [not_and_or]
Proof state after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
notAndSplit : (~Q⋀R) ∈ ↑X → (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
specialize notAndSplit notQandR_in_X
Proof state after:
case intro.intro.intro.intro.intro.right
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notAndSplit : (~Q) ∈ ↑X ∨ (~R) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right.inl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q ∨ ¬evaluate (↑⟨M, ⋯⟩) X R
Tactic:
left
Proof state after:
case intro.intro.intro.intro.intro.right.inl.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q
Theorem: loadedTruthLemma
Proof state before:
case intro.intro.intro.intro.intro.right.inl.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
Q R : Formula
M : KripkeModel { x // x ∈ Worlds }
i : ∀ (X : { x // x ∈ Worlds }), saturated ↑X ∧ ⊥ ∉ ↑X ∧ ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝² : ∀ (X : { x // x ∈ Worlds }) (p : ℕ), (·p) ∈ ↑X ↔ M.val X p
iii : (fun M => ∀ (X Y : { x // x ∈ Worlds }) (a : ℕ) (P : Formula), M.Rel a X Y → (⌈·a⌉P) ∈ ↑X → P ∈ ↑Y) M
right✝² : ∀ (X : { x // x ∈ Worlds }) (α : Program) (P : Formula), (~⌈α⌉P) ∈ ↑X → ∃ Y, _root_.Q M.Rel α X Y ∧ (~P) ∈ ↑Y
plus_Q : Q ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X Q
minus_Q : (~Q) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X Q
plus_R : R ∈ ↑X → evaluate (↑⟨M, ⋯⟩) X R
minus_R : (~R) ∈ ↑X → ¬evaluate (↑⟨M, ⋯⟩) X R
X_saturated : saturated ↑X
left✝¹ : ⊥ ∉ ↑X
right✝¹ : ∀ (pp : ℕ), (·pp) ∈ ↑X → (~·pp) ∉ ↑X
left✝ : (~~Q) ∈ ↑X → Q ∈ ↑X
andSplit : Q⋀R ∈ ↑X → Q ∈ ↑X ∧ R ∈ ↑X
right✝ :
  ((⌈?'Q⌉Q) ∈ ↑X → ∃ l, ((Xset (?'Q) l Q).all fun y => decide (y ∈ ↑X)) = true) ∧
    ((~⌈?'Q⌉Q) ∈ ↑X → ∃ Fδ ∈ H (?'Q), ((Yset Fδ Q).all fun y => decide (y ∈ ↑X)) = true)
notQandR_in_X : (~Q⋀R) ∈ ↑X
notQ_in_X : (~Q) ∈ ↑X
⊢ ¬evaluate (↑⟨M, ⋯⟩) X Q
Tactic:
exact minus_Q notQ_in_X
Proof state after:
no goals