NF weak partition development: PartialTotalizationBridgeDev002.

def NFChoice.DirectNominalPrf.Nominal.Totalization.totalizeRho {n : ℕ} (rho : SemanticCore.Var → Option (Fin n)) (default : Fin n) : SemanticCore.Var → Fin n

Proof-translation construction identified upstream as totalizeRho.

Equations

• NFChoice.DirectNominalPrf.Nominal.Totalization.totalizeRho rho default x = (rho x).getD default

theorem NFChoice.DirectNominalPrf.Nominal.Totalization.totalize_update_some {n : ℕ} (rho : SemanticCore.Var → Option (Fin n)) (default value : Fin n) (x : SemanticCore.Var) : totalizeRho (Function.update rho x (some value)) default = Function.update (totalizeRho rho default) x value

theorem NFChoice.DirectNominalPrf.Nominal.Totalization.totalize_lift {n : ℕ} (rho : SemanticCore.Var → Option (Fin n)) (default : Fin n) : totalizeRho (SemanticCore.PartialLowering.liftRhoOption rho) default.succ = SemanticCore.Lowering.liftRho (totalizeRho rho default)

theorem NFChoice.DirectNominalPrf.Nominal.Totalization.totalize_bind {n : ℕ} (rho : SemanticCore.Var → Option (Fin n)) (default : Fin n) (x : SemanticCore.Var) : totalizeRho (SemanticCore.PartialLowering.bindRhoOption rho x) default.succ = SemanticCore.Lowering.bindRho (totalizeRho rho default) x

theorem NFChoice.DirectNominalPrf.Nominal.Totalization.lowerClassPredOption_some_totalize {n : ℕ} (rho : SemanticCore.Var → Option (Fin n)) (default candidate : Fin n) (A : SemanticCore.Class) (f : Foundation.Formula n) (h : SemanticCore.PartialLowering.lowerClassPredOption rho candidate A = some f) : SemanticCore.Lowering.lowerClassPred (totalizeRho rho default) candidate A = f

theorem NFChoice.DirectNominalPrf.Nominal.Totalization.lowerWffOption_some_totalize {n : ℕ} (rho : SemanticCore.Var → Option (Fin n)) (default : Fin n) (p : SemanticCore.Wff) (f : Foundation.Formula n) (h : SemanticCore.PartialLowering.lowerWffOption rho p = some f) : SemanticCore.Lowering.lowerWff (totalizeRho rho default) p = f