Theorem: combMo_preserves_truth_at_oldWOrld (Pdl/Soundness.lean)

State before:
case right.right.intro.intro.inl
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : 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 ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
val✝ : Unit
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inl val✝) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
Tactic:
rcases IH_a with ⟨IH_rel, sameR, noNewL⟩
State after:
case right.right.intro.intro.inl.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
val✝ : Unit
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inl 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 ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)

State before:
case right.right.intro.intro.inl.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : Program
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
val✝ : Unit
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inl 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 ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
Tactic:
apply noNewL
State after:
no goals

State before:
case right.right.intro.intro.inr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : 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 ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
val✝ : (k : β) × (collection k).fst
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
⊢ False
Tactic:
absurd b_rel_u_to
State after:
case right.right.intro.intro.inr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : 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 ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
val✝ : (k : β) × (collection k).fst
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())

State before:
case right.right.intro.intro.inr
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : 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 ())
IH_b :
  (∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
      relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
        relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂) ∧
    (∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
        R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)) ∧
      ∀ (R : β) (oldWorld : (collection R).fst),
        ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
R : β
oldWorld : (collection R).fst
val✝ : (k : β) × (collection k).fst
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
Tactic:
rcases IH_b with ⟨IH_rel, sameR, noNewL⟩
State after:
case right.right.intro.intro.inr.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : 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
val✝ : (k : β) × (collection k).fst
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂
sameR :
  ∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
    R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())

State before:
case right.right.intro.intro.inr.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a b : 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
val✝ : (k : β) × (collection k).fst
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inr val✝)
b_rel_u_to : relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
IH_rel :
  ∀ (R : β) (oldWorld₁ oldWorld₂ : (collection R).fst),
    relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
      relate (collection R).snd.2.1 b oldWorld₁ oldWorld₂
sameR :
  ∀ (R₁ R₂ : β) (oldWorld₁ : (collection R₁).fst) (oldWorld₂ : (collection R₂).fst),
    R₁ ≠ R₂ → ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 b (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 b (Sum.inr val✝) (Sum.inl ())
Tactic:
apply noNewL
State after:
no goals

State before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a a_1 : Program),
    (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 →
      (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_1 →
        (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⋓a_1)
Tactic:
aesop
State after:
no goals

State before:
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
⊢ ∀ (a : Program),
    (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 →
      (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:
intro a IH_a
State after:
β : 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₁ 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 ())

State before:
β : 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₁ 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 ())
Tactic:
constructor
State after:
case left
β : 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₁ 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₂

case right
β : 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₁ 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 ())

State before:
case right
β : 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₁ 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 ())
Tactic:
constructor
State after:
case right.left
β : 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₁ 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₂⟩)

case right.right
β : 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),
    ¬relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())

State before:
case left
β : 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₁ 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₂
Tactic:
intro R oldWorld₁ oldWorld₂
State after:
case left
β : 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₁ 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₂

State before:
case left
β : 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₁ 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₂
Tactic:
have star_preserved : ∀ (w v : (collection R).fst),
  Relation.ReflTransGen (relate (combinedModel collection newVal).fst a)
    (Sum.inr ⟨R, w⟩) (Sum.inr ⟨R, v⟩) ↔ Relation.ReflTransGen (relate (collection R).snd.snd.fst a) w v :=
  by
  intro w v
  rw [ReflTransGen.iff_finitelyManySteps]
  rw [ReflTransGen.iff_finitelyManySteps]
  sorry
State after:
case left
β : 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₁ oldWorld₂ : (collection R).fst
star_preserved :
  ∀ (w v : (collection R).fst),
    Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, w⟩) (Sum.inr ⟨R, v⟩) ↔
      Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v
⊢ relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
    relate (collection R).snd.2.1 (∗a) oldWorld₁ oldWorld₂

State before:
case left
β : 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₁ oldWorld₂ : (collection R).fst
star_preserved :
  ∀ (w v : (collection R).fst),
    Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, w⟩) (Sum.inr ⟨R, v⟩) ↔
      Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v
