NF weak partition development: NFStandard.WPP.

def NFChoice.Foundation.NFStandard.WPPSyntax : Sentence

The closed intrinsic formula obtained by lowering the accepted WPP source.

Equations

• NFChoice.Foundation.NFStandard.WPPSyntax = (NFChoice.SemanticCore.PartialLowering.lowerClosed NFChoice.Compiler.CompactSourceSyntax.synWwpp).getD NFChoice.Foundation.Formula.falsum

theorem NFChoice.Foundation.NFStandard.lowerClosed_syn_wwpp : SemanticCore.PartialLowering.lowerClosed Compiler.CompactSourceSyntax.synWwpp = some WPPSyntax

def NFChoice.Foundation.NFStandard.WPP : Fol.sentence LNF

WPP as a Flypitch sentence, exactly lowered from the accepted source.

Equations

• NFChoice.Foundation.NFStandard.WPP = NFChoice.Foundation.Formula.toFlypitch NFChoice.Foundation.NFStandard.WPPSyntax