Theorem: LN.HoldsShift (FOL/LN/Paper.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ (∀ (d : D), Holds D I (shift D V d) F) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ ∀ (a : D), Holds D I (shift D V a) F ↔ Holds D I (Function.updateITE V (free_ z) a ∘ Var.openList 0 [free_ z]) F

State before:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
⊢ ∀ (a : D), Holds D I (shift D V a) F ↔ Holds D I (Function.updateITE V (free_ z) a ∘ Var.openList 0 [free_ z]) F
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ Holds D I (shift D V d) F ↔ Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F

State before:
case h
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ Holds D I (shift D V d) F ↔ Holds D I (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) F
Tactic:
apply HoldsCoincideVar
State after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ ∀ (v : Var), occursFreeIn v F → shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v

State before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
⊢ ∀ (v : Var), occursFreeIn v F → shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v
Tactic:
intro v a1
State after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v

State before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = (Function.updateITE V (free_ z) d ∘ Var.openList 0 [free_ z]) v
Tactic:
simp
State after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = Function.updateITE V (free_ z) d (Var.openList 0 [free_ z] v)

State before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = Function.updateITE V (free_ z) d (Var.openList 0 [free_ z] v)
Tactic:
simp only [Function.updateITE]
State after:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = if Var.openList 0 [free_ z] v = free_ z then d else V (Var.openList 0 [free_ z] v)

State before:
case h.h1
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
v : Var
a1 : occursFreeIn v F
⊢ shift D V d v = if Var.openList 0 [free_ z] v = free_ z then d else V (Var.openList 0 [free_ z] v)
Tactic:
cases v
State after:
case h.h1.free_
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a✝ : String
a1 : occursFreeIn (free_ a✝) F
⊢ shift D V d (free_ a✝) =
    if Var.openList 0 [free_ z] (free_ a✝) = free_ z then d else V (Var.openList 0 [free_ z] (free_ a✝))

case h.h1.bound_
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a✝ : ℕ
a1 : occursFreeIn (bound_ a✝) F
⊢ shift D V d (bound_ a✝) =
    if Var.openList 0 [free_ z] (bound_ a✝) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ a✝))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ shift D V d (free_ x') =
    if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Tactic:
case _ x' =>
  simp only [shift]
  simp only [Var.openList]
  split_ifs
  case _ c1 =>
    simp at c1
    simp only [← c1] at h1
    contradiction
  case _ c1 =>
    rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) F
⊢ shift D V d (bound_ i) =
    if Var.openList 0 [free_ z] (bound_ i) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ i))
Tactic:
case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  case succ i =>
    simp only [shift]
    simp only [Var.openList]
    simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ shift D V d (free_ x') =
    if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Tactic:
simp only [shift]
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if Var.openList 0 [free_ z] (free_ x') = free_ z then d else V (Var.openList 0 [free_ z] (free_ x'))
Tactic:
simp only [Var.openList]
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if free_ x' = free_ z then d else V (free_ x')

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
⊢ V (free_ x') = if free_ x' = free_ z then d else V (free_ x')
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
h✝ : free_ x' = free_ z
⊢ V (free_ x') = d

case neg
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
h✝ : ¬free_ x' = free_ z
⊢ V (free_ x') = V (free_ x')

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : free_ x' = free_ z
⊢ V (free_ x') = d
Tactic:
case _ c1 =>
  simp at c1
  simp only [← c1] at h1
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : ¬free_ x' = free_ z
⊢ V (free_ x') = V (free_ x')
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : free_ x' = free_ z
⊢ V (free_ x') = d
Tactic:
simp at c1
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
⊢ V (free_ x') = d

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
⊢ V (free_ x') = d
Tactic:
simp only [← c1] at h1
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
h1 : ¬occursFreeIn (free_ x') F
⊢ V (free_ x') = d

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : x' = z
h1 : ¬occursFreeIn (free_ x') F
⊢ V (free_ x') = d
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
x' : String
a1 : occursFreeIn (free_ x') F
c1 : ¬free_ x' = free_ z
⊢ V (free_ x') = V (free_ x')
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ i) F
⊢ shift D V d (bound_ i) =
    if Var.openList 0 [free_ z] (bound_ i) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ i))
Tactic:
cases i
State after:
case zero
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ shift D V d (bound_ 0) =
    if Var.openList 0 [free_ z] (bound_ 0) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ 0))

case succ
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
n✝ : ℕ
a1 : occursFreeIn (bound_ (n✝ + 1)) F
⊢ shift D V d (bound_ (n✝ + 1)) =
    if Var.openList 0 [free_ z] (bound_ (n✝ + 1)) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ (n✝ + 1)))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ shift D V d (bound_ 0) =
    if Var.openList 0 [free_ z] (bound_ 0) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ 0))
Tactic:
case zero =>
  simp only [shift]
  simp only [Var.openList]
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ shift D V d (bound_ (i + 1)) =
    if Var.openList 0 [free_ z] (bound_ (i + 1)) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ (i + 1)))
Tactic:
case succ i =>
  simp only [shift]
  simp only [Var.openList]
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ shift D V d (bound_ 0) =
    if Var.openList 0 [free_ z] (bound_ 0) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ 0))
