Theorem: LN.Formula.OpenListLC (FOL/LN/Paper.lean)

State before:
F : Formula
j : ℕ
zs : List String
h1 : lc_at j F
⊢ openList j (List.map free_ zs) F = F
Tactic:
induction F generalizing j
State after:
case pred_
zs : List String
a✝¹ : String
a✝ : List Var
j : ℕ
h1 : lc_at j (pred_ a✝¹ a✝)
⊢ openList j (List.map free_ zs) (pred_ a✝¹ a✝) = pred_ a✝¹ a✝

case not_
zs : List String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j a✝.not_
⊢ openList j (List.map free_ zs) a✝.not_ = a✝.not_

case imp_
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (j : ℕ), lc_at j a✝¹ → openList j (List.map free_ zs) a✝¹ = a✝¹
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j (a✝¹.imp_ a✝)
⊢ openList j (List.map free_ zs) (a✝¹.imp_ a✝) = a✝¹.imp_ a✝

case forall_
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (j : ℕ), lc_at j a✝ → openList j (List.map free_ zs) a✝ = a✝
j : ℕ
h1 : lc_at j (forall_ a✝¹ a✝)
⊢ openList j (List.map free_ zs) (forall_ a✝¹ a✝) = forall_ a✝¹ a✝

State before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : lc_at j (pred_ X vs)
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Tactic:
case pred_ X vs =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  simp
  apply List.map_mem_id
  intro v a1
  specialize h1 v a1
  cases v
  case _ x =>
    simp only [Var.openList]
  case _ i =>
    cases i
    case zero =>
      simp only [Var.lc_at] at h1
      simp only [Var.openList]
      simp only [if_pos h1]
    case succ i =>
      simp only [Var.lc_at] at h1
      simp only [Var.openList]
      simp only [if_pos h1]
State after:
no goals

State before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi.not_
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  congr!
  exact phi_ih j h1
State after:
no goals

State before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j (forall_ x phi)
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Tactic:
case forall_ x phi phi_ih =>
  simp only [Formula.lc_at] at h1
  simp only [Formula.openList]
  simp
  exact phi_ih (j + 1) h1
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : lc_at j (pred_ X vs)
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Tactic:
simp only [Formula.lc_at] at h1
State after:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs

State before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ openList j (List.map free_ zs) (pred_ X vs) = pred_ X vs
Tactic:
simp only [Formula.openList]
State after:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ pred_ X (List.map (Var.openList j (List.map free_ zs)) vs) = pred_ X vs

State before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ pred_ X (List.map (Var.openList j (List.map free_ zs)) vs) = pred_ X vs
Tactic:
simp
State after:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map (Var.openList j (List.map free_ zs)) vs = vs

State before:
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ List.map (Var.openList j (List.map free_ zs)) vs = vs
Tactic:
apply List.map_mem_id
State after:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, Var.openList j (List.map free_ zs) x = x

State before:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
⊢ ∀ x ∈ vs, Var.openList j (List.map free_ zs) x = x
Tactic:
intro v a1
State after:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ Var.openList j (List.map free_ zs) v = v

State before:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
h1 : ∀ v ∈ vs, Var.lc_at j v
v : Var
a1 : v ∈ vs
⊢ Var.openList j (List.map free_ zs) v = v
Tactic:
specialize h1 v a1
State after:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
h1 : Var.lc_at j v
⊢ Var.openList j (List.map free_ zs) v = v

State before:
case h1
zs : List String
X : String
vs : List Var
j : ℕ
v : Var
a1 : v ∈ vs
h1 : Var.lc_at j v
⊢ Var.openList j (List.map free_ zs) v = v
Tactic:
cases v
State after:
case h1.free_
zs : List String
X : String
vs : List Var
j : ℕ
a✝ : String
a1 : free_ a✝ ∈ vs
h1 : Var.lc_at j (free_ a✝)
⊢ Var.openList j (List.map free_ zs) (free_ a✝) = free_ a✝

case h1.bound_
zs : List String
X : String
vs : List Var
j a✝ : ℕ
a1 : bound_ a✝ ∈ vs
h1 : Var.lc_at j (bound_ a✝)
⊢ Var.openList j (List.map free_ zs) (bound_ a✝) = bound_ a✝

State before:
zs : List String
X : String
vs : List Var
j : ℕ
x : String
a1 : free_ x ∈ vs
h1 : Var.lc_at j (free_ x)
⊢ Var.openList j (List.map free_ zs) (free_ x) = free_ x
Tactic:
case _ x =>
  simp only [Var.openList]
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ i ∈ vs
h1 : Var.lc_at j (bound_ i)
⊢ Var.openList j (List.map free_ zs) (bound_ i) = bound_ i
Tactic:
case _ i =>
  cases i
  case zero =>
    simp only [Var.lc_at] at h1
    simp only [Var.openList]
    simp only [if_pos h1]
  case succ i =>
    simp only [Var.lc_at] at h1
    simp only [Var.openList]
    simp only [if_pos h1]
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j : ℕ
x : String
a1 : free_ x ∈ vs
h1 : Var.lc_at j (free_ x)
⊢ Var.openList j (List.map free_ zs) (free_ x) = free_ x
Tactic:
simp only [Var.openList]
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ i ∈ vs
h1 : Var.lc_at j (bound_ i)
⊢ Var.openList j (List.map free_ zs) (bound_ i) = bound_ i
Tactic:
cases i
State after:
case zero
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0

