Documentation

LeanPool.NFWeakPartition.NominalLoweringLemmas

NF weak partition development: NominalLoweringLemmas.

Structural facts used by the direct Metamath certificate compiler. They turn the source $d x ph check into the exact de-Bruijn lift equation needed by Flypitch's quantifier rules.

source
def NFChoice.DirectNominalPrf.Nominal.shiftIndexAt (cutoff index : ℕ) :
ℕ

Proof-translation construction identified upstream as shiftIndexAt.

Equations
Instances For
    source
    def NFChoice.DirectNominalPrf.Nominal.shiftRhoAt (rho : SemanticCore.Var → ℕ) (cutoff : ℕ) :
    SemanticCore.Var → ℕ

    Proof-translation construction identified upstream as shiftRhoAt.

    Equations
    Instances For
      source
      @[simp]
      theorem NFChoice.DirectNominalPrf.Nominal.shiftIndexAt_zero (index : ℕ) :
      shiftIndexAt 0 index = index + 1
      source
      @[simp]
      theorem NFChoice.DirectNominalPrf.Nominal.shiftIndexAt_succ_zero (cutoff : ℕ) :
      shiftIndexAt (cutoff + 1) 0 = 0
      source
      theorem NFChoice.DirectNominalPrf.Nominal.shiftRhoAt_update (rho : SemanticCore.Var → ℕ) (cutoff : ℕ) (x : SemanticCore.Var) (candidate : ℕ) :
      shiftRhoAt (updateRho rho x candidate) cutoff = updateRho (shiftRhoAt rho cutoff) x (shiftIndexAt cutoff candidate)
      source
      theorem NFChoice.DirectNominalPrf.Nominal.shiftRhoAt_bind (rho : SemanticCore.Var → ℕ) (cutoff : ℕ) (x : SemanticCore.Var) :
      shiftRhoAt (bindRho rho x) (cutoff + 1) = bindRho (shiftRhoAt rho cutoff) x
      source
      theorem NFChoice.DirectNominalPrf.Nominal.shiftRhoAt_lift (rho : SemanticCore.Var → ℕ) (cutoff : ℕ) :
      shiftRhoAt (liftRho rho) (cutoff + 1) = liftRho (shiftRhoAt rho cutoff)
      source
      theorem NFChoice.DirectNominalPrf.Nominal.lowerClassPred_shiftAt (rho : SemanticCore.Var → ℕ) (candidate cutoff : ℕ) (A : SemanticCore.Class) :
      lowerClassPred (shiftRhoAt rho cutoff) (shiftIndexAt cutoff candidate) A = lowerClassPred rho candidate A ↑f' 1 # cutoff
      source
      theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_shiftAt (rho : SemanticCore.Var → ℕ) (cutoff : ℕ) (p : SemanticCore.Wff) :
      lowerWff (shiftRhoAt rho cutoff) p = lowerWff rho p ↑f' 1 # cutoff
      source
      theorem NFChoice.DirectNominalPrf.Nominal.lowerClassPred_congr_fv (rho sigma : SemanticCore.Var → ℕ) (candidate : ℕ) (A : SemanticCore.Class) (h : ∀ x ∈ A.fv, rho x = sigma x) :
      lowerClassPred rho candidate A = lowerClassPred sigma candidate A
      source
      theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_congr_fv (rho sigma : SemanticCore.Var → ℕ) (p : SemanticCore.Wff) (h : ∀ x ∈ p.fv, rho x = sigma x) :
      lowerWff rho p = lowerWff sigma p
      source
      theorem NFChoice.DirectNominalPrf.Nominal.bindRho_eq_shiftRhoAt_zero_of_ne (rho : SemanticCore.Var → ℕ) {x y : SemanticCore.Var} (hyx : y ≠ x) :
      bindRho rho x y = shiftRhoAt rho 0 y
      source
      theorem NFChoice.DirectNominalPrf.Nominal.lowerWff_bind_eq_lift_of_not_mem_fv (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (p : SemanticCore.Wff) (hx : x ∉ p.fv) :
      lowerWff (bindRho rho x) p = Fol.liftFormula1 (lowerWff rho p)
      source
      def NFChoice.DirectNominalPrf.Nominal.ax17 (p : SemanticCore.Wff) (x : SemanticCore.Var) (hx : x ∉ p.fv) :
      NPrf (p.imp (SemanticCore.Wff.all x p))

      Proof-translation construction identified upstream as ax17.

      Equations
      Instances For