NF weak partition development: NominalSubstitutionLemmas.

Substitution naturality for nominal lowering. This supplies the one-hole template required by Flypitch's syntactic proof of Metamath ax-11.

theorem NFChoice.DirectNominalPrf.Nominal.underBinder_substIndexAt (replacement depth : ℕ) : (underBinder fun (index : ℕ) => substIndexAt index replacement depth) = fun (index : ℕ) => substIndexAt index replacement (depth + 1)

theorem NFChoice.DirectNominalPrf.Nominal.renameTerm_substIndexAt (replacement depth : ℕ) {l : ℕ} (t : Fol.preterm Foundation.LNF l) : renameTerm (fun (index : ℕ) => substIndexAt index replacement depth) t = Fol.substTerm t (&replacement) depth

theorem NFChoice.DirectNominalPrf.Nominal.renameFormula_substIndexAt (replacement depth : ℕ) {l : ℕ} (p : Fol.preformula l) : renameFormula (fun (index : ℕ) => substIndexAt index replacement depth) p = p [&replacement // depth]f

theorem NFChoice.DirectNominalPrf.Nominal.renameRho_subst_bind_lift (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (replacement : ℕ) : renameRho (fun (index : ℕ) => substIndexAt index replacement 0) (bindRho (liftRho rho) x) = updateRho (liftRho rho) x replacement

theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_template_subst (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (replacement : ℕ) (p : SemanticCore.Wff) : lowerWff (bindRho (liftRho rho) x) p [&replacement // 0]f = lowerWff (updateRho (liftRho rho) x replacement) p

theorem NFChoice.DirectNominalPrf.Nominal.shiftRhoAt_bind_one (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : shiftRhoAt (bindRho rho x) 1 = bindRho (liftRho rho) x

theorem NFChoice.DirectNominalPrf.Nominal.ax11Inst_lowerWff (rho : SemanticCore.Var → ℕ) (y : SemanticCore.Var) (p : SemanticCore.Wff) : GenericLogicalHandlers.ax11Inst (lowerWff (bindRho rho y) p) &(rho y) = lowerWff (liftRho rho) p

noncomputable def NFChoice.DirectNominalPrf.Nominal.ax11Structural (x y : SemanticCore.Var) (p : SemanticCore.Wff) : 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 kernel-checked nominal implementation of Metamath ax-11.

Equations

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