NF weak partition development: NominalLogicalWrappersComplete.

Coincident-variable branches erased by the MM0 Lean exporter.

def NFChoice.DirectNominalPrf.Nominal.impRefl {L : Fol.Language} (Γ : Set (Fol.formula L)) (p : Fol.formula L) : Fol.prf Γ (Fol.preformula.imp p p)

Proof-translation construction identified upstream as impRefl.

Equations

• NFChoice.DirectNominalPrf.Nominal.impRefl Γ p = (NFChoice.Fol.prf.axm ⋯).impI

def NFChoice.DirectNominalPrf.Nominal.ax7Same (x : SemanticCore.Var) (p : SemanticCore.Wff) : NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all x p)).imp (SemanticCore.Wff.all x (SemanticCore.Wff.all x p)))

The x = y branch of quantifier commutation is implication reflexivity.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax7 (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hSwap : ∀ (rho : SemanticCore.Var → ℕ), y ≠ x → lowerWff (bindRho (bindRho rho y) x) p = GenericLogicalHandlers.swap01 (lowerWff (bindRho (bindRho rho x) y) p)) : NPrf ((SemanticCore.Wff.all x (SemanticCore.Wff.all y p)).imp (SemanticCore.Wff.all y (SemanticCore.Wff.all x p)))

Total ax-7: the emitter supplies only the noncoincident de-Bruijn swap identity; the coincident branch is discharged here.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax9SelfCore (Γ : Set (Fol.formula Foundation.LNF)) : Fol.prf Γ (Fol.not' (Fol.preformula.all (Fol.not' (Fol.preformula.equal &0 &0))))

Equality existence when the source names in ax-9 coincide.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax9 (x y : SemanticCore.Var) : NPrf (SemanticCore.Wff.all x (SemanticCore.Wff.objEq x y).neg).neg

Total Metamath ax-9, including x = y.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax12SameXYCore (Γ : Set (Fol.formula Foundation.LNF)) (s : Fol.term Foundation.LNF) (q : Fol.formula Foundation.LNF) : Fol.prf Γ (Fol.preformula.imp (Fol.not' (Fol.preformula.equal s s)) q)

Ex falso branch of ax-12 when x = y.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax12SameXZCore (Γ : Set (Fol.formula Foundation.LNF)) (s t : Fol.term Foundation.LNF) (q : Fol.formula Foundation.LNF) : Fol.prf Γ (Fol.preformula.imp (Fol.not' (Fol.preformula.equal s t)) ((Fol.preformula.equal t s).imp q))

Ex falso branch of ax-12 when x = z but x ≠ y.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax12 (x y z : SemanticCore.Var) : NPrf ((SemanticCore.Wff.objEq x y).neg.imp ((SemanticCore.Wff.objEq y z).imp (SemanticCore.Wff.all x (SemanticCore.Wff.objEq y z))))

Total Metamath ax-12, including every bundled-variable coincidence.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax11SameCore (Γ : Set (Fol.formula Foundation.LNF)) (s : Fol.term Foundation.LNF) (body : Fol.formula Foundation.LNF) : Fol.prf Γ ((Fol.preformula.equal s s).imp ((Fol.preformula.all body).imp ((Fol.preformula.equal &0 &0).imp body).all))

ax-11 when its two bundled source names coincide.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ax11Same (x : SemanticCore.Var) (p : SemanticCore.Wff) : NPrf ((SemanticCore.Wff.objEq x x).imp ((SemanticCore.Wff.all x p).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x x).imp p))))

Nominal ax-11 coincident branch.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax11 (x y : SemanticCore.Var) (p : SemanticCore.Wff) (template : (SemanticCore.Var → ℕ) → Fol.formula Foundation.LNF) (hSource : ∀ (rho : SemanticCore.Var → ℕ), y ≠ x → GenericLogicalHandlers.ax11Inst (lowerWff (bindRho rho y) p) &(rho y) = template rho [Fol.liftTerm1 &(rho x) // 0]f) (hTarget : ∀ (rho : SemanticCore.Var → ℕ), y ≠ x → template rho [&0 // 0]f = lowerWff (bindRho rho x) p) : NPrf ((SemanticCore.Wff.objEq x y).imp ((SemanticCore.Wff.all y p).imp (SemanticCore.Wff.all x ((SemanticCore.Wff.objEq x y).imp p))))

Total ax-11: the emitter's template equalities are needed only when its two bundled source names differ.

Equations

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