NF weak partition development: NominalNFLiteralBaseFour.

theorem NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axExtLowering (x y z : SemanticCore.Var) (_hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (rho : SemanticCore.Var → ℕ) : lowerWff rho (NFLiteralHandlers.axExtGoal x y z) = NFLiteralHandlers.openAll2 (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axExt)) &(rho x) &(rho y)

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axExt (x y z : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) : NPrf (NFLiteralHandlers.axExtGoal x y z)

Proof-translation construction identified upstream as axExt.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axExt x y z hxy hxz hyz = NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axExtOfLowering x y z hxy hxz hyz ⋯

theorem NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axNinLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) (rho : SemanticCore.Var → ℕ) : lowerWff rho (NFLiteralHandlers.axNinGoal x y z w) = NFLiteralHandlers.openAll2 (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axNin)) &(rho x) &(rho y)

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axNin (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) : NPrf (NFLiteralHandlers.axNinGoal x y z w)

Proof-translation construction identified upstream as axNin.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axNin x y z w hxy hxz hxw hyz hyw hzw = NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axNinOfLowering x y z w hxy hxz hxw hyz hyw hzw ⋯

theorem NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axSnLowering (x y z : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) (rho : SemanticCore.Var → ℕ) : lowerWff rho (NFLiteralHandlers.axSnGoal x y z) = NFLiteralHandlers.openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axSn)) &(rho x)

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axSn (x y z : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hyz : y ≠ z) : NPrf (NFLiteralHandlers.axSnGoal x y z)

Proof-translation construction identified upstream as axSn.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.axSn x y z hxy hxz hyz = NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSnOfLowering x y z hxy hxz hyz ⋯

theorem NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.ax1cLowering (x y z w : SemanticCore.Var) (hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) (rho : SemanticCore.Var → ℕ) : lowerWff rho (NFLiteralHandlers.ax1cGoal x y z w) = Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.ax1c)

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.ax1c (x y z w : SemanticCore.Var) (hxy : x ≠ y) (hxz : x ≠ z) (hxw : x ≠ w) (hyz : y ≠ z) (hyw : y ≠ w) (hzw : z ≠ w) : NPrf (NFLiteralHandlers.ax1cGoal x y z w)

Proof-translation construction identified upstream as ax1c.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralBaseFour.ax1c x y z w hxy hxz hxw hyz hyw hzw = NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.ax1cOfLowering x y z w hxy hxz hxw hyz hyw hzw ⋯