internlm/Lean-Github huggingface dataset:
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case intro.intro.intro.inr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
star_rel : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
hyp :
  Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl () ∧
    ∃ y,
      Sum.inr ⟨R, oldWorld⟩ ≠ y ∧
        relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) y ∧
          Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) y (Sum.inl ())
val✝ : (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inr val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
⊢ False
Tactic:
absurd b_rel_u_to
Proof state after:
case intro.intro.intro.inr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
IH_a :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
star_rel : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
hyp :
  Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl () ∧
    ∃ y,
      Sum.inr ⟨R, oldWorld⟩ ≠ y ∧
        relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) y ∧
          Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) y (Sum.inl ())
val✝ : (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inr val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
case intro.intro.intro.inr.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
R : β
oldWorld : (collection R).fst
star_rel : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
hyp :
  Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl () ∧
    ∃ y,
      Sum.inr ⟨R, oldWorld⟩ ≠ y ∧
        relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) y ∧
          Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) y (Sum.inl ())
val✝ : (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inr val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 a oldWorld₁ oldWorld₂
sameR :
  ∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
    R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
Tactic:
sorry
Proof state after:
no goals
Theorem: combMo_preserves_truth_at_oldWOrld
Proof state before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a : Formula),
    (fun φ =>
          ∀ (R : β) (oldWorld : (collection R).fst),
            evaluate (combinedModel collection newVal).1 (Sum.inr ⟨R, oldWorld⟩) φ ↔
              evaluate (collection R).snd.2.1 oldWorld φ)
        a →
      (fun π =>
          (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
              relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
                relate (collection R).snd.2.1 π oldWorld₁ oldWorld₂) ∧
            (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
                R₁ ≠ R₂ →
                  ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
              ∀ (R : β) (oldWorld : (collection R).fst),
                ¬relate (combinedModel collection newVal).1 π (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ()))
        (?'a)
Tactic:
aesop
Proof state after:
no goals
Theorem: endNodeIsEndNodeOfChild
Proof state before:
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)
Tactic:
have := endNode_to_endNodeOfChildNonComp lrA E_in
Proof state after:
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)
Theorem: endNodeIsEndNodeOfChild
Proof state before:
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ Y, ∃ (h : Y ∈ a✝), E ∈ endNodesOf (subTabs Y h)
Tactic:
use this
Proof state after:
case h
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ (h : ↑this ∈ a✝), E ∈ endNodesOf (subTabs (↑this) h)
Theorem: endNodeIsEndNodeOfChild
Proof state before:
case h
E X : TNode
a✝ : List TNode
subTabs : (Y : TNode) → Y ∈ a✝ → LocalTableau Y
lrA : LocalRuleApp X a✝
E_in : E ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
this : { x // ∃ (h : x ∈ a✝), E ∈ endNodesOf (subTabs x h) }
⊢ ∃ (h : ↑this ∈ a✝), E ∈ endNodesOf (subTabs (↑this) h)
Tactic:
aesop
Proof state after:
no goals
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
⊢ Z ∈ endNodesOf ltX
Tactic:
cases h' : subTabs Y Y_in
Proof state after:
case byLocalRule
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
B✝ : List TNode
next✝ : (Y : TNode) → Y ∈ B✝ → LocalTableau Y
x✝ : LocalRuleApp Y B✝
h' : subTabs Y Y_in = LocalTableau.byLocalRule x✝ next✝
⊢ Z ∈ endNodesOf ltX

case sim
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
a✝ : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim a✝
⊢ Z ∈ endNodesOf ltX
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf ltX
Tactic:
subst h
Proof state after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Tactic:
simp
Proof state after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l
Tactic:
use endNodesOf (subTabs Y Y_in)
Proof state after:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
constructor
Proof state after:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)

