internlm/Lean-Github huggingface dataset:
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
⊢ evaluate (↑MG) X τ
Tactic:
have := loadedTruthLemma MG X τ
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
⊢ evaluate (↑MG) X τ
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ : Formula
τ_in : τ ∈ F (?'a✝) (α_def ▸ ℓ)
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
⊢ evaluate (↑MG) X τ
Tactic:
subst α_def
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
τ : Formula
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑X
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ_in : τ ∈ F (?'a✝) (⋯ ▸ ℓ)
⊢ evaluate (↑MG) X τ
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
τ : Formula
forTermination : lengthOfFormula τ < lengthOfProgram (?'a✝)
this : (τ ∈ ↑X → evaluate (↑MG) X τ) ∧ ((~τ) ∈ ↑X → ¬evaluate (↑MG) X τ)
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑X
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
τ_in : τ ∈ F (?'a✝) (⋯ ▸ ℓ)
⊢ evaluate (↑MG) X τ
Tactic:
simp_all only [instBot, relate, Subtype.exists, lengthOfProgram, true_or, forall_true_left]
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
⊢ (↑MG, X)⊨Con (F (?'a✝) (α_def ▸ ℓ))
Tactic:
simp [modelCanSemImplyForm,conEval]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
⊢ ∀ f ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X f
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
⊢ ∀ f ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X f
Tactic:
exact X_F
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑X
Tactic:
simp_all only [instBot, relate, Subtype.exists]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
ℓ : TP α
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ Y Y
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
ℓ : TP α
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ Y Y
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y
Tactic:
subst_eqs
Proof state after:
case refl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y
Theorem: loadedTruthLemmaProg
Proof state before:
case refl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ ↑Y
Tactic:
apply Xset_sub_X
Proof state after:
case refl.a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
Theorem: loadedTruthLemmaProg
Proof state before:
case refl.a
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ (⌈⌈δ⌉⌉φ) ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
Tactic:
right
Proof state after:
case refl.a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
Theorem: loadedTruthLemmaProg
Proof state before:
case refl.a.h
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
X : { x // x ∈ Worlds }
φ a✝ : Formula
Y : { x // x ∈ Worlds }
δ : List Program
boxP_in_X : (⌈?'a✝⌉φ) ∈ ↑Y
X_rel_Y : X = Y ∧ evaluate (↑MG) X a✝
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑Y → P ∈ ↑Y) ∧
      (P⋀Q ∈ ↑Y → P ∈ ↑Y ∧ Q ∈ ↑Y) ∧
        ((~P⋀Q) ∈ ↑Y → (~P) ∈ ↑Y ∨ (~Q) ∈ ↑Y) ∧
          ((⌈α⌉P) ∈ ↑Y → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑Y) ∧
            ((~⌈α⌉P) ∈ ↑Y → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑Y)
X_δ_Y : relateSeq (↑MG) δ Y Y
ℓ : TP (?'a✝)
Xset_sub_X : ∀ (x : Formula), (x ∈ F (?'a✝) ℓ ∨ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑Y
X_F : ∀ τ ∈ F (?'a✝) (⋯ ▸ ℓ), evaluate (↑MG) Y τ
δ_in_P : δ ∈ P (?'a✝) (⋯ ▸ ℓ)
⊢ ∃ a ∈ P (?'a✝) ℓ, (⌈⌈a⌉⌉φ) = ⌈⌈δ⌉⌉φ
Tactic:
use δ
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
⊢ ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
Tactic:
intro d d_in_δ X' Y' φ' dφ_in_X' X'_d_Y'
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ φ' ∈ ↑Y'
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ φ' ∈ ↑Y'
Tactic:
have forTermination : lengthOf d < lengthOf α := by
  have := P_goes_down d_in_δ δ_in_P
  simp_all [isAtomic, isStar]
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
forTermination : lengthOf d < lengthOf α
⊢ φ' ∈ ↑Y'
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
forTermination : lengthOf d < lengthOf α
⊢ φ' ∈ ↑Y'
Tactic:
exact loadedTruthLemmaProg MG d X' φ' dφ_in_X' Y' X'_d_Y'
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
⊢ lengthOf d < lengthOf α
Tactic:
have := P_goes_down d_in_δ δ_in_P
Proof state after:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this :
  if isAtomic (?'a✝) = true then d = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram d ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram d < lengthOfProgram (?'a✝)
⊢ lengthOf d < lengthOf α
Theorem: loadedTruthLemmaProg
Proof state before:
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
d : Program
d_in_δ : d ∈ δ
X' Y' : { x // x ∈ Worlds }
φ' : Formula
dφ_in_X' : (⌈d⌉φ') ∈ ↑X'
X'_d_Y' : relate (↑MG) d X' Y'
this :
  if isAtomic (?'a✝) = true then d = (?'a✝)
  else
    if isStar (?'a✝) = true then lengthOfProgram d ≤ lengthOfProgram (?'a✝)
    else lengthOfProgram d < lengthOfProgram (?'a✝)
⊢ lengthOf d < lengthOf α
Tactic:
simp_all [isAtomic, isStar]
Proof state after:
no goals
Theorem: loadedTruthLemmaProg
Proof state before:
case test.intro.intro.intro.inl
Worlds : Finset (Finset Formula)
MG : ModelGraph Worlds
α : Program
X : { x // x ∈ Worlds }
φ : Formula
boxP_in_X : (⌈α⌉φ) ∈ ↑X
a✝ : Formula
α_def : α = (?'a✝)
Y : { x // x ∈ Worlds }
X_rel_Y : relate (↑MG) (?'a✝) X Y
satX :
  ∀ (P Q : Formula) (α : Program),
    ((~~P) ∈ ↑X → P ∈ ↑X) ∧
      (P⋀Q ∈ ↑X → P ∈ ↑X ∧ Q ∈ ↑X) ∧
        ((~P⋀Q) ∈ ↑X → (~P) ∈ ↑X ∨ (~Q) ∈ ↑X) ∧
          ((⌈α⌉P) ∈ ↑X → ∃ l, ∀ x ∈ Xset α l P, x ∈ ↑X) ∧
            ((~⌈α⌉P) ∈ ↑X → ∃ a b, (a, b) ∈ H α ∧ ∀ x ∈ Yset (a, b) P, x ∈ ↑X)
ℓ : TP α
Xset_sub_X : ∀ (x : Formula), (x ∈ F α ℓ ∨ ∃ a ∈ P α ℓ, (⌈⌈a⌉⌉φ) = x) → x ∈ ↑X
X_F : ∀ τ ∈ F (?'a✝) (α_def ▸ ℓ), evaluate (↑MG) X τ
δ : List Program
δ_in_P : δ ∈ P (?'a✝) (α_def ▸ ℓ)
X_δ_Y : relateSeq (↑MG) δ X Y
δφ_in_X : (⌈⌈δ⌉⌉φ) ∈ ↑X
IHδ : ∀ d ∈ δ, ∀ (X' Y' : { x // x ∈ Worlds }) (φ' : Formula), (⌈d⌉φ') ∈ ↑X' → relate (↑MG) d X' Y' → φ' ∈ ↑Y'
h✝ : δ = []
⊢ φ ∈ ↑Y
Tactic:
simp_all [relateSeq]
Proof state after:
no goals