⊢ relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R, oldWorld₁⟩) (Sum.inr ⟨R, oldWorld₂⟩) ↔
    relate (collection R).snd.2.1 (∗a) oldWorld₁ oldWorld₂
Tactic:
constructor <;> aesop
State after:
no goals

State before:
β : 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₁ oldWorld₂ : (collection R).fst
⊢ ∀ (w v : (collection R).fst),
    Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, w⟩) (Sum.inr ⟨R, v⟩) ↔
      Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v
Tactic:
intro w v
State after:
β : 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₁ oldWorld₂ w v : (collection R).fst
⊢ Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, w⟩) (Sum.inr ⟨R, v⟩) ↔
    Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v

State before:
β : 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₁ oldWorld₂ w v : (collection R).fst
⊢ Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, w⟩) (Sum.inr ⟨R, v⟩) ↔
    Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v
Tactic:
rw [ReflTransGen.iff_finitelyManySteps]
State after:
β : 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₁ oldWorld₂ w v : (collection R).fst
⊢ (∃ n ys,
      Sum.inr ⟨R, w⟩ = ys.head ∧
        Sum.inr ⟨R, v⟩ = ys.last ∧
          ∀ (i : Fin n), relate (combinedModel collection newVal).1 a (ys.get i.castSucc) (ys.get i.succ)) ↔
    Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v

State before:
β : 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₁ oldWorld₂ w v : (collection R).fst
⊢ (∃ n ys,
      Sum.inr ⟨R, w⟩ = ys.head ∧
        Sum.inr ⟨R, v⟩ = ys.last ∧
          ∀ (i : Fin n), relate (combinedModel collection newVal).1 a (ys.get i.castSucc) (ys.get i.succ)) ↔
    Relation.ReflTransGen (relate (collection R).snd.2.1 a) w v
Tactic:
rw [ReflTransGen.iff_finitelyManySteps]
State after:
β : 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₁ oldWorld₂ w v : (collection R).fst
⊢ (∃ n ys,
      Sum.inr ⟨R, w⟩ = ys.head ∧
        Sum.inr ⟨R, v⟩ = ys.last ∧
          ∀ (i : Fin n), relate (combinedModel collection newVal).1 a (ys.get i.castSucc) (ys.get i.succ)) ↔
    ∃ n ys,
      w = ys.head ∧ v = ys.last ∧ ∀ (i : Fin n), relate (collection R).snd.2.1 a (ys.get i.castSucc) (ys.get i.succ)

State before:
β : 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₁ oldWorld₂ w v : (collection R).fst
⊢ (∃ n ys,
      Sum.inr ⟨R, w⟩ = ys.head ∧
        Sum.inr ⟨R, v⟩ = ys.last ∧
          ∀ (i : Fin n), relate (combinedModel collection newVal).1 a (ys.get i.castSucc) (ys.get i.succ)) ↔
    ∃ n ys,
      w = ys.head ∧ v = ys.last ∧ ∀ (i : Fin n), relate (collection R).snd.2.1 a (ys.get i.castSucc) (ys.get i.succ)
Tactic:
sorry
State after:
no goals

State before:
case right.left
β : 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₁ 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₂⟩)
Tactic:
intro R₁ R₂ oldWorld₁ oldWorld₂ hneq
State after:
case right.left
β : 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₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
⊢ ¬relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)

State before:
case right.left
β : 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₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
⊢ ¬relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
Tactic:
unfold relate
State after:
case right.left
β : 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₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R₁, oldWorld₁⟩)
      (Sum.inr ⟨R₂, oldWorld₂⟩)

State before:
case right.left
β : 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₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R₁, oldWorld₁⟩)
      (Sum.inr ⟨R₂, oldWorld₂⟩)
Tactic:
rcases IH_a with ⟨IH_rel, sameR, noNewL⟩
State after:
case right.left.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
R₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
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 ⟨R₁, oldWorld₁⟩)
      (Sum.inr ⟨R₂, oldWorld₂⟩)

State before:
case right.left.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
R₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
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 ⟨R₁, oldWorld₁⟩)
      (Sum.inr ⟨R₂, oldWorld₂⟩)
