NF weak partition development: NAR4H5C095M3Part044.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0010 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_E_f : f ∉ E.fv) (dv_E_u : u ∉ E.fv) (dv_E_x : x ∉ E.fv) : Nominal.TReflOn [(nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy794 D R S_cls E, nb095AlphaDummy796 u S_cls E), (nb095AlphaDummy793 D R S_cls E, nb095AlphaDummy795 u S_cls E), (nb095AlphaDummy797 D R S_cls E, nb095AlphaDummy798 u S_cls E), (nb095AlphaDummy791 D R S_cls E, nb095AlphaDummy792 u S_cls E), (nb095AlphaDummy789 D R S_cls E, nb095AlphaDummy790 u S_cls E), (nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (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)] E.fv

Checked nominal proof certificate identified upstream as nb095_focused_refl_0010.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0010 x u D R S_cls f E dv_E_f dv_E_u dv_E_x = ⋯.reflOn

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0098 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy351 D R S_cls E, nb095AlphaDummy352 u S_cls), (nb095AlphaDummy349 D R S_cls E, nb095AlphaDummy350 u S_cls), (nb095AlphaDummy340 D R S_cls E, nb095AlphaDummy342 u S_cls), (nb095AlphaDummy339 D R S_cls E, nb095AlphaDummy341 u S_cls), (nb095AlphaDummy337 D R S_cls E, nb095AlphaDummy338 u S_cls E), (nb095AlphaDummy335 D R S_cls E, nb095AlphaDummy336 u S_cls E), (nb095AlphaDummy794 D R S_cls E, nb095AlphaDummy796 u S_cls E), (nb095AlphaDummy793 D R S_cls E, nb095AlphaDummy795 u S_cls E), (nb095AlphaDummy797 D R S_cls E, nb095AlphaDummy798 u S_cls E), (nb095AlphaDummy791 D R S_cls E, nb095AlphaDummy792 u S_cls E), (nb095AlphaDummy789 D R S_cls E, nb095AlphaDummy790 u S_cls E), (nb095AlphaDummy004 D R S_cls E, nb095AlphaDummy006 x u D R S_cls f E), (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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy351 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy351 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy345 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy346 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy340 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy345 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy346 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy352 u S_cls)) (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy352 u S_cls)) (SemanticCore.Class.cab (nb095AlphaDummy347 u S_cls) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy348 u S_cls) (SemanticCore.Class.cv (nb095AlphaDummy342 u S_cls)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy347 u S_cls)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy348 u S_cls))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0098.

Equations

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