Theorem: FOL.NV.Forall_isFreeIn (FOL/NV/Margaris/Fol.lean)

State before:
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (Forall_ xs P) ↔ x ∉ xs ∧ isFreeIn x P
Tactic:
simp only [Formula.Forall_]
State after:
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (List.foldr forall_ P xs) ↔ x ∉ xs ∧ isFreeIn x P

State before:
P : Formula
xs : List VarName
x : VarName
⊢ isFreeIn x (List.foldr forall_ P xs) ↔ x ∉ xs ∧ isFreeIn x P
Tactic:
induction xs
State after:
case nil
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P

case cons
P : Formula
x head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isFreeIn x (List.foldr forall_ P tail✝) ↔ x ∉ tail✝ ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (head✝ :: tail✝)) ↔ x ∉ head✝ :: tail✝ ∧ isFreeIn x P

State before:
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P
Tactic:
case nil =>
  simp
State after:
no goals

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∉ xs_hd :: xs_tl ∧ isFreeIn x P
Tactic:
case cons xs_hd xs_tl xs_ih =>
  simp
  simp only [isFreeIn]
  simp only [xs_ih]
  tauto
State after:
no goals

State before:
P : Formula
x : VarName
⊢ isFreeIn x (List.foldr forall_ P []) ↔ x ∉ [] ∧ isFreeIn x P
Tactic:
simp
State after:
no goals

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (List.foldr forall_ P (xs_hd :: xs_tl)) ↔ x ∉ xs_hd :: xs_tl ∧ isFreeIn x P
Tactic:
simp
State after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ isFreeIn x (forall_ xs_hd (List.foldr forall_ P xs_tl)) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Tactic:
simp only [isFreeIn]
State after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ isFreeIn x (List.foldr forall_ P xs_tl) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ isFreeIn x (List.foldr forall_ P xs_tl) ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Tactic:
simp only [xs_ih]
State after:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ x ∉ xs_tl ∧ isFreeIn x P ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P

State before:
P : Formula
x xs_hd : VarName
xs_tl : List VarName
xs_ih : isFreeIn x (List.foldr forall_ P xs_tl) ↔ x ∉ xs_tl ∧ isFreeIn x P
⊢ ¬x = xs_hd ∧ x ∉ xs_tl ∧ isFreeIn x P ↔ (¬x = xs_hd ∧ x ∉ xs_tl) ∧ isFreeIn x P
Tactic:
tauto
State after:
no goals