NF weak partition development: NAR4H5C095M3Part035.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0005 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_D_f : f ∉ D.fv) (dv_D_u : u ∉ D.fv) (dv_D_x : x ∉ D.fv) : Nominal.TReflOn [(nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (nb095AlphaDummy003 D R S_cls E, nb095AlphaDummy005 x u D R S_cls f E), (nb095AlphaDummy001 D R S_cls E, u), (nb095AlphaDummy002 D R S_cls E, x), (nb095AlphaDummy000 D R S_cls E, f)] D.fv

Checked nominal proof certificate identified upstream as nb095_focused_refl_0005.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0005 x u D R S_cls f E dv_D_f dv_D_u dv_D_x = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0434 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy003 D R S_cls E ∉ ∅

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_fv_empty_0435 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy005 x u D R S_cls f E ∉ ∅