case succ
zs : List String
X : String
vs : List Var
j n✝ : ℕ
a1 : bound_ (n✝ + 1) ∈ vs
h1 : Var.lc_at j (bound_ (n✝ + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (n✝ + 1)) = bound_ (n✝ + 1)

State before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Tactic:
case zero =>
  simp only [Var.lc_at] at h1
  simp only [Var.openList]
  simp only [if_pos h1]
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : Var.lc_at j (bound_ (i + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Tactic:
case succ i =>
  simp only [Var.lc_at] at h1
  simp only [Var.openList]
  simp only [if_pos h1]
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : Var.lc_at j (bound_ 0)
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Tactic:
simp only [Var.lc_at] at h1
State after:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0

State before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ Var.openList j (List.map free_ zs) (bound_ 0) = bound_ 0
Tactic:
simp only [Var.openList]
State after:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ (if 0 < j then bound_ 0
    else
      if x : 0 - j < (List.map free_ zs).length then (List.map free_ zs)[0 - j]
      else bound_ (0 - j - (List.map free_ zs).length + j)) =
    bound_ 0

State before:
zs : List String
X : String
vs : List Var
j : ℕ
a1 : bound_ 0 ∈ vs
h1 : 0 < j
⊢ (if 0 < j then bound_ 0
    else
      if x : 0 - j < (List.map free_ zs).length then (List.map free_ zs)[0 - j]
      else bound_ (0 - j - (List.map free_ zs).length + j)) =
    bound_ 0
Tactic:
simp only [if_pos h1]
State after:
no goals

State before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : Var.lc_at j (bound_ (i + 1))
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Tactic:
simp only [Var.lc_at] at h1
State after:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)

State before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ Var.openList j (List.map free_ zs) (bound_ (i + 1)) = bound_ (i + 1)
Tactic:
simp only [Var.openList]
State after:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ (if i + 1 < j then bound_ (i + 1)
    else
      if x : i + 1 - j < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - j]
      else bound_ (i + 1 - j - (List.map free_ zs).length + j)) =
    bound_ (i + 1)

State before:
zs : List String
X : String
vs : List Var
j i : ℕ
a1 : bound_ (i + 1) ∈ vs
h1 : i + 1 < j
⊢ (if i + 1 < j then bound_ (i + 1)
    else
      if x : i + 1 - j < (List.map free_ zs).length then (List.map free_ zs)[i + 1 - j]
      else bound_ (i + 1 - j - (List.map free_ zs).length + j)) =
    bound_ (i + 1)
Tactic:
simp only [if_pos h1]
State after:
no goals

State before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi.not_
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Tactic:
simp only [Formula.lc_at] at h1
State after:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_

State before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi.not_ = phi.not_
Tactic:
simp only [Formula.openList]
State after:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ (openList j (List.map free_ zs) phi).not_ = phi.not_

State before:
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ (openList j (List.map free_ zs) phi).not_ = phi.not_
Tactic:
congr!
State after:
case h.e'_1
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi = phi

State before:
case h.e'_1
zs : List String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j phi
⊢ openList j (List.map free_ zs) phi = phi
Tactic:
exact phi_ih j h1
State after:
no goals

State before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j (phi.imp_ psi)
⊢ openList j (List.map free_ zs) (phi.imp_ psi) = phi.imp_ psi
Tactic:
simp only [Formula.lc_at] at h1
State after:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ openList j (List.map free_ zs) (phi.imp_ psi) = phi.imp_ psi

State before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ openList j (List.map free_ zs) (phi.imp_ psi) = phi.imp_ psi
Tactic:
simp only [Formula.openList]
State after:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi

State before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1 : lc_at j phi ∧ lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
Tactic:
cases h1
State after:
case intro
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
left✝ : lc_at j phi
right✝ : lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi

State before:
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ (openList j (List.map free_ zs) phi).imp_ (openList j (List.map free_ zs) psi) = phi.imp_ psi
Tactic:
congr!
State after:
case h.e'_1
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) phi = phi

case h.e'_2
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) psi = psi

State before:
case h.e'_1
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) phi = phi
Tactic:
exact phi_ih j h1_left
State after:
no goals

State before:
case h.e'_2
zs : List String
phi psi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
psi_ih : ∀ (j : ℕ), lc_at j psi → openList j (List.map free_ zs) psi = psi
j : ℕ
h1_left : lc_at j phi
h1_right : lc_at j psi
⊢ openList j (List.map free_ zs) psi = psi
Tactic:
exact psi_ih j h1_right
State after:
no goals

State before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at j (forall_ x phi)
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Tactic:
simp only [Formula.lc_at] at h1
State after:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi

State before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList j (List.map free_ zs) (forall_ x phi) = forall_ x phi
Tactic:
simp only [Formula.openList]
State after:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ forall_ x (openList (j + 1) (List.map free_ zs) phi) = forall_ x phi

State before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ forall_ x (openList (j + 1) (List.map free_ zs) phi) = forall_ x phi
Tactic:
simp
State after:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList (j + 1) (List.map free_ zs) phi = phi

State before:
zs : List String
x : String
phi : Formula
phi_ih : ∀ (j : ℕ), lc_at j phi → openList j (List.map free_ zs) phi = phi
j : ℕ
h1 : lc_at (j + 1) phi
⊢ openList (j + 1) (List.map free_ zs) phi = phi
Tactic:
exact phi_ih (j + 1) h1
State after:
no goals