NF weak partition development: ClassBoundaryNormalizationDev005.

def NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.mem (s t : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as mem.

Equations

• NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.mem s t = ((NFChoice.Fol.preformula.rel NFChoice.Foundation.LNFRelation.mem).apprel s).apprel t

def NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.cvPred (x : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as cvPred.

Equations

• NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.cvPred x = NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.mem (&0) (NFChoice.Fol.liftTerm1 x)

def NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.applyPred (P : Fol.formula Foundation.LNF) (x : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as applyPred.

Equations

• NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.applyPred P x = P [x // 0]f

def NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.represents (x : Fol.term Foundation.LNF) (P : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as represents.

Equations

• One or more equations did not get rendered due to their size.

theorem NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.cvPredLiftForWitness (x : Fol.term Foundation.LNF) : cvPred (Fol.liftTerm1 x) = cvPred x ↑f' 1 # 1

theorem NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.representsWitnessSubst (x : Fol.term Foundation.LNF) : represents (&0) (cvPred x ↑f' 1 # 1) [x // 0]f = represents x (cvPred x)

theorem NFChoice.DirectCertificate.ClassBoundaryNormalizationDev005.classMemWitnessBodySubst (x : Fol.term Foundation.LNF) (Q : Fol.formula Foundation.LNF) : Fol.and' (represents (&0) (cvPred x ↑f' 1 # 1)) Q [x // 0]f = Fol.and' (represents x (cvPred x)) (applyPred Q x)