NF weak partition development: BoundedNominalLoweringBridgeDev004.

def NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.finValRho {n : ℕ} (rho : SemanticCore.Var → Fin n) : SemanticCore.Var → ℕ

Proof-translation construction identified upstream as finValRho.

Equations

• NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.finValRho rho x = ↑(rho x)

theorem NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.finVal_update {n : ℕ} (rho : SemanticCore.Var → Fin n) (x : SemanticCore.Var) (value : Fin n) : finValRho (Function.update rho x value) = updateRho (finValRho rho) x ↑value

theorem NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.finVal_lift {n : ℕ} (rho : SemanticCore.Var → Fin n) : finValRho (SemanticCore.Lowering.liftRho rho) = liftRho (finValRho rho)

theorem NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.finVal_bind {n : ℕ} (rho : SemanticCore.Var → Fin n) (x : SemanticCore.Var) : finValRho (SemanticCore.Lowering.bindRho rho x) = bindRho (finValRho rho) x

theorem NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.lowerClassPred_toFlypitch {n : ℕ} (rho : SemanticCore.Var → Fin n) (candidate : Fin n) (A : SemanticCore.Class) : lowerClassPred (finValRho rho) (↑candidate) A = Fol.BoundedPreformula.fst (SemanticCore.Lowering.lowerClassPred rho candidate A).toFlypitch

theorem NFChoice.DirectNominalPrf.Nominal.BoundedNominalLoweringBridgeDev004.lowerWff_toFlypitch {n : ℕ} (rho : SemanticCore.Var → Fin n) (p : SemanticCore.Wff) : lowerWff (finValRho rho) p = Fol.BoundedPreformula.fst (SemanticCore.Lowering.lowerWff rho p).toFlypitch