NF weak partition development: NFCompactLeafGate.

theorem NFChoice.Compiler.NFCompactLeafGate.axNinCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) : SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex z (SemanticCore.Wff.all w (CompactSourceSyntax.synWb (SemanticCore.Wff.objMem w z) (CompactSourceSyntax.synWnan (SemanticCore.Wff.objMem w x) (SemanticCore.Wff.objMem w y)))))

theorem NFChoice.Compiler.NFCompactLeafGate.axSnCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) : SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex y (SemanticCore.Wff.all z (CompactSourceSyntax.synWb (SemanticCore.Wff.objMem z y) (SemanticCore.Wff.objEq z x))))

theorem NFChoice.Compiler.NFCompactLeafGate.ax1cCompact {S : Fol.Structure Foundation.LNF} (hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF) (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) : SemanticCore.Wff.Valid S (CompactSourceSyntax.synWex x (SemanticCore.Wff.all y (CompactSourceSyntax.synWb (SemanticCore.Wff.objMem y x) (CompactSourceSyntax.synWex z (SemanticCore.Wff.all w (CompactSourceSyntax.synWb (SemanticCore.Wff.objMem w y) (SemanticCore.Wff.objEq w z)))))))