Nominal proof certificates grouped in dependency order.

Certificates from AlphaSupport.NAR4H5C095M3Part036Stage1.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0079 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy261 D R S_cls E, nb095AlphaDummy262 x R), (nb095AlphaDummy259 D R S_cls E, nb095AlphaDummy260 x R), (nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy261 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy261 D R S_cls E)) (SemanticCore.Class.cab (nb095AlphaDummy255 D R S_cls E) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy256 D R S_cls E) (SemanticCore.Class.cv (nb095AlphaDummy250 D R S_cls E)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy255 D R S_cls E)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy262 x R)) (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy252 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy262 x R)) (SemanticCore.Class.cab (nb095AlphaDummy257 x R) (Compiler.CompactSourceSyntax.synWrex (nb095AlphaDummy258 x R) (SemanticCore.Class.cv (nb095AlphaDummy252 x R)) (SemanticCore.Wff.classEq (SemanticCore.Class.cv (nb095AlphaDummy257 x R)) (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0079.

Equations

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

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095SplitAlpha0080 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : Nominal.TAlphaWff [(nb095AlphaDummy287 D R S_cls E, nb095AlphaDummy288 x R), (nb095AlphaDummy256 D R S_cls E, nb095AlphaDummy258 x R), (nb095AlphaDummy255 D R S_cls E, nb095AlphaDummy257 x R), (nb095AlphaDummy285 D R S_cls E, nb095AlphaDummy286 x R), (nb095AlphaDummy259 D R S_cls E, nb095AlphaDummy260 x R), (nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (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)] ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy287 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy256 D R S_cls E))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy287 D R S_cls E)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg) ((SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy288 x R)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCphi (SemanticCore.Class.cv (nb095AlphaDummy258 x R))))).imp (SemanticCore.Wff.classMem (SemanticCore.Class.cv (nb095AlphaDummy288 x R)) (Compiler.CompactSourceSyntax.synCcompl (Compiler.CompactSourceSyntax.synCsn Compiler.CompactSourceSyntax.synC0c))).neg)

Checked nominal proof certificate identified upstream as nb095_split_alpha_0080.

Equations

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

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

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_1500 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy003 D R S_cls E ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0047 (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 ∉ R.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_wpp_notmem_1501 (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 ∉ (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0273 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) : Nominal.TEnvFresh [(nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (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)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

Certificates from AlphaSupport.NAR4H5C095M3Part036Stage2.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0267 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) (dv_R_f : f ∉ R.fv) (dv_R_u : u ∉ R.fv) (dv_R_x : x ∉ R.fv) : Nominal.TReflOn [(nb095AlphaDummy250 D R S_cls E, nb095AlphaDummy252 x R), (nb095AlphaDummy249 D R S_cls E, nb095AlphaDummy251 x R), (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)] (Compiler.CompactSourceSyntax.synCcnv (Compiler.CompactSourceSyntax.synCdif R Compiler.CompactSourceSyntax.synCid)).fv

Checked nominal proof certificate identified upstream as nb095_wpp_refl_0267.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095WppRefl0267 x u D R S_cls f E dv_R_f dv_R_u dv_R_x = ⋯.reflOn

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0048 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy004 D R S_cls E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_focused_notmem_0049 (x u : SemanticCore.Var) (D R S_cls : SemanticCore.Class) (f : SemanticCore.Var) (E : SemanticCore.Class) : nb095AlphaDummy006 x u D R S_cls f E ∉ D.fv

theorem NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095_compact_envfresh_0274 (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.TEnvFresh [(nb095AlphaDummy247 D R S_cls E, nb095AlphaDummy248 x D R), (nb095AlphaDummy245 D R S_cls E, nb095AlphaDummy246 x D R), (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)] D.fv

Certificates from AlphaSupport.NAR4H5C095M3Part036Stage3.

noncomputable def NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0006 (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), (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)] D.fv

Checked nominal proof certificate identified upstream as nb095_focused_refl_0006.

Equations

• NFChoice.DirectNominalPrf.NominalAlphaWrappersRepaired.nb095FocusedRefl0006 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_0436 (D R S_cls E : SemanticCore.Class) : nb095AlphaDummy004 D R S_cls E ∉ ∅

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