Documentation

LeanPool.NFWeakPartition.CoreFVSimp

NF weak partition development: CoreFVSimp.

Shallow, nonrecursive simplification equations for semantic FV support.

source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_class_cv (x : SemanticCore.Var) :
(SemanticCore.Class.cv x).fv = {x}
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_class_cab (x : SemanticCore.Var) (p : SemanticCore.Wff) :
(SemanticCore.Class.cab x p).fv = p.fv.erase x
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_falsum :
SemanticCore.Wff.falsum.fv = ∅
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_imp (p q : SemanticCore.Wff) :
(p.imp q).fv = p.fv ∪ q.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_all (x : SemanticCore.Var) (p : SemanticCore.Wff) :
(SemanticCore.Wff.all x p).fv = p.fv.erase x
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_objEq (x y : SemanticCore.Var) :
(SemanticCore.Wff.objEq x y).fv = {x, y}
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_objMem (x y : SemanticCore.Var) :
(SemanticCore.Wff.objMem x y).fv = {x, y}
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_classEq (A B : SemanticCore.Class) :
(SemanticCore.Wff.classEq A B).fv = A.fv ∪ B.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_classMem (A B : SemanticCore.Class) :
(SemanticCore.Wff.classMem A B).fv = A.fv ∪ B.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_neg (p : SemanticCore.Wff) :
p.neg.fv = p.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_conj (p q : SemanticCore.Wff) :
(p.conj q).fv = p.fv ∪ q.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_disj (p q : SemanticCore.Wff) :
(p.disj q).fv = p.fv ∪ q.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_biimp (p q : SemanticCore.Wff) :
(p.biimp q).fv = p.fv ∪ q.fv
source
@[simp]
theorem NFChoice.Compiler.CoreFVSimp.fv_wff_ex (x : SemanticCore.Var) (p : SemanticCore.Wff) :
(SemanticCore.Wff.ex x p).fv = p.fv.erase x