NF weak partition development: NAR4H5C095M3Part028.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0188 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TReflOn [(nb095AlphaDummy383 D R S_cls E, nb095AlphaDummy384 f), (nb095AlphaDummy381 D R S_cls E, nb095AlphaDummy382 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] Compiler.CompactSourceSyntax.synCid.fv

Checked nominal proof certificate identified upstream as nb095_wpp_refl_0188.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0188 x u D R S_cls f E = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0057 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy399 D R S_cls E, nb095AlphaDummy400 f), (nb095AlphaDummy397 D R S_cls E, nb095AlphaDummy398 f), (nb095AlphaDummy386 D R S_cls E, nb095AlphaDummy389 f), (nb095AlphaDummy385 D R S_cls E, nb095AlphaDummy388 f), (nb095AlphaDummy391 D R S_cls E, nb095AlphaDummy392 f), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy399 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy393 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy394 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy385 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy393 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy399 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy393 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy394 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy385 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy393 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy394 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy400 f)) (SemanticCore.Class.cab (nb095AlphaDummy395 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy396 f) (SemanticCore.Class.cv (nb095AlphaDummy388 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy395 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy400 f)) (SemanticCore.Class.cab (nb095AlphaDummy395 f) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy396 f) (SemanticCore.Class.cv (nb095AlphaDummy388 f)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy395 f)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy396 f))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0057.

Equations

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