NF weak partition development: NFLeafWrappers.Basic.
Typed source-leaf adapters for the ten non-extensional Hailperin axioms.
The caller supplies the actual Expander-normalized primitive nominal body. In
particular, this keeps every synthetic class-abstraction dummy explicit in the
generated term rather than fixing a global name here. The two computational
side conditions are exactly the certificate accepted by valid_literal_leaf:
the universal-closure list covers the free names and lowering that closure is
the literal source sentence.
Although the source $d hypotheses are not needed after the lowering
certificate has been checked, they are retained verbatim in every adapter.
This makes the generated call site expose precisely the contract checked by
Metamath before substitution.
theorem
NFChoice.NFLeafWrappers.source_ax_nin
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x, y].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x, y] p) = some Foundation.ExactLiteralTrial.literalAxNin)
:
theorem
NFChoice.NFLeafWrappers.source_ax_xp
{S : Fol.Structure Foundation.LNF}
(hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF)
(x y z w t : SemanticCore.Var)
(_hxy : x ≠ y)
(_hxz : x ≠ z)
(_hxw : x ≠ w)
(_hxt : x ≠ t)
(_hyz : y ≠ z)
(_hyw : y ≠ w)
(_hyt : y ≠ t)
(_hzw : z ≠ w)
(_hzt : z ≠ t)
(_hwt : w ≠ t)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxXp)
:
theorem
NFChoice.NFLeafWrappers.source_ax_cnv
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxCnv)
:
theorem
NFChoice.NFLeafWrappers.source_ax_1c
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [] p) = some Foundation.ExactLiteralTrial.literalAx1c)
:
theorem
NFChoice.NFLeafWrappers.source_ax_sset
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [] p) = some Foundation.ExactLiteralTrial.literalAxSset)
:
theorem
NFChoice.NFLeafWrappers.source_ax_si
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxSi)
:
theorem
NFChoice.NFLeafWrappers.source_ax_ins2
{S : Fol.Structure Foundation.LNF}
(hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF)
(x y z w t : SemanticCore.Var)
(_hxy : x ≠ y)
(_hxz : x ≠ z)
(_hxw : x ≠ w)
(_hxt : x ≠ t)
(_hyz : y ≠ z)
(_hyw : y ≠ w)
(_hyt : y ≠ t)
(_hzw : z ≠ w)
(_hzt : z ≠ t)
(_hwt : w ≠ t)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxIns2)
:
theorem
NFChoice.NFLeafWrappers.source_ax_ins3
{S : Fol.Structure Foundation.LNF}
(hNF : Fol.allRealizeSentence S Foundation.ExactLiteralTrial.LiteralHailperinNF)
(x y z w t : SemanticCore.Var)
(_hxy : x ≠ y)
(_hxz : x ≠ z)
(_hxw : x ≠ w)
(_hxt : x ≠ t)
(_hyz : y ≠ z)
(_hyw : y ≠ w)
(_hyt : y ≠ t)
(_hzw : z ≠ w)
(_hzt : z ≠ t)
(_hwt : w ≠ t)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxIns3)
:
theorem
NFChoice.NFLeafWrappers.source_ax_typlower
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxTypeLower)
:
theorem
NFChoice.NFLeafWrappers.source_ax_sn
{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)
(p : SemanticCore.Wff)
(hcover : p.fv ⊆ [x].toFinset)
(hlower :
SemanticCore.PartialLowering.lowerClosed (SemanticCore.PartialLowering.closeNames [x] p) = some Foundation.ExactLiteralTrial.literalAxSn)
: