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

State before:
P_u P_v : Formula
u v : VarName
h1 : Similar P_u P_v u v
⊢ Similar P_u.not_ P_v.not_ u v
Tactic:
simp only [Similar] at *
State after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u.not_ ∧
    ¬isFreeIn u P_v.not_ ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_

State before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u.not_ ∧
    ¬isFreeIn u P_v.not_ ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [isFreeIn] at *
State after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_

State before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u ∧ fastAdmits v u P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmits u v P_u.not_ ∧
        fastAdmits v u P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [fastAdmits] at *
State after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u.not_ ∧
        fastAdmitsAux v u ∅ P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_

State before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u.not_ ∧
        fastAdmitsAux v u ∅ P_v.not_ ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [fastAdmitsAux] at *
State after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_

State before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = fastReplaceFree u v P_u.not_ ∧ P_u.not_ = fastReplaceFree v u P_v.not_
Tactic:
simp only [fastReplaceFree] at *
State after:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = (fastReplaceFree u v P_u).not_ ∧ P_u.not_ = (fastReplaceFree v u P_v).not_

State before:
P_u P_v : Formula
u v : VarName
h1 :
  ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧ fastAdmitsAux v u ∅ P_v ∧ P_v = fastReplaceFree u v P_u ∧ P_u = fastReplaceFree v u P_v
⊢ ¬isFreeIn v P_u ∧
    ¬isFreeIn u P_v ∧
      fastAdmitsAux u v ∅ P_u ∧
        fastAdmitsAux v u ∅ P_v ∧ P_v.not_ = (fastReplaceFree u v P_u).not_ ∧ P_u.not_ = (fastReplaceFree v u P_v).not_
Tactic:
tauto
State after:
no goals