NF weak partition development: NominalSwapLemmas.

The concrete adjacent de-Bruijn permutation used by Metamath ax-7.

def NFChoice.DirectNominalPrf.Nominal.swapIndexAt (depth index : ℕ) : ℕ

Swap indices depth and depth + 1, fixing every other index.

Equations

• NFChoice.DirectNominalPrf.Nominal.swapIndexAt depth index = if index = depth then depth + 1 else if index = depth + 1 then depth else index

def NFChoice.DirectNominalPrf.Nominal.liftIndexAt (index amount cutoff : ℕ) : ℕ

Proof-translation construction identified upstream as liftIndexAt.

Equations

• NFChoice.DirectNominalPrf.Nominal.liftIndexAt index amount cutoff = if cutoff ≤ index then index + amount else index

def NFChoice.DirectNominalPrf.Nominal.substIndexAt (index replacement target : ℕ) : ℕ

Proof-translation construction identified upstream as substIndexAt.

Equations

• NFChoice.DirectNominalPrf.Nominal.substIndexAt index replacement target = if index < target then index else if target < index then index - 1 else replacement + target

theorem NFChoice.DirectNominalPrf.Nominal.liftTermAt_var (index amount cutoff : ℕ) : (&index ↑' amount # cutoff) = &(liftIndexAt index amount cutoff)

@[simp]

theorem NFChoice.DirectNominalPrf.Nominal.substTerm_var_var (index replacement target : ℕ) : Fol.substTerm (&index) (&replacement) target = &(substIndexAt index replacement target)

theorem NFChoice.DirectNominalPrf.Nominal.swapIndexAt_numeric (depth index : ℕ) : swapIndexAt depth index = substIndexAt (substIndexAt (liftIndexAt (liftIndexAt index 1 (depth + 2)) 1 (depth + 2)) 0 (depth + 1)) 1 depth

def NFChoice.DirectNominalPrf.Nominal.swapTermAt (depth : ℕ) {l : ℕ} (t : Fol.preterm Foundation.LNF l) : Fol.preterm Foundation.LNF l

Flypitch's lift/substitute presentation of the same term permutation.

Equations

• NFChoice.DirectNominalPrf.Nominal.swapTermAt depth t = NFChoice.Fol.substTerm (NFChoice.Fol.substTerm ((t ↑' 1 # depth + 2) ↑' 1 # depth + 2) (&0) (depth + 1)) (&1) depth

def NFChoice.DirectNominalPrf.Nominal.swapFormulaAt (depth : ℕ) {l : ℕ} (p : Fol.preformula l) : Fol.preformula l

Flypitch's lift/substitute presentation of the same formula permutation.

Equations

• NFChoice.DirectNominalPrf.Nominal.swapFormulaAt depth p = ((p ↑f' 1 # depth + 2) ↑f' 1 # depth + 2) [&0 // depth + 1]f [&1 // depth]f

theorem NFChoice.DirectNominalPrf.Nominal.underBinder_swapIndexAt (depth : ℕ) : underBinder (swapIndexAt depth) = swapIndexAt (depth + 1)

theorem NFChoice.DirectNominalPrf.Nominal.renameTerm_swapIndexAt (depth : ℕ) {l : ℕ} (t : Fol.preterm Foundation.LNF l) : renameTerm (swapIndexAt depth) t = swapTermAt depth t

theorem NFChoice.DirectNominalPrf.Nominal.renameFormula_swapIndexAt (depth : ℕ) {l : ℕ} (p : Fol.preformula l) : renameFormula (swapIndexAt depth) p = swapFormulaAt depth p

theorem NFChoice.DirectNominalPrf.Nominal.renameFormula_swap01 (p : Fol.formula Foundation.LNF) : renameFormula (swapIndexAt 0) p = GenericLogicalHandlers.swap01 p

theorem NFChoice.DirectNominalPrf.Nominal.renameRho_swap_bind_bind (rho : SemanticCore.Var → ℕ) (x y : SemanticCore.Var) (hyx : y ≠ x) : renameRho (swapIndexAt 0) (bindRho (bindRho rho x) y) = bindRho (bindRho rho y) x

theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_bind_swap (rho : SemanticCore.Var → ℕ) (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hyx : y ≠ x) : lowerWff (bindRho (bindRho rho y) x) p = GenericLogicalHandlers.swap01 (lowerWff (bindRho (bindRho rho x) y) p)

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

Total kernel-checked nominal implementation of Metamath ax-7.

Equations

• NFChoice.DirectNominalPrf.Nominal.ax7Structural x y p = NFChoice.DirectNominalPrf.Nominal.ax7 x y p ⋯