NF weak partition development: NominalDfClabStructuralDev005.

@[reducible, inline]

abbrev NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.Theory : Fol.SentTheory Foundation.LNF

Proof-translation construction identified upstream as Theory.

Equations

• NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.Theory = NFChoice.Foundation.ExactLiteralTrial.LiteralHailperinNF

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.renameRho_subst_bind (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (replacement : ℕ) : renameRho (fun (index : ℕ) => substIndexAt index replacement 0) (bindRho rho x) = updateRho rho x replacement

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.lowerWff_bound_subst (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (replacement : ℕ) (p : SemanticCore.Wff) : lowerWff (bindRho rho x) p [&replacement // 0]f = lowerWff (updateRho rho x replacement) p

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.updateRho_self (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : updateRho rho x (rho x) = rho

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.updateRho_lift_zero_eq_bind (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : updateRho (liftRho rho) x 0 = bindRho rho x

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.classPred_cv (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) : ClassHandlersDev011.classPred rho (SemanticCore.Class.cv x) = DirectCertificate.ClassBoundaryNormalizationDev005.cvPred &(rho x)

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.classPred_cab (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (p : SemanticCore.Wff) : ClassHandlersDev011.classPred rho (SemanticCore.Class.cab x p) = lowerWff (bindRho rho x) p

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.lowerWff_sbDefiniens_ne (rho : SemanticCore.Var → ℕ) (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hxy : x ≠ y) : lowerWff rho (SemanticCore.sbDefiniens x y p) = DfClabProperSubstitutionCoreDev003.properSubstRhs (lowerWff (bindRho rho y) p) &(rho x) &(rho y)

theorem NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.lowerWff_sbDefiniens_same (rho : SemanticCore.Var → ℕ) (x : SemanticCore.Var) (p : SemanticCore.Wff) : lowerWff rho (SemanticCore.sbDefiniens x x p) = DfClabProperSubstitutionCoreDev003.coincidentSubstRhs (lowerWff (bindRho rho x) p) &(rho x)

noncomputable def NFChoice.DirectNominalPrf.Nominal.DfClabStructuralDev005.dfClabStructural (x y : SemanticCore.Var) (p : SemanticCore.Wff) : NPrf (ClassHandlersDev011.dfClabGoal x y p)

Proof-translation construction identified upstream as dfClabStructural.

Equations

• One or more equations did not get rendered due to their size.