Tactic:
specialize sameR R₁ R₂ oldWorld₁ oldWorld₂ hneq
State after:
case right.left.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
R₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
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₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
sameR : ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R₁, oldWorld₁⟩)
      (Sum.inr ⟨R₂, oldWorld₂⟩)

State before:
case right.left.intro.intro
β : Type
collection : β → (W : Type) × ℕ × KripkeModel W × W
newVal : ℕ → Prop
mF : Formula
mR : β
moW : (collection mR).fst
a : Program
R₁ R₂ : β
oldWorld₁ : (collection R₁).fst
oldWorld₂ : (collection R₂).fst
hneq : R₁ ≠ R₂
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₂
noNewL :
  ∀ (R : β) (oldWorld : (collection R).fst),
    ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
sameR : ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R₁, oldWorld₁⟩) (Sum.inr ⟨R₂, oldWorld₂⟩)
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R₁, oldWorld₁⟩)
      (Sum.inr ⟨R₂, oldWorld₂⟩)
Tactic:
sorry
State after:
no goals

State before:
case right.right
β : 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),
    ¬relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
Tactic:
intro R oldWorld
State after:
case right.right
β : 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
⊢ ¬relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())

State before:
case right.right
β : 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
⊢ ¬relate (combinedModel collection newVal).1 (∗a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
Tactic:
unfold relate
State after:
case right.right
β : 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
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())

State before:
case right.right
β : 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
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr ⟨R, oldWorld⟩) (Sum.inl ())
Tactic:
intro star_rel
State after:
case right.right
β : 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 ())
⊢ False

State before:
case right.right
β : 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 ())
⊢ False
Tactic:
cases ReflTransGen.cases_tail_eq_neq star_rel
State after:
case right.right.inl
β : 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 ())
h✝ : Sum.inr ⟨R, oldWorld⟩ = Sum.inl ()
⊢ False

case right.right.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 ())
h✝ :
  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 ())
⊢ False

State before:
β : 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 ()
⊢ False
Tactic:
case inl hyp => simp at hyp
State after:
no goals

State before:
β : 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 ()
⊢ False
Tactic:
simp at hyp
State after:
no goals

State before:
β : 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 ())
⊢ False
Tactic:
rcases hyp.2 with ⟨u, _neq_u, a_rel_to_u, b_rel_u_to⟩
State after:
case intro.intro.intro
β : 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 ())
u : Unit ⊕ (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ u
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) u
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) u (Sum.inl ())
⊢ False

State before:
case intro.intro.intro
β : 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 ())
u : Unit ⊕ (k : β) × (collection k).fst
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ u
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) u
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) u (Sum.inl ())
⊢ False
Tactic:
cases u
State after:
case intro.intro.intro.inl
β : 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✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl val✝) (Sum.inl ())
⊢ False

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

State before:
case intro.intro.intro.inl
β : 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✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl val✝) (Sum.inl ())
⊢ False
Tactic:
absurd a_rel_to_u
State after:
case intro.intro.intro.inl
β : 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✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl val✝) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)

State before:
case intro.intro.intro.inl
β : 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✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl val✝) (Sum.inl ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
Tactic:
rcases IH_a with ⟨IH_rel, sameR, noNewL⟩
State after:
case intro.intro.intro.inl.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✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl 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 ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)

State before:
case intro.intro.intro.inl.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✝ : Unit
_neq_u : Sum.inr ⟨R, oldWorld⟩ ≠ Sum.inl val✝
a_rel_to_u : relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
b_rel_u_to : Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inl 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 ())
⊢ ¬relate (combinedModel collection newVal).1 a (Sum.inr ⟨R, oldWorld⟩) (Sum.inl val✝)
Tactic:
apply noNewL
State after:
no goals

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
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 ())

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 ())
⊢ ¬Relation.ReflTransGen (relate (combinedModel collection newVal).1 a) (Sum.inr val✝) (Sum.inl ())
Tactic:
rcases IH_a with ⟨IH_rel, sameR, noNewL⟩
State after:
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 ())

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
State after:
no goals

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
State after:
no goals