Tactic:
simp only [shift]
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ d = if Var.openList 0 [free_ z] (bound_ 0) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ 0))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ d = if Var.openList 0 [free_ z] (bound_ 0) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ 0))
Tactic:
simp only [Var.openList]
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ d =
    if
        (if 0 < 0 then bound_ 0
          else if x : 0 - 0 < [free_ z].length then [free_ z][0 - 0] else bound_ (0 - 0 - [free_ z].length + 0)) =
          free_ z then
      d
    else
      V
        (if 0 < 0 then bound_ 0
        else if x : 0 - 0 < [free_ z].length then [free_ z][0 - 0] else bound_ (0 - 0 - [free_ z].length + 0))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
a1 : occursFreeIn (bound_ 0) F
⊢ d =
    if
        (if 0 < 0 then bound_ 0
          else if x : 0 - 0 < [free_ z].length then [free_ z][0 - 0] else bound_ (0 - 0 - [free_ z].length + 0)) =
          free_ z then
      d
    else
      V
        (if 0 < 0 then bound_ 0
        else if x : 0 - 0 < [free_ z].length then [free_ z][0 - 0] else bound_ (0 - 0 - [free_ z].length + 0))
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ shift D V d (bound_ (i + 1)) =
    if Var.openList 0 [free_ z] (bound_ (i + 1)) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ (i + 1)))
Tactic:
simp only [shift]
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ V (bound_ i) =
    if Var.openList 0 [free_ z] (bound_ (i + 1)) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ (i + 1)))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ V (bound_ i) =
    if Var.openList 0 [free_ z] (bound_ (i + 1)) = free_ z then d else V (Var.openList 0 [free_ z] (bound_ (i + 1)))
Tactic:
simp only [Var.openList]
State after:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ V (bound_ i) =
    if
        (if i + 1 < 0 then bound_ (i + 1)
          else
            if x : i + 1 - 0 < [free_ z].length then [free_ z][i + 1 - 0]
            else bound_ (i + 1 - 0 - [free_ z].length + 0)) =
          free_ z then
      d
    else
      V
        (if i + 1 < 0 then bound_ (i + 1)
        else
          if x : i + 1 - 0 < [free_ z].length then [free_ z][i + 1 - 0] else bound_ (i + 1 - 0 - [free_ z].length + 0))

State before:
D : Type
I : Interpretation D
V : VarAssignment D
F : Formula
z : String
h1 : ¬occursFreeIn (free_ z) F
d : D
i : ℕ
a1 : occursFreeIn (bound_ (i + 1)) F
⊢ V (bound_ i) =
    if
        (if i + 1 < 0 then bound_ (i + 1)
          else
            if x : i + 1 - 0 < [free_ z].length then [free_ z][i + 1 - 0]
            else bound_ (i + 1 - 0 - [free_ z].length + 0)) =
          free_ z then
      d
    else
      V
        (if i + 1 < 0 then bound_ (i + 1)
        else
          if x : i + 1 - 0 < [free_ z].length then [free_ z][i + 1 - 0] else bound_ (i + 1 - 0 - [free_ z].length + 0))
Tactic:
simp
State after:
no goals