NF weak partition development: NominalClassHandlersDev011.

@[reducible, inline]

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

Proof-translation construction identified upstream as Theory.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.classPred (rho : SemanticCore.Var → ℕ) (A : SemanticCore.Class) : Fol.formula Foundation.LNF

The candidate-slot predicate used for a nominal class at valuation rho.

Equations

• NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.classPred rho A = NFChoice.DirectNominalPrf.Nominal.lowerClassPred (NFChoice.DirectNominalPrf.Nominal.liftRho rho) 0 A

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

Exact normalized source conclusion of df-clab.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfCleqGoal (x : SemanticCore.Var) (A B : SemanticCore.Class) : SemanticCore.Wff

Exact normalized source conclusion of df-cleq.

Equations

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

def NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfClelGoal (x : SemanticCore.Var) (A B : SemanticCore.Class) : SemanticCore.Wff

Exact normalized source conclusion of df-clel.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfClabOfLowering (x y : SemanticCore.Var) (p : SemanticCore.Wff) (hClassMem : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cab y p)) = DirectCertificate.ClassBoundaryCoreDev006.classMem (DirectCertificate.ClassBoundaryNormalizationDev005.cvPred &(rho x)) (classPred rho (SemanticCore.Class.cab y p))) (hSubst : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (SemanticCore.sbDefiniens x y p) = DirectCertificate.ClassBoundaryNormalizationDev005.applyPred (classPred rho (SemanticCore.Class.cab y p)) &(rho x)) : NPrf (dfClabGoal x y p)

Sound df-clab handler. hClassMem is structural lowering; hSubst is the compiler's checked normalization equation identifying application of a class abstraction with the already-expanded proper-substitution definiens.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfCleqOfShift (x y z : SemanticCore.Var) (A B : SemanticCore.Class) (_hAxExt : NPrf ((SemanticCore.Wff.all x ((SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv y)).biimp (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) (SemanticCore.Class.cv z)))).imp (SemanticCore.Wff.classEq (SemanticCore.Class.cv y) (SemanticCore.Class.cv z)))) (hClassEq : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (SemanticCore.Wff.classEq A B) = DirectCertificate.ClassBoundaryCoreDev006.classEq (classPred rho A) (classPred rho B)) (hMemA : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) A) = DirectCertificate.ClassBoundaryRawHandlersDev010.liftedClassMem (classPred rho A)) (hMemB : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) = DirectCertificate.ClassBoundaryRawHandlersDev010.liftedClassMem (classPred rho B)) : NPrf (dfCleqGoal x A B)

Sound df-cleq handler. The first proof argument preserves the original MM0/Metamath exporter signature. The exact theory already contains ax-ext; the two bridge equations are the kernel-visible images of $d x A and $d x B.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.Nominal.ClassHandlersDev011.dfClelOfShift (x : SemanticCore.Var) (A B : SemanticCore.Class) (hClassMem : ∀ (rho : SemanticCore.Var → ℕ), lowerWff rho (SemanticCore.Wff.classMem A B) = DirectCertificate.ClassBoundaryCoreDev006.classMem (classPred rho A) (classPred rho B)) (hEqA : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) (SemanticCore.Wff.classEq (SemanticCore.Class.cv x) A) = DirectCertificate.ClassBoundaryNormalizationDev005.represents (&0) (classPred rho A ↑f' 1 # 1)) (hMemB : ∀ (rho : SemanticCore.Var → ℕ), lowerWff (bindRho rho x) (SemanticCore.Wff.classMem (SemanticCore.Class.cv x) B) = DirectCertificate.ClassBoundaryRawHandlersDev010.liftedClassMem (classPred rho B)) : NPrf (dfClelGoal x A B)

Sound df-clel handler. The three identities expose the source DV facts and the structural class lowering rather than hiding them in an axiom.

Equations

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