NF weak partition development: NominalWffPrf.

def NFChoice.DirectNominalPrf.Nominal.liftRho (rho : SemanticCore.Var → ℕ) : SemanticCore.Var → ℕ

Proof-translation construction identified upstream as liftRho.

Equations

• NFChoice.DirectNominalPrf.Nominal.liftRho rho x = rho x + 1

def NFChoice.DirectNominalPrf.Nominal.bindRho (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : SemanticCore.Var → ℕ

Proof-translation construction identified upstream as bindRho.

Equations

• NFChoice.DirectNominalPrf.Nominal.bindRho rho x y = if y = x then 0 else rho y + 1

def NFChoice.DirectNominalPrf.Nominal.updateRho (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (value : ℕ) : SemanticCore.Var → ℕ

Proof-translation construction identified upstream as updateRho.

Equations

• NFChoice.DirectNominalPrf.Nominal.updateRho rho x value y = if y = x then value else rho y

def NFChoice.DirectNominalPrf.Nominal.neg (p : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as neg.

Equations

• NFChoice.DirectNominalPrf.Nominal.neg p = NFChoice.Fol.preformula.imp p ⊥'

def NFChoice.DirectNominalPrf.Nominal.conj (p q : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as conj.

Equations

• NFChoice.DirectNominalPrf.Nominal.conj p q = NFChoice.DirectNominalPrf.Nominal.neg (NFChoice.Fol.preformula.imp p (NFChoice.DirectNominalPrf.Nominal.neg q))

def NFChoice.DirectNominalPrf.Nominal.biimp (p q : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as biimp.

Equations

• NFChoice.DirectNominalPrf.Nominal.biimp p q = NFChoice.DirectNominalPrf.Nominal.conj (NFChoice.Fol.preformula.imp p q) (NFChoice.Fol.preformula.imp q p)

def NFChoice.DirectNominalPrf.Nominal.ex (p : Fol.formula Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as ex.

Equations

• NFChoice.DirectNominalPrf.Nominal.ex p = NFChoice.DirectNominalPrf.Nominal.neg (NFChoice.Fol.preformula.all (NFChoice.DirectNominalPrf.Nominal.neg p))

def NFChoice.DirectNominalPrf.Nominal.lowerClassPred (rho : SemanticCore.Var → ℕ) (candidate : ℕ) : SemanticCore.Class → Fol.formula Foundation.LNF

Proof-translation construction identified upstream as lowerClassPred.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectNominalPrf.Nominal.lowerClassPred rho candidate (NFChoice.SemanticCore.Class.cv x_1) = NFChoice.DirectNominalPrf.GenericLogicalHandlers.nfMem &candidate &(rho x_1)

def NFChoice.DirectNominalPrf.Nominal.lowerWff (rho : SemanticCore.Var → ℕ) : SemanticCore.Wff → Fol.formula Foundation.LNF

Proof-translation construction identified upstream as lowerWff.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectNominalPrf.Nominal.lowerWff rho NFChoice.SemanticCore.Wff.falsum = ⊥'
• NFChoice.DirectNominalPrf.Nominal.lowerWff rho (p.imp q) = NFChoice.Fol.preformula.imp (NFChoice.DirectNominalPrf.Nominal.lowerWff rho p) (NFChoice.DirectNominalPrf.Nominal.lowerWff rho q)
• NFChoice.DirectNominalPrf.Nominal.lowerWff rho (NFChoice.SemanticCore.Wff.objEq x_1 y) = NFChoice.Fol.preformula.equal &(rho x_1) &(rho y)
• NFChoice.DirectNominalPrf.Nominal.lowerWff rho (NFChoice.SemanticCore.Wff.objMem x_1 y) = NFChoice.DirectNominalPrf.GenericLogicalHandlers.nfMem &(rho x_1) &(rho y)

def NFChoice.DirectNominalPrf.Nominal.NPrf (p : SemanticCore.Wff) : Type

Proof-translation construction identified upstream as NPrf.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.mp {p q : SemanticCore.Wff} (hp : NPrf p) (hpq : NPrf (p.imp q)) : NPrf q

Proof-translation construction identified upstream as mp.

Equations

• NFChoice.DirectNominalPrf.Nominal.mp hp hpq rho = NFChoice.DirectNominalPrf.GenericLogicalHandlers.mp (hp rho) (hpq rho)

def NFChoice.DirectNominalPrf.Nominal.ax1 (p q : SemanticCore.Wff) : NPrf (p.imp (q.imp p))

Proof-translation construction identified upstream as ax1.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax2 (p q r : SemanticCore.Wff) : NPrf ((p.imp (q.imp r)).imp ((p.imp q).imp (p.imp r)))

Proof-translation construction identified upstream as ax2.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax3 (p q : SemanticCore.Wff) : NPrf ((p.neg.imp q.neg).imp (q.imp p))

Proof-translation construction identified upstream as ax3.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.axMeredith (p q r s t : SemanticCore.Wff) : NPrf (((((p.imp q).imp (r.neg.imp s.neg)).imp r).imp t).imp ((t.imp p).imp (s.imp p)))

Proof-translation construction identified upstream as axMeredith.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.biimpRefl (p : SemanticCore.Wff) : NPrf (p.biimp p)

A source definition becomes reflexivity after its constructor is unfolded.

Equations

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