case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (subTabs Y Y_in)
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)
Tactic:
use Y, Y_in
Proof state after:
no goals
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
Y_isSimp : isBasic Y = true
h' : subTabs Y Y_in = LocalTableau.sim Y_isSimp
⊢ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
exact Z_in
Proof state after:
no goals
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
ltX : LocalTableau X
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
h : ltX = LocalTableau.byLocalRule lrA subTabs
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf ltX
Tactic:
subst h
Proof state after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
Z_in : Z ∈ endNodesOf (subTabs Y Y_in)
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Tactic:
rw [h'] at Z_in
Proof state after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA subTabs)
Tactic:
simp
Proof state after:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l
Theorem: endNodeOfChild_to_endNode
Proof state before:
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ l, (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = l) ∧ Z ∈ l
Tactic:
use endNodesOf (subTabs Y Y_in)
Proof state after:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ (∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)) ∧ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
constructor
Proof state after:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)

case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (subTabs Y Y_in)
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h.left
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ ∃ a, ∃ (h : a ∈ C), endNodesOf (subTabs a ⋯) = endNodesOf (subTabs Y Y_in)
Tactic:
use Y, Y_in
Proof state after:
no goals
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (subTabs Y Y_in)
Tactic:
rw [h']
Proof state after:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
Theorem: endNodeOfChild_to_endNode
Proof state before:
case h.right
X Y : TNode
C : List TNode
lrA : LocalRuleApp X C
subTabs : (Y : TNode) → Y ∈ C → LocalTableau Y
Y_in : Y ∈ C
Z : TNode
C' : List TNode
subTabs' : (Y : TNode) → Y ∈ C' → LocalTableau Y
lrA' : LocalRuleApp Y C'
Z_in : Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
h' : subTabs Y Y_in = LocalTableau.byLocalRule lrA' subTabs'
⊢ Z ∈ endNodesOf (LocalTableau.byLocalRule lrA' subTabs')
Tactic:
exact Z_in
Proof state after:
no goals
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
h : some tabΔ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
M : KripkeModel W
v : W
φ : AnyFormula
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) Δ
v_X : (M, v)⊨Δ
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
let ⟨L,R,O⟩ := Δ
Proof state after:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
h : some tabΔ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
h : some tabΔ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
let ⟨ΔNode, ΔHist, ΔTab⟩ := tabΔ
Proof state after:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔNode : TNode
ΔHist : LoadHistory
ΔTab : ClosedTableau ΔHist ΔNode
h : some ⟨ΔNode, ⟨ΔHist, ΔTab⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Theorem: loadedDiamondPaths
Proof state before:
tabΔ : (Y : TNode) × (HistY : LoadHistory) × ClosedTableau HistY Y
W : Type
α : Program
w : W
Root Δ : TNode
tab : ClosedTableau ([], []) Root
path_to_Δ : List TNode
M : KripkeModel W
v : W
φ : AnyFormula
v_α_w : relate M α v w
w_φ : (M, w)⊨~''φ
L R : List Formula
O : Option (NegLoadFormula ⊕ NegLoadFormula)
negLoad_in : NegLoadFormula_in_TNode (~'⌊α⌋φ) (L, R, O)
v_X : (M, v)⊨(L, R, O)
ΔHist : LoadHistory
α✝ : Program
φ✝ : Formula
L✝ R✝ : List Formula
a✝¹ : (~⌈α✝⌉φ✝) ∈ L✝
a✝ : ClosedTableau ([], []) (L✝.erase (~⌈α✝⌉φ✝), R✝, some (Sum.inl (toNegLoad α✝ φ✝)))
h : some ⟨(L✝, R✝, none), ⟨ΔHist, ClosedTableau.mrkL a✝¹ a✝⟩⟩ = tabInAt ⟨Root, ⟨([], []), tab⟩⟩ path_to_Δ
⊢ ∃ path_Δ_to_Γ,
    ∃ Γ ∈ tabInAt ⟨Root, ⟨([], []), tab⟩⟩ (path_to_Δ ++ path_Δ_to_Γ), AnyNegFormula_in_TNode (~''φ) Γ.fst ∧ (M, w)⊨Γ.fst
Tactic:
case mrkL =>
  simp at negLoad_in
  cases negLoad_in
  case inl hyp => subst hyp; sorry
  all_goals sorry
Proof state after:
no goals