NF weak partition development: NominalRenamingLemmas.

Functoriality of nominal lowering under a de-Bruijn variable renaming.

This is the structural bridge needed by binder-permutation rules such as Metamath ax-7: instead of proving a fresh equality for every generated application, the certificate compiler can instantiate one kernel-checked renaming theorem.

def NFChoice.DirectNominalPrf.Nominal.underBinder (sigma : ℕ → ℕ) : ℕ → ℕ

Extend a renaming under one de-Bruijn binder.

Equations

• NFChoice.DirectNominalPrf.Nominal.underBinder sigma 0 = 0
• NFChoice.DirectNominalPrf.Nominal.underBinder sigma n.succ = sigma n + 1

def NFChoice.DirectNominalPrf.Nominal.renameTerm (sigma : ℕ → ℕ) {l : ℕ} : Fol.preterm Foundation.LNF l → Fol.preterm Foundation.LNF l

Apply a de-Bruijn renaming to a (possibly partially applied) term.

Equations

• NFChoice.DirectNominalPrf.Nominal.renameTerm sigma &n = &(sigma n)
• NFChoice.DirectNominalPrf.Nominal.renameTerm sigma (NFChoice.Fol.preterm.func f) = NFChoice.Fol.preterm.func f
• NFChoice.DirectNominalPrf.Nominal.renameTerm sigma (t.app s) = (NFChoice.DirectNominalPrf.Nominal.renameTerm sigma t).app (NFChoice.DirectNominalPrf.Nominal.renameTerm sigma s)

def NFChoice.DirectNominalPrf.Nominal.renameFormula (sigma : ℕ → ℕ) {l : ℕ} : Fol.preformula l → Fol.preformula l

Apply a de-Bruijn renaming to a (possibly partially applied) formula.

Equations

• One or more equations did not get rendered due to their size.
• NFChoice.DirectNominalPrf.Nominal.renameFormula sigma ⊥' = ⊥'
• NFChoice.DirectNominalPrf.Nominal.renameFormula sigma (NFChoice.Fol.preformula.rel r) = NFChoice.Fol.preformula.rel r
• NFChoice.DirectNominalPrf.Nominal.renameFormula sigma (p.apprel t) = (NFChoice.DirectNominalPrf.Nominal.renameFormula sigma p).apprel (NFChoice.DirectNominalPrf.Nominal.renameTerm sigma t)
• NFChoice.DirectNominalPrf.Nominal.renameFormula sigma (p.imp q) = (NFChoice.DirectNominalPrf.Nominal.renameFormula sigma p).imp (NFChoice.DirectNominalPrf.Nominal.renameFormula sigma q)
• NFChoice.DirectNominalPrf.Nominal.renameFormula sigma p.all = (NFChoice.DirectNominalPrf.Nominal.renameFormula (NFChoice.DirectNominalPrf.Nominal.underBinder sigma) p).all

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

Proof-translation construction identified upstream as renameRho.

Equations

• NFChoice.DirectNominalPrf.Nominal.renameRho sigma rho x = sigma (rho x)

@[simp]

theorem NFChoice.DirectNominalPrf.Nominal.underBinder_zero (sigma : ℕ → ℕ) : underBinder sigma 0 = 0

@[simp]

theorem NFChoice.DirectNominalPrf.Nominal.underBinder_succ (sigma : ℕ → ℕ) (n : ℕ) : underBinder sigma (n + 1) = sigma n + 1

theorem NFChoice.DirectNominalPrf.Nominal.renameRho_update (sigma : ℕ → ℕ) (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (candidate : ℕ) : renameRho sigma (updateRho rho x candidate) = updateRho (renameRho sigma rho) x (sigma candidate)

theorem NFChoice.DirectNominalPrf.Nominal.renameRho_bind (sigma : ℕ → ℕ) (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : renameRho (underBinder sigma) (bindRho rho x) = bindRho (renameRho sigma rho) x

theorem NFChoice.DirectNominalPrf.Nominal.renameRho_lift (sigma : ℕ → ℕ) (rho : SemanticCore.Var → ℕ) : renameRho (underBinder sigma) (liftRho rho) = liftRho (renameRho sigma rho)

theorem NFChoice.DirectNominalPrf.Nominal.lowerClassPred_rename (sigma : ℕ → ℕ) (rho : SemanticCore.Var → ℕ) (candidate : ℕ) (A : SemanticCore.Class) : lowerClassPred (renameRho sigma rho) (sigma candidate) A = renameFormula sigma (lowerClassPred rho candidate A)

theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_rename (sigma : ℕ → ℕ) (rho : SemanticCore.Var → ℕ) (p : SemanticCore.Wff) : lowerWff (renameRho sigma rho) p = renameFormula sigma (lowerWff rho p)