NF weak partition development: NominalNFLiteralHandlers.

@[reducible, inline]

abbrev NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.Theory : Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as Theory.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.Theory = NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalProof (name : Foundation.HailperinAxiomName) : Fol.prf Theory.fst (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula name))

One exact member of the eleven-sentence Metamath Hailperin-derived basis.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalProof name = NFChoice.Fol.prf.axm ⋯

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.openAll (f : Fol.formula Foundation.LNF) (t : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Instantiate the outermost universal of a literal basis sentence.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.openAll body.all t = body [t // 0]f
• NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.openAll f t = f

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.openAll2 (f : Fol.formula Foundation.LNF) (s t : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as openAll2.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxExtAt (s t : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll2 (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axExt)) s t)

Proof-translation construction identified upstream as literalAxExtAt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxNinAt (s t : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll2 (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axNin)) s t)

Proof-translation construction identified upstream as literalAxNinAt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxSnAt (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axSn)) s)

Proof-translation construction identified upstream as literalAxSnAt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxXpAt (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axXp)) s)

Proof-translation construction identified upstream as literalAxXpAt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxCnvAt (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axCnv)) s)

Proof-translation construction identified upstream as literalAxCnvAt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxSiAt (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axSi)) s)

Proof-translation construction identified upstream as literalAxSiAt.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxIns2At (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axIns2)) s)

Proof-translation construction identified upstream as literalAxIns2At.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxIns3At (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axIns3)) s)

Proof-translation construction identified upstream as literalAxIns3At.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxTypeLowerAt (s : Fol.term Foundation.LNF) : Fol.prf Theory.fst (openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axTypeLower)) s)

Proof-translation construction identified upstream as literalAxTypeLowerAt.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axExtGoal (x y z : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axExtGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axNinGoal (x y z w : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axNinGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSnGoal (x y z : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axSnGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.ax1cGoal (x y z w : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as ax1cGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axXpGoal (x y z w t : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axXpGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axCnvGoal (x y z w : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axCnvGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSsetGoal (x y z w : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axSsetGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSiGoal (x y z w : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axSiGoal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axIns2Goal (x y z w t : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axIns2Goal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axIns3Goal (x y z w t : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axIns3Goal.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axTypeLowerGoal (x y z w : SemanticCore.Var) : SemanticCore.Wff

Proof-translation construction identified upstream as axTypeLowerGoal.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axExtOfLowering (x y z : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hyz : y ≠ z) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axExtGoal x y z) = openAll2 (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axExt)) &(rho x) &(rho y)) : NPrf (axExtGoal x y z)

Proof-translation construction identified upstream as axExtOfLowering.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axExtOfLowering x y z _hxy _hxz _hyz hLower rho = ⋯.mpr (NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxExtAt &(rho x) &(rho y))

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axNinOfLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (_hyz : y ≠ z) (_hyw : y ≠ w) (_hzw : z ≠ w) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axNinGoal x y z w) = openAll2 (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axNin)) &(rho x) &(rho y)) : NPrf (axNinGoal x y z w)

Proof-translation construction identified upstream as axNinOfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSnOfLowering (x y z : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hyz : y ≠ z) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axSnGoal x y z) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axSn)) &(rho x)) : NPrf (axSnGoal x y z)

Proof-translation construction identified upstream as axSnOfLowering.

Equations

• NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSnOfLowering x y z _hxy _hxz _hyz hLower rho = ⋯.mpr (NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.literalAxSnAt &(rho x))

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.ax1cOfLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (_hyz : y ≠ z) (_hyw : y ≠ w) (_hzw : z ≠ w) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (ax1cGoal x y z w) = Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.ax1c)) : NPrf (ax1cGoal x y z w)

Proof-translation construction identified upstream as ax1cOfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axXpOfLowering (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) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axXpGoal x y z w t) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axXp)) &(rho x)) : NPrf (axXpGoal x y z w t)

Proof-translation construction identified upstream as axXpOfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axCnvOfLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (_hyz : y ≠ z) (_hyw : y ≠ w) (_hzw : z ≠ w) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axCnvGoal x y z w) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axCnv)) &(rho x)) : NPrf (axCnvGoal x y z w)

Proof-translation construction identified upstream as axCnvOfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSsetOfLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (_hyz : y ≠ z) (_hyw : y ≠ w) (_hzw : z ≠ w) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axSsetGoal x y z w) = Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axSset)) : NPrf (axSsetGoal x y z w)

Proof-translation construction identified upstream as axSsetOfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axSiOfLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (_hyz : y ≠ z) (_hyw : y ≠ w) (_hzw : z ≠ w) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axSiGoal x y z w) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axSi)) &(rho x)) : NPrf (axSiGoal x y z w)

Proof-translation construction identified upstream as axSiOfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axIns2OfLowering (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) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axIns2Goal x y z w t) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axIns2)) &(rho x)) : NPrf (axIns2Goal x y z w t)

Proof-translation construction identified upstream as axIns2OfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axIns3OfLowering (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) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axIns3Goal x y z w t) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axIns3)) &(rho x)) : NPrf (axIns3Goal x y z w t)

Proof-translation construction identified upstream as axIns3OfLowering.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.NFLiteralHandlers.axTypeLowerOfLowering (x y z w : SemanticCore.Var) (_hxy : x ≠ y) (_hxz : x ≠ z) (_hxw : x ≠ w) (_hyz : y ≠ z) (_hyw : y ≠ w) (_hzw : z ≠ w) (hLower : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (axTypeLowerGoal x y z w) = openAll (Fol.BoundedPreformula.fst (Foundation.ExactLiteralTrial.literalAxiomFormula Foundation.HailperinAxiomName.axTypeLower)) &(rho x)) : NPrf (axTypeLowerGoal x y z w)

Proof-translation construction identified upstream as axTypeLowerOfLowering.

Equations

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