NF weak partition development: GenericLogicalHandlers.

Proof-producing counterparts of the propositional Metamath kernel leaves. They are independent of the nominal syntax representation: the nominal compiler only has to lower its instantiated formulas and call these terms.

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax1 {L : Fol.Language} (Γ : Set (Fol.formula L)) (p q : Fol.formula L) : Fol.prf Γ (Fol.preformula.imp p (Fol.preformula.imp q p))

Proof-translation construction identified upstream as ax1.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax1 Γ p q = (NFChoice.Fol.prf.axm ⋯).impI.impI

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax2 {L : Fol.Language} (Γ : Set (Fol.formula L)) (p q r : Fol.formula L) : Fol.prf Γ ((Fol.preformula.imp p (Fol.preformula.imp q r)).imp ((Fol.preformula.imp p q).imp (Fol.preformula.imp p r)))

Proof-translation construction identified upstream as ax2.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax3 {L : Fol.Language} (Γ : Set (Fol.formula L)) (p q : Fol.formula L) : Fol.prf Γ ((Fol.preformula.imp (Fol.not' p) (Fol.not' q)).imp (Fol.preformula.imp q p))

Proof-translation construction identified upstream as ax3.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.mp {L : Fol.Language} {Γ : Set (Fol.formula L)} {p q : Fol.formula L} (hp : Fol.prf Γ p) (hpq : Fol.prf Γ (Fol.preformula.imp p q)) : Fol.prf Γ q

Proof-translation construction identified upstream as mp.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.mp hp hpq = NFChoice.Fol.prf.impE p hpq hp

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax5 {L : Fol.Language} (Γ : Set (Fol.formula L)) (p q : Fol.formula L) : Fol.prf Γ ((Fol.preformula.imp p q).all.imp ((Fol.preformula.all p).imp (Fol.preformula.all q)))

Proof-translation construction identified upstream as ax5.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.freshIntro {L : Fol.Language} (Γ : Set (Fol.formula L)) (p : Fol.formula L) : Fol.prf Γ (Fol.preformula.imp p (Fol.liftFormula1 p).all)

Proof-translation construction identified upstream as freshIntro.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.freshIntro Γ p = (⋯.mpr (NFChoice.Fol.prf.axm ⋯)).allI.impI

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax6Core {L : Fol.Language} (Γ : Set (Fol.formula L)) (p : Fol.formula L) : Fol.prf Γ (Fol.preformula.imp (Fol.not' p) (Fol.preformula.all (Fol.not' (Fol.liftFormula1 p))))

Proof-translation construction identified upstream as ax6Core.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax6Core Γ p = id (⋯.mp (NFChoice.DirectNominalPrf.GenericLogicalHandlers.freshIntro Γ (NFChoice.Fol.not' p)))

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.equalitySubst {L : Fol.Language} (Γ : Set (Fol.formula L)) (s t : Fol.term L) (p : Fol.formula L) : Fol.prf Γ ((Fol.preformula.equal s t).imp (p [s // 0]f.imp (p [t // 0]f)))

Proof-translation construction identified upstream as equalitySubst.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.equalitySubst Γ s t p = (NFChoice.Fol.prf.subst₂ s t p (NFChoice.Fol.prf.axm ⋯) (NFChoice.Fol.prf.axm ⋯)).impI.impI

noncomputable def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax8 {L : Fol.Language} (Γ : Set (Fol.formula L)) (s t u : Fol.term L) : Fol.prf Γ ((Fol.preformula.equal s t).imp ((Fol.preformula.equal s u).imp (Fol.preformula.equal t u)))

Proof-translation construction identified upstream as ax8.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax8 Γ s t u = (NFChoice.Fol.prfTrans (NFChoice.Fol.prfSymm (NFChoice.Fol.prf.axm ⋯)) (NFChoice.Fol.prf.axm ⋯)).impI.impI

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax9 {L : Fol.Language} (Γ : Set (Fol.formula L)) (t : Fol.term L) : Fol.prf Γ (Fol.not' (Fol.preformula.all (Fol.not' (Fol.preformula.equal (&0) (Fol.liftTerm1 t)))))

Proof-translation construction identified upstream as ax9.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.nfMem (s t : Fol.term Foundation.LNF) : Fol.formula Foundation.LNF

Proof-translation construction identified upstream as nfMem.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.nfMem s t = ((NFChoice.Fol.preformula.rel NFChoice.Foundation.LNFRelation.mem).apprel s).apprel t

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax13 (Γ : Set (Fol.formula Foundation.LNF)) (s t u : Fol.term Foundation.LNF) : Fol.prf Γ ((Fol.preformula.equal s t).imp (Fol.preformula.imp (nfMem s u) (nfMem t u)))

Proof-translation construction identified upstream as ax13.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax14 (Γ : Set (Fol.formula Foundation.LNF)) (s t u : Fol.term Foundation.LNF) : Fol.prf Γ ((Fol.preformula.equal s t).imp (Fol.preformula.imp (nfMem u s) (nfMem u t)))

Proof-translation construction identified upstream as ax14.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax12Core {L : Fol.Language} (Γ : Set (Fol.formula L)) (a p : Fol.formula L) : Fol.prf Γ (Fol.preformula.imp a (Fol.preformula.imp p (Fol.liftFormula1 p).all))

Proof-translation construction identified upstream as ax12Core.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax12Core Γ a p = (⋯.mpr (⋯.mpr (NFChoice.Fol.prf.axm ⋯))).allI.impI.impI

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.swap01 {L : Fol.Language} (p : Fol.formula L) : Fol.formula L

Proof-translation construction identified upstream as swap01.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.swap01 p = ((p ↑f' 1 # 2) ↑f' 1 # 2) [&0 // 1]f [&1 // 0]f

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax7Core {L : Fol.Language} (Γ : Set (Fol.formula L)) (p : Fol.formula L) : Fol.prf Γ ((Fol.preformula.all p).all.imp (Fol.preformula.all (swap01 p)).all)

Proof-translation construction identified upstream as ax7Core.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax11Inst {L : Fol.Language} (body : Fol.formula L) (t : Fol.term L) : Fol.formula L

Proof-translation construction identified upstream as ax11Inst.

Equations

• NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax11Inst body t = (body ↑f' 1 # 1) [NFChoice.Fol.liftTerm1 t // 0]f

noncomputable def NFChoice.DirectNominalPrf.GenericLogicalHandlers.ax11Core {L : Fol.Language} (Γ : Set (Fol.formula L)) (s t : Fol.term L) (allBody targetBody template : Fol.formula L) (hSource : ax11Inst allBody t = template [Fol.liftTerm1 s // 0]f) (hTarget : template [&0 // 0]f = targetBody) : Fol.prf Γ ((Fol.preformula.equal s t).imp ((Fol.preformula.all allBody).imp ((Fol.preformula.equal (&0) (Fol.liftTerm1 t)).imp targetBody).all))

Proof-translation construction identified upstream as ax11Core.

Equations

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

def NFChoice.DirectNominalPrf.GenericLogicalHandlers.axMeredith {L : Fol.Language} (Γ : Set (Fol.formula L)) (p q r s t : Fol.formula L) : Fol.prf Γ (((((Fol.preformula.imp p q).imp (Fol.preformula.imp (Fol.not' r) (Fol.not' s))).imp r).imp t).imp ((Fol.preformula.imp t p).imp (Fol.preformula.imp s p)))

Proof-translation construction identified upstream as axMeredith.

